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.
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.
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
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_targett::assignment_typet assignment_type
symex_assignt(goto_symex_statet &state, symex_targett::assignment_typet assignment_type, const namespacet &ns, const symex_configt &symex_config, symex_targett &target)
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)
The interface of the target container for symbolic execution to record its symbolic steps into.
Semantic type conversion.
Definition std_expr.h:1920
Configuration used for a symbolic execution.
Generate Equation using Symbolic Execution.