cprover
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 "symex_target.h"
16#include <util/expr.h>
17
19class expr_skeletont;
21class ssa_exprt;
22struct symex_configt;
23
26{
27public:
31 const namespacet &ns,
34 : state(state),
36 ns(ns),
39 {
40 }
41
46 void assign_symbol(
47 const ssa_exprt &lhs, // L1
48 const expr_skeletont &full_lhs,
49 const exprt &rhs,
50 const exprt::operandst &guard);
51
52 void assign_rec(
53 const exprt &lhs,
54 const expr_skeletont &full_lhs,
55 const exprt &rhs,
56 exprt::operandst &guard);
57
58private:
61 const namespacet &ns;
64
66 const ssa_exprt &lhs, // L1
67 const expr_skeletont &full_lhs,
68 const struct_exprt &rhs,
69 const exprt::operandst &guard);
70
72 const ssa_exprt &lhs, // L1
73 const expr_skeletont &full_lhs,
74 const exprt &rhs,
75 const exprt::operandst &guard);
76
79 template <bool use_update>
80 void assign_array(
81 const index_exprt &lhs,
82 const expr_skeletont &full_lhs,
83 const exprt &rhs,
84 exprt::operandst &guard);
85
88 template <bool use_update>
90 const member_exprt &lhs,
91 const expr_skeletont &full_lhs,
92 const exprt &rhs,
93 exprt::operandst &guard);
94
95 void assign_if(
96 const if_exprt &lhs,
97 const expr_skeletont &full_lhs,
98 const exprt &rhs,
99 exprt::operandst &guard);
100
101 void assign_typecast(
102 const typecast_exprt &lhs,
103 const expr_skeletont &full_lhs,
104 const exprt &rhs,
105 exprt::operandst &guard);
106
108 const byte_extract_exprt &lhs,
109 const expr_skeletont &full_lhs,
110 const exprt &rhs,
111 exprt::operandst &guard);
112};
113
114#endif // CPROVER_GOTO_SYMEX_SYMEX_ASSIGN_H
Expression of type type extracted from some object op starting at position offset (given in number of...
Expression in which some part is missing and can be substituted for another expression.
Definition: expr_skeleton.h:26
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
Central data structure: state.
The trinary if-then-else operator.
Definition: std_expr.h:2226
Array index operator.
Definition: std_expr.h:1328
Extract member of struct or union.
Definition: std_expr.h:2667
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:1722
Functor for symex assignment.
Definition: symex_assign.h:26
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 symex_configt & symex_config
Definition: symex_assign.h:62
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
Definition: symex_assign.h:59
void assign_array(const index_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
symex_targett & target
Definition: symex_assign.h:63
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_targett::assignment_typet assignment_type
Definition: symex_assign.h:60
symex_assignt(goto_symex_statet &state, symex_targett::assignment_typet assignment_type, const namespacet &ns, const symex_configt &symex_config, symex_targett &target)
Definition: symex_assign.h:28
const namespacet & ns
Definition: symex_assign.h:61
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)
The interface of the target container for symbolic execution to record its symbolic steps into.
Definition: symex_target.h:25
Semantic type conversion.
Definition: std_expr.h:1920
Configuration used for a symbolic execution.
Definition: symex_config.h:17
Generate Equation using Symbolic Execution.