CBMC: /home/runner/work/cbmc/cbmc/src/goto-symex/symex_assign.cpp File Reference

CBMC

Loading...

Searching...

No Matches

Classes | Functions

symex_assign.cpp File Reference

Symbolic Execution. More...

#include "symex_assign.h"
#include <util/byte_operators.h>
#include <util/pointer_expr.h>
#include <util/range.h>
#include "expr_skeleton.h"
#include "goto_symex_state.h"
#include "simplify_expr_with_value_set.h"
#include "symex_config.h"

+ Include dependency graph for symex_assign.cpp:

Go to the source code of this file.

Classes

struct assignmentt

Assignment from the rhs value to the lhs variable. More...

Functions

constexpr bool use_update ()

static bool is_string_constant_initialization (const exprt &rhs)

Determine whether the RHS expression is a string constant initialization.

Detailed Description

Symbolic Execution.

Definition in file symex_assign.cpp.

Function Documentation

◆ is_string_constant_initialization()

static bool is_string_constant_initialization ( const exprt & rhs )

static

Determine whether the RHS expression is a string constant initialization.

Parameters: rhs The RHS expression

Returns: True if the expression points to the first character of a string constant

Definition at line 41 of file symex_assign.cpp.

◆ use_update()

constexpr bool use_update ( )

constexpr

Definition at line 28 of file symex_assign.cpp.