cprover
symex_assign.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "symex_assign.h"
13 
14 #include "expr_skeleton.h"
15 #include "goto_symex_state.h"
16 #include <util/byte_operators.h>
17 #include <util/expr_util.h>
18 #include <util/range.h>
19 
20 #include "symex_config.h"
21 
22 // We can either use with_exprt or update_exprt when building expressions that
23 // modify components of an array or a struct. Set USE_UPDATE to use
24 // update_exprt.
25 // #define USE_UPDATE
26 
27 constexpr bool use_update()
28 {
29 #ifdef USE_UPDATE
30  return true;
31 #else
32  return false;
33 #endif
34 }
35 
37  const exprt &lhs,
38  const expr_skeletont &full_lhs,
39  const exprt &rhs,
40  exprt::operandst &guard)
41 {
42  if(is_ssa_expr(lhs))
43  {
44  assign_symbol(to_ssa_expr(lhs), full_lhs, rhs, guard);
45  }
46  else if(lhs.id() == ID_index)
47  assign_array<use_update()>(to_index_expr(lhs), full_lhs, rhs, guard);
48  else if(lhs.id()==ID_member)
49  {
50  const typet &type = to_member_expr(lhs).struct_op().type();
51  if(type.id() == ID_struct || type.id() == ID_struct_tag)
52  {
53  assign_struct_member<use_update()>(
54  to_member_expr(lhs), full_lhs, rhs, guard);
55  }
56  else if(type.id() == ID_union || type.id() == ID_union_tag)
57  {
58  // should have been replaced by byte_extract
60  "assign_rec: unexpected assignment to union member");
61  }
62  else
64  "assign_rec: unexpected assignment to member of '" + type.id_string() +
65  "'");
66  }
67  else if(lhs.id()==ID_if)
68  assign_if(to_if_expr(lhs), full_lhs, rhs, guard);
69  else if(lhs.id()==ID_typecast)
70  assign_typecast(to_typecast_expr(lhs), full_lhs, rhs, guard);
72  {
73  // ignore
74  }
75  else if(lhs.id()==ID_byte_extract_little_endian ||
76  lhs.id()==ID_byte_extract_big_endian)
77  {
78  assign_byte_extract(to_byte_extract_expr(lhs), full_lhs, rhs, guard);
79  }
80  else if(lhs.id() == ID_complex_real)
81  {
82  // this is stuff like __real__ x = 1;
83  const complex_real_exprt &complex_real_expr = to_complex_real_expr(lhs);
84 
85  const complex_imag_exprt complex_imag_expr(complex_real_expr.op());
86 
87  complex_exprt new_rhs(
88  rhs, complex_imag_expr, to_complex_type(complex_real_expr.op().type()));
89 
90  assign_rec(complex_real_expr.op(), full_lhs, new_rhs, guard);
91  }
92  else if(lhs.id() == ID_complex_imag)
93  {
94  const complex_imag_exprt &complex_imag_expr = to_complex_imag_expr(lhs);
95 
96  const complex_real_exprt complex_real_expr(complex_imag_expr.op());
97 
98  complex_exprt new_rhs(
99  complex_real_expr, rhs, to_complex_type(complex_imag_expr.op().type()));
100 
101  assign_rec(complex_imag_expr.op(), full_lhs, new_rhs, guard);
102  }
103  else
105  "assignment to '" + lhs.id_string() + "' not handled");
106 }
107 
109 struct assignmentt final
110 {
115 };
116 
129  const ssa_exprt &lhs, // L1
130  const expr_skeletont &full_lhs,
131  const struct_exprt &rhs,
132  const exprt::operandst &guard)
133 {
134  const auto &components = to_struct_type(ns.follow(lhs.type())).components();
135  PRECONDITION(rhs.operands().size() == components.size());
136 
137  for(const auto &comp_rhs : make_range(components).zip(rhs.operands()))
138  {
139  const auto &comp = comp_rhs.first;
140  const exprt lhs_field = state.field_sensitivity.apply(
141  ns, state, member_exprt{lhs, comp.get_name(), comp.type()}, true);
142  INVARIANT(
143  lhs_field.id() == ID_symbol,
144  "member of symbol should be susceptible to field-sensitivity");
145 
146  assign_symbol(to_ssa_expr(lhs_field), full_lhs, comp_rhs.second, guard);
147  }
148 }
149 
151  const ssa_exprt &lhs, // L1
152  const expr_skeletont &full_lhs,
153  const exprt &rhs,
154  const exprt::operandst &guard)
155 {
156  exprt l2_rhs =
157  state
158  .rename(
159  // put assignment guard into the rhs
160  guard.empty()
161  ? rhs
162  : static_cast<exprt>(if_exprt{conjunction(guard), rhs, lhs}),
163  ns)
164  .get();
165 
166  assignmentt assignment{lhs, full_lhs, l2_rhs};
167 
169  assignment.rhs = simplify_expr(std::move(assignment.rhs), ns);
170 
171  const ssa_exprt l2_lhs = state
172  .assignment(
173  assignment.lhs,
174  assignment.rhs,
175  ns,
179  .get();
180 
181  state.record_events.push(false);
182  // Note any other symbols mentioned in the skeleton are rvalues -- for example
183  // array indices -- and were renamed to L2 at the start of
184  // goto_symext::symex_assign.
185  const exprt l2_full_lhs = assignment.original_lhs_skeleton.apply(l2_lhs);
187  {
188  INVARIANT(
189  !check_renaming(l2_full_lhs), "l2_full_lhs should be renamed to L2");
190  }
191  state.record_events.pop();
192 
193  auto current_assignment_type =
194  ns.lookup(l2_lhs.get_object_name()).is_auxiliary
196  : assignment_type;
197 
200  l2_lhs,
201  l2_full_lhs,
202  get_original_name(l2_full_lhs),
203  assignment.rhs,
204  state.source,
205  current_assignment_type);
206 
207  const ssa_exprt &l1_lhs = assignment.lhs;
209  {
210  // Split composite symbol lhs into its components
213  // Erase the composite symbol from our working state. Note that we need to
214  // have it in the propagation table and the value set while doing the field
215  // assignments, thus we cannot skip putting it in there above.
216  state.propagation.erase_if_exists(l1_lhs.get_identifier());
217  state.value_set.erase_symbol(l1_lhs, ns);
218  }
219 }
220 
222  const ssa_exprt &lhs, // L1
223  const expr_skeletont &full_lhs,
224  const exprt &rhs,
225  const exprt::operandst &guard)
226 {
227  // Shortcut the common case of a whole-struct initializer:
228  if(rhs.id() == ID_struct)
229  assign_from_struct(lhs, full_lhs, to_struct_expr(rhs), guard);
230  else
231  assign_non_struct_symbol(lhs, full_lhs, rhs, guard);
232 }
233 
235  const typecast_exprt &lhs,
236  const expr_skeletont &full_lhs,
237  const exprt &rhs,
238  exprt::operandst &guard)
239 {
240  // these may come from dereferencing on the lhs
241  exprt rhs_typecasted = typecast_exprt::conditional_cast(rhs, lhs.op().type());
242  expr_skeletont new_skeleton =
243  full_lhs.compose(expr_skeletont::remove_op0(lhs));
244  assign_rec(lhs.op(), new_skeleton, rhs_typecasted, guard);
245 }
246 
247 template <bool use_update>
249  const index_exprt &lhs,
250  const expr_skeletont &full_lhs,
251  const exprt &rhs,
252  exprt::operandst &guard)
253 {
254  const exprt &lhs_array=lhs.array();
255  const exprt &lhs_index=lhs.index();
256  const typet &lhs_index_type = lhs_array.type();
257 
258  PRECONDITION(lhs_index_type.id() == ID_array);
259 
260  if(use_update)
261  {
262  // turn
263  // a[i]=e
264  // into
265  // a'==UPDATE(a, [i], e)
266  const update_exprt new_rhs{lhs_array, index_designatort(lhs_index), rhs};
267  const expr_skeletont new_skeleton =
268  full_lhs.compose(expr_skeletont::remove_op0(lhs));
269  assign_rec(lhs, new_skeleton, new_rhs, guard);
270  }
271  else
272  {
273  // turn
274  // a[i]=e
275  // into
276  // a'==a WITH [i:=e]
277  const with_exprt new_rhs{lhs_array, lhs_index, rhs};
278  const expr_skeletont new_skeleton =
279  full_lhs.compose(expr_skeletont::remove_op0(lhs));
280  assign_rec(lhs_array, new_skeleton, new_rhs, guard);
281  }
282 }
283 
284 template <bool use_update>
286  const member_exprt &lhs,
287  const expr_skeletont &full_lhs,
288  const exprt &rhs,
289  exprt::operandst &guard)
290 {
291  // Symbolic execution of a struct member assignment.
292 
293  // lhs must be member operand, which
294  // takes one operand, which must be a structure.
295 
296  exprt lhs_struct = lhs.op();
297 
298  // typecasts involved? C++ does that for inheritance.
299  if(lhs_struct.id()==ID_typecast)
300  {
301  if(to_typecast_expr(lhs_struct).op().id() == ID_null_object)
302  {
303  // ignore, and give up
304  return;
305  }
306  else
307  {
308  // remove the type cast, we assume that the member is there
309  exprt tmp = to_typecast_expr(lhs_struct).op();
310 
311  if(tmp.type().id() == ID_struct || tmp.type().id() == ID_struct_tag)
312  lhs_struct=tmp;
313  else
314  return; // ignore and give up
315  }
316  }
317 
318  const irep_idt &component_name=lhs.get_component_name();
319 
320  if(use_update)
321  {
322  // turn
323  // a.c=e
324  // into
325  // a'==UPDATE(a, .c, e)
326  const update_exprt new_rhs{
327  lhs_struct, member_designatort(component_name), rhs};
328  const expr_skeletont new_skeleton =
329  full_lhs.compose(expr_skeletont::remove_op0(lhs));
330  assign_rec(lhs_struct, new_skeleton, new_rhs, guard);
331  }
332  else
333  {
334  // turn
335  // a.c=e
336  // into
337  // a'==a WITH [c:=e]
338 
339  with_exprt new_rhs(lhs_struct, exprt(ID_member_name), rhs);
340  new_rhs.where().set(ID_component_name, component_name);
341  const expr_skeletont new_skeleton =
342  full_lhs.compose(expr_skeletont::remove_op0(lhs));
343  assign_rec(lhs_struct, new_skeleton, new_rhs, guard);
344  }
345 }
346 
348  const if_exprt &lhs,
349  const expr_skeletont &full_lhs,
350  const exprt &rhs,
351  exprt::operandst &guard)
352 {
353  // we have (c?a:b)=e;
354 
355  guard.push_back(lhs.cond());
356  assign_rec(lhs.true_case(), full_lhs, rhs, guard);
357  guard.pop_back();
358 
359  guard.push_back(not_exprt(lhs.cond()));
360  assign_rec(lhs.false_case(), full_lhs, rhs, guard);
361  guard.pop_back();
362 }
363 
365  const byte_extract_exprt &lhs,
366  const expr_skeletont &full_lhs,
367  const exprt &rhs,
368  exprt::operandst &guard)
369 {
370  // we have byte_extract_X(object, offset)=value
371  // turn into object=byte_update_X(object, offset, value)
372 
374  if(lhs.id()==ID_byte_extract_little_endian)
375  byte_update_id = ID_byte_update_little_endian;
376  else if(lhs.id()==ID_byte_extract_big_endian)
377  byte_update_id = ID_byte_update_big_endian;
378  else
379  UNREACHABLE;
380 
381  const byte_update_exprt new_rhs{byte_update_id, lhs.op(), lhs.offset(), rhs};
382  const expr_skeletont new_skeleton =
383  full_lhs.compose(expr_skeletont::remove_op0(lhs));
384  assign_rec(lhs.op(), new_skeleton, new_rhs, guard);
385 }
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2258
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:147
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
value_sett::erase_symbol
void erase_symbol(const symbol_exprt &symbol_expr, const namespacet &ns)
Definition: value_set.cpp:1731
make_and
exprt make_and(exprt a, exprt b)
Conjunction of two expressions.
Definition: expr_util.cpp:289
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1874
conjunction
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:34
symex_assign.h
Symbolic Execution of assignments.
byte_update_exprt
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
Definition: byte_operators.h:78
goto_symex_statet::assignment
NODISCARD renamedt< ssa_exprt, L2 > assignment(ssa_exprt lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value, bool allow_pointer_unsoundness=false)
Definition: goto_symex_state.cpp:73
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
typet
The type of an expression, extends irept.
Definition: type.h:28
expr_skeleton.h
Expression skeleton.
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:57
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2237
byte_update_id
static irep_idt byte_update_id()
Definition: byte_operators.cpp:30
symex_assignt::assign_from_struct
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.
Definition: symex_assign.cpp:128
symex_assignt::assign_struct_member
void assign_struct_member(const member_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
Definition: symex_assign.cpp:285
unsupported_operation_exceptiont
Thrown when we encounter an instruction, parameters to an instruction etc.
Definition: exception_utils.h:144
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2172
member_designatort
Definition: std_expr.h:2391
complex_real_exprt
Real part of the expression describing a complex number.
Definition: std_expr.h:1775
exprt
Base class for all expressions.
Definition: expr.h:54
ssa_exprt::get_object_name
irep_idt get_object_name() const
goto_symex_statet::source
symex_targett::sourcet source
Definition: goto_symex_state.h:60
goto_symex_statet::is_read_only_object
static bool is_read_only_object(const exprt &lvalue)
Returns true if lvalue is a read-only object, such as the null object.
Definition: goto_symex_state.h:245
symex_assignt::assign_byte_extract
void assign_byte_extract(const byte_extract_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
Definition: symex_assign.cpp:364
to_complex_type
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1040
field_sensitivityt::apply
NODISCARD exprt apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write) const
Turn an expression expr into a field-sensitive SSA expression.
Definition: field_sensitivity.cpp:33
use_update
constexpr bool use_update()
Definition: symex_assign.cpp:27
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:2209
assignmentt::original_lhs_skeleton
expr_skeletont original_lhs_skeleton
Skeleton to reconstruct the original lhs in the assignment.
Definition: symex_assign.cpp:113
goto_statet::propagation
sharing_mapt< irep_idt, exprt > propagation
Definition: goto_state.h:71
to_complex_real_expr
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition: std_expr.h:1801
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1668
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
byte_operators.h
Expression classes for byte-level operators.
is_ssa_expr
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:125
symex_assignt::assign_typecast
void assign_typecast(const typecast_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
Definition: symex_assign.cpp:234
symex_targett::assignment
virtual void assignment(const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &ssa_full_lhs, const exprt &original_full_lhs, const exprt &ssa_rhs, const sourcet &source, assignment_typet assignment_type)=0
Write to a local variable.
to_ssa_expr
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:145
byte_extract_exprt::op
exprt & op()
Definition: byte_operators.h:43
guard_exprt::as_expr
exprt as_expr() const
Definition: guard_expr.h:46
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:2643
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
goto_statet::guard
guardt guard
Definition: goto_state.h:58
symex_configt::allow_pointer_unsoundness
bool allow_pointer_unsoundness
Definition: symex_config.h:25
assignmentt
Assignment from the rhs value to the lhs variable.
Definition: symex_assign.cpp:110
symex_assignt::assign_if
void assign_if(const if_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
Definition: symex_assign.cpp:347
symex_assignt::assign_array
void assign_array(const index_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
Definition: symex_assign.cpp:248
symex_configt::simplify_opt
bool simplify_opt
Definition: symex_config.h:31
assignmentt::rhs
exprt rhs
Definition: symex_assign.cpp:114
irept::id_string
const std::string & id_string() const
Definition: irep.h:410
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2659
index_exprt::index
exprt & index()
Definition: std_expr.h:1354
index_exprt::array
exprt & array()
Definition: std_expr.h:1344
symex_assignt::assignment_type
symex_targett::assignment_typet assignment_type
Definition: symex_assign.h:60
expr_skeletont::remove_op0
static expr_skeletont remove_op0(exprt e)
Create a skeleton by removing the first operand of e.
Definition: expr_skeleton.cpp:20
get_original_name
exprt get_original_name(exprt expr)
Undo all levels of renaming.
Definition: renaming_level.cpp:157
irept::id
const irep_idt & id() const
Definition: irep.h:407
range.h
Ranges: pair of begin and end iterators, which can be initialized from containers,...
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
complex_exprt
Complex constructor from a pair of numbers.
Definition: std_expr.h:1707
symex_assignt::assign_rec
void assign_rec(const exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
Definition: symex_assign.cpp:36
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:293
symex_assignt::assign_non_struct_symbol
void assign_non_struct_symbol(const ssa_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, const exprt::operandst &guard)
Definition: symex_assign.cpp:150
index_designatort
Definition: std_expr.h:2338
to_complex_imag_expr
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition: std_expr.h:1846
symex_assignt::ns
const namespacet & ns
Definition: symex_assign.h:61
goto_symex_statet::field_sensitivity
field_sensitivityt field_sensitivity
Definition: goto_symex_state.h:120
update_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2442
field_sensitivityt::field_assignments
void field_assignments(const namespacet &ns, goto_symex_statet &state, const ssa_exprt &lhs, symex_targett &target, bool allow_pointer_unsoundness)
Assign to the individual fields of a non-expanded symbol lhs.
Definition: field_sensitivity.cpp:227
byte_extract_exprt::offset
exprt & offset()
Definition: byte_operators.h:44
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2613
expr_util.h
Deprecated expression utility functions.
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2199
goto_symex_state.h
Symbolic Execution.
field_sensitivityt::is_divisible
bool is_divisible(const ssa_exprt &expr) const
Determine whether expr would translate to an atomic SSA expression (returns false) or a composite obj...
Definition: field_sensitivity.cpp:349
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
symex_assignt::symex_config
const symex_configt & symex_config
Definition: symex_assign.h:62
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
symex_configt::constant_propagation
bool constant_propagation
Definition: symex_config.h:27
symex_assignt::target
symex_targett & target
Definition: symex_assign.h:63
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1900
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2189
check_renaming
bool check_renaming(const typet &type)
Check that type is correctly renamed to level 2 and return true in case an error is detected.
Definition: renaming_level.cpp:197
complex_imag_exprt
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:1820
byte_extract_exprt
Expression of type type extracted from some object op starting at position offset (given in number of...
Definition: byte_operators.h:29
expr_skeletont::compose
expr_skeletont compose(expr_skeletont other) const
Replace the missing part of the current skeleton by another skeleton, ending in a bigger skeleton cor...
Definition: expr_skeleton.cpp:51
goto_symex_statet::record_events
std::stack< bool > record_events
Definition: goto_symex_state.h:208
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2697
goto_symex_statet::rename
NODISCARD renamedt< exprt, level > rename(exprt expr, const namespacet &ns)
Rewrites symbol expressions in exprt, applying a suffix to each symbol reflecting its most recent ver...
symex_assignt::state
goto_symex_statet & state
Definition: symex_assign.h:59
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:2627
exprt::operands
operandst & operands()
Definition: expr.h:92
symex_targett::assignment_typet::HIDDEN
@ HIDDEN
index_exprt
Array index operator.
Definition: std_expr.h:1328
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
symex_configt::run_validation_checks
bool run_validation_checks
Should the additional validation checks be run? If this flag is set the checks for renaming (both lev...
Definition: symex_config.h:44
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1866
assignmentt::lhs
ssa_exprt lhs
Definition: symex_assign.cpp:111
with_exprt::where
exprt & where()
Definition: std_expr.h:2278
goto_statet::value_set
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
Definition: goto_state.h:51
make_range
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
expr_skeletont
Expression in which some part is missing and can be substituted for another expression.
Definition: expr_skeleton.h:26
to_struct_expr
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1691
symex_config.h
Symbolic Execution.
symex_assignt::assign_symbol
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}...
Definition: symex_assign.cpp:221
not_exprt
Boolean negation.
Definition: std_expr.h:2127