CBMC
Loading...
Searching...
No Matches
symex_assign.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution
4
5Author: Romain Brenguier, romain.brenguier@diffblue.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_SYMEX_SYMEX_ASSIGN_H
13#define CPROVER_GOTO_SYMEX_SYMEX_ASSIGN_H
14
15#include <util/expr.h>
16
17#include "shadow_memory.h"
18#include "symex_target.h"
19
21class expr_skeletont;
23class ssa_exprt;
24struct symex_configt;
25
28{
29public:
47
52 void assign_symbol(
53 const ssa_exprt &lhs, // L1
54 const expr_skeletont &full_lhs,
55 const exprt &rhs,
56 const exprt::operandst &guard);
57
58 void assign_rec(
59 const exprt &lhs,
60 const expr_skeletont &full_lhs,
61 const exprt &rhs,
63
64private:
65 std::optional<shadow_memoryt> shadow_memory;
68 const namespacet &ns;
72
74 const ssa_exprt &lhs, // L1
75 const expr_skeletont &full_lhs,
76 const struct_exprt &rhs,
77 const exprt::operandst &guard);
78
80 const ssa_exprt &lhs, // L1
81 const expr_skeletont &full_lhs,
82 const exprt &rhs,
83 const exprt::operandst &guard);
84
87 template <bool use_update>
88 void assign_array(
89 const index_exprt &lhs,
90 const expr_skeletont &full_lhs,
91 const exprt &rhs,
93
96 template <bool use_update>
98 const member_exprt &lhs,
99 const expr_skeletont &full_lhs,
100 const exprt &rhs,
102
103 void assign_if(
104 const if_exprt &lhs,
105 const expr_skeletont &full_lhs,
106 const exprt &rhs,
108
109 void assign_typecast(
110 const typecast_exprt &lhs,
111 const expr_skeletont &full_lhs,
112 const exprt &rhs,
114
116 const byte_extract_exprt &lhs,
117 const expr_skeletont &full_lhs,
118 const exprt &rhs,
120};
121
122#endif // CPROVER_GOTO_SYMEX_SYMEX_ASSIGN_H
static exprt guard(const exprt::operandst &guards, exprt cond)
Expression of type type extracted from some object op starting at position offset (given in number of...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Expression in which some part is missing and can be substituted for another expression.
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
Central data structure: state.
The trinary if-then-else operator.
Definition std_expr.h:2502
Array index operator.
Definition std_expr.h:1470
Extract member of struct or union.
Definition std_expr.h:2972
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Expression providing an SSA-renamed symbol of expressions.
Definition ssa_expr.h:17
Struct constructor from list of elements.
Definition std_expr.h:1877
Functor for symex assignment.
void assign_byte_extract(const byte_extract_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
void assign_if(const if_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
const irep_idt & language_mode
const symex_configt & symex_config
void assign_non_struct_symbol(const ssa_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, const exprt::operandst &guard)
goto_symex_statet & state
void assign_array(const index_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
symex_targett & target
void assign_rec(const exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
void assign_symbol(const ssa_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, const exprt::operandst &guard)
Record the assignment of value rhs to variable lhs in state and add the equation to target: lhs#{n+1}...
void assign_struct_member(const member_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
symex_assignt(std::optional< shadow_memoryt > shadow_memory, goto_symex_statet &state, symex_targett::assignment_typet assignment_type, const namespacet &ns, const symex_configt &symex_config, const irep_idt &language_mode, symex_targett &target)
symex_targett::assignment_typet assignment_type
const namespacet & ns
void assign_from_struct(const ssa_exprt &lhs, const expr_skeletont &full_lhs, const struct_exprt &rhs, const exprt::operandst &guard)
Assign a struct expression to a symbol.
void assign_typecast(const typecast_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
std::optional< shadow_memoryt > shadow_memory
The interface of the target container for symbolic execution to record its symbolic steps into.
Semantic type conversion.
Definition std_expr.h:2073
Symex Shadow Memory Instrumentation.
Configuration used for a symbolic execution.
Generate Equation using Symbolic Execution.