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.h"
16 #include "goto_symex_state.h"
17 #include <util/byte_operators.h>
18 #include <util/expr_util.h>
19 #include <util/format_expr.h>
20 
21 // We can either use with_exprt or update_exprt when building expressions that
22 // modify components of an array or a struct. Set USE_UPDATE to use
23 // update_exprt.
24 // #define USE_UPDATE
25 
26 constexpr bool use_update()
27 {
28 #ifdef USE_UPDATE
29  return true;
30 #else
31  return false;
32 #endif
33 }
34 
36  const exprt &lhs,
37  const expr_skeletont &full_lhs,
38  const exprt &rhs,
39  exprt::operandst &guard)
40 {
41  if(lhs.id() == ID_symbol && lhs.get_bool(ID_C_SSA_symbol))
42  {
43  assign_symbol(to_ssa_expr(lhs), full_lhs, rhs, guard);
44  }
45  else if(lhs.id() == ID_index)
46  assign_array<use_update()>(to_index_expr(lhs), full_lhs, rhs, guard);
47  else if(lhs.id()==ID_member)
48  {
49  const typet &type = to_member_expr(lhs).struct_op().type();
50  if(type.id() == ID_struct || type.id() == ID_struct_tag)
51  {
52  assign_struct_member<use_update()>(
53  to_member_expr(lhs), full_lhs, rhs, guard);
54  }
55  else if(type.id() == ID_union || type.id() == ID_union_tag)
56  {
57  // should have been replaced by byte_extract
59  "assign_rec: unexpected assignment to union member");
60  }
61  else
63  "assign_rec: unexpected assignment to member of '" + type.id_string() +
64  "'");
65  }
66  else if(lhs.id()==ID_if)
67  assign_if(to_if_expr(lhs), full_lhs, rhs, guard);
68  else if(lhs.id()==ID_typecast)
69  assign_typecast(to_typecast_expr(lhs), full_lhs, rhs, guard);
71  {
72  // ignore
73  }
74  else if(lhs.id()==ID_byte_extract_little_endian ||
75  lhs.id()==ID_byte_extract_big_endian)
76  {
77  assign_byte_extract(to_byte_extract_expr(lhs), full_lhs, rhs, guard);
78  }
79  else if(lhs.id() == ID_complex_real)
80  {
81  // this is stuff like __real__ x = 1;
82  const complex_real_exprt &complex_real_expr = to_complex_real_expr(lhs);
83 
84  const complex_imag_exprt complex_imag_expr(complex_real_expr.op());
85 
86  complex_exprt new_rhs(
87  rhs, complex_imag_expr, to_complex_type(complex_real_expr.op().type()));
88 
89  assign_rec(complex_real_expr.op(), full_lhs, new_rhs, guard);
90  }
91  else if(lhs.id() == ID_complex_imag)
92  {
93  const complex_imag_exprt &complex_imag_expr = to_complex_imag_expr(lhs);
94 
95  const complex_real_exprt complex_real_expr(complex_imag_expr.op());
96 
97  complex_exprt new_rhs(
98  complex_real_expr, rhs, to_complex_type(complex_imag_expr.op().type()));
99 
100  assign_rec(complex_imag_expr.op(), full_lhs, new_rhs, guard);
101  }
102  else
104  "assignment to '" + lhs.id_string() + "' not handled");
105 }
106 
108 struct assignmentt final
109 {
114 };
115 
128  const ssa_exprt &lhs, // L1
129  const expr_skeletont &full_lhs,
130  const struct_exprt &rhs,
131  const exprt::operandst &guard)
132 {
133  const auto &components = to_struct_type(ns.follow(lhs.type())).components();
134  PRECONDITION(rhs.operands().size() == components.size());
135 
136  for(const auto &comp_rhs : make_range(components).zip(rhs.operands()))
137  {
138  const auto &comp = comp_rhs.first;
139  const exprt lhs_field = state.field_sensitivity.apply(
140  ns, state, member_exprt{lhs, comp.get_name(), comp.type()}, true);
141  INVARIANT(
142  lhs_field.id() == ID_symbol,
143  "member of symbol should be susceptible to field-sensitivity");
144 
145  assign_symbol(to_ssa_expr(lhs_field), full_lhs, comp_rhs.second, guard);
146  }
147 }
148 
150  const ssa_exprt &lhs, // L1
151  const expr_skeletont &full_lhs,
152  const exprt &rhs,
153  const exprt::operandst &guard)
154 {
155  exprt l2_rhs =
156  state
157  .rename(
158  // put assignment guard into the rhs
159  guard.empty()
160  ? rhs
161  : static_cast<exprt>(if_exprt{conjunction(guard), rhs, lhs}),
162  ns)
163  .get();
164 
165  assignmentt assignment{lhs, full_lhs, l2_rhs};
166 
168  assignment.rhs = simplify_expr(std::move(assignment.rhs), ns);
169 
170  const ssa_exprt l2_lhs = state
171  .assignment(
172  assignment.lhs,
173  assignment.rhs,
174  ns,
178  .get();
179 
180  state.record_events.push(false);
181  // Note any other symbols mentioned in the skeleton are rvalues -- for example
182  // array indices -- and were renamed to L2 at the start of
183  // goto_symext::symex_assign.
184  const exprt l2_full_lhs = assignment.original_lhs_skeleton.apply(l2_lhs);
186  {
187  INVARIANT(
188  !check_renaming(l2_full_lhs), "l2_full_lhs should be renamed to L2");
189  }
190  state.record_events.pop();
191 
192  auto current_assignment_type =
193  ns.lookup(l2_lhs.get_object_name()).is_auxiliary
195  : assignment_type;
196 
199  l2_lhs,
200  l2_full_lhs,
201  get_original_name(l2_full_lhs),
202  assignment.rhs,
203  state.source,
204  current_assignment_type);
205 
206  const ssa_exprt &l1_lhs = assignment.lhs;
208  {
209  // Split composite symbol lhs into its components
212  // Erase the composite symbol from our working state. Note that we need to
213  // have it in the propagation table and the value set while doing the field
214  // assignments, thus we cannot skip putting it in there above.
215  state.propagation.erase_if_exists(l1_lhs.get_identifier());
216  state.value_set.erase_symbol(l1_lhs, ns);
217  }
218 }
219 
221  const ssa_exprt &lhs, // L1
222  const expr_skeletont &full_lhs,
223  const exprt &rhs,
224  const exprt::operandst &guard)
225 {
226  // Shortcut the common case of a whole-struct initializer:
227  if(rhs.id() == ID_struct)
228  assign_from_struct(lhs, full_lhs, to_struct_expr(rhs), guard);
229  else
230  assign_non_struct_symbol(lhs, full_lhs, rhs, guard);
231 }
232 
234  const typecast_exprt &lhs,
235  const expr_skeletont &full_lhs,
236  const exprt &rhs,
237  exprt::operandst &guard)
238 {
239  // these may come from dereferencing on the lhs
240  exprt rhs_typecasted = typecast_exprt::conditional_cast(rhs, lhs.op().type());
241  expr_skeletont new_skeleton =
242  full_lhs.compose(expr_skeletont::remove_op0(lhs));
243  assign_rec(lhs.op(), new_skeleton, rhs_typecasted, guard);
244 }
245 
246 template <bool use_update>
248  const index_exprt &lhs,
249  const expr_skeletont &full_lhs,
250  const exprt &rhs,
251  exprt::operandst &guard)
252 {
253  const exprt &lhs_array=lhs.array();
254  const exprt &lhs_index=lhs.index();
255  const typet &lhs_index_type = lhs_array.type();
256 
257  PRECONDITION(lhs_index_type.id() == ID_array);
258 
259  if(use_update)
260  {
261  // turn
262  // a[i]=e
263  // into
264  // a'==UPDATE(a, [i], e)
265  const update_exprt new_rhs{lhs_array, index_designatort(lhs_index), rhs};
266  const expr_skeletont new_skeleton =
267  full_lhs.compose(expr_skeletont::remove_op0(lhs));
268  assign_rec(lhs, new_skeleton, new_rhs, guard);
269  }
270  else
271  {
272  // turn
273  // a[i]=e
274  // into
275  // a'==a WITH [i:=e]
276  const with_exprt new_rhs{lhs_array, lhs_index, rhs};
277  const expr_skeletont new_skeleton =
278  full_lhs.compose(expr_skeletont::remove_op0(lhs));
279  assign_rec(lhs_array, new_skeleton, new_rhs, guard);
280  }
281 }
282 
283 template <bool use_update>
285  const member_exprt &lhs,
286  const expr_skeletont &full_lhs,
287  const exprt &rhs,
288  exprt::operandst &guard)
289 {
290  // Symbolic execution of a struct member assignment.
291 
292  // lhs must be member operand, which
293  // takes one operand, which must be a structure.
294 
295  exprt lhs_struct = lhs.op();
296 
297  // typecasts involved? C++ does that for inheritance.
298  if(lhs_struct.id()==ID_typecast)
299  {
300  if(to_typecast_expr(lhs_struct).op().id() == ID_null_object)
301  {
302  // ignore, and give up
303  return;
304  }
305  else
306  {
307  // remove the type cast, we assume that the member is there
308  exprt tmp = to_typecast_expr(lhs_struct).op();
309 
310  if(tmp.type().id() == ID_struct || tmp.type().id() == ID_struct_tag)
311  lhs_struct=tmp;
312  else
313  return; // ignore and give up
314  }
315  }
316 
317  const irep_idt &component_name=lhs.get_component_name();
318 
319  if(use_update)
320  {
321  // turn
322  // a.c=e
323  // into
324  // a'==UPDATE(a, .c, e)
325  const update_exprt new_rhs{
326  lhs_struct, member_designatort(component_name), rhs};
327  const expr_skeletont new_skeleton =
328  full_lhs.compose(expr_skeletont::remove_op0(lhs));
329  assign_rec(lhs_struct, new_skeleton, new_rhs, guard);
330  }
331  else
332  {
333  // turn
334  // a.c=e
335  // into
336  // a'==a WITH [c:=e]
337 
338  with_exprt new_rhs(lhs_struct, exprt(ID_member_name), rhs);
339  new_rhs.where().set(ID_component_name, component_name);
340  const expr_skeletont new_skeleton =
341  full_lhs.compose(expr_skeletont::remove_op0(lhs));
342  assign_rec(lhs_struct, new_skeleton, new_rhs, guard);
343  }
344 }
345 
347  const if_exprt &lhs,
348  const expr_skeletont &full_lhs,
349  const exprt &rhs,
350  exprt::operandst &guard)
351 {
352  // we have (c?a:b)=e;
353 
354  guard.push_back(lhs.cond());
355  assign_rec(lhs.true_case(), full_lhs, rhs, guard);
356  guard.pop_back();
357 
358  guard.push_back(not_exprt(lhs.cond()));
359  assign_rec(lhs.false_case(), full_lhs, rhs, guard);
360  guard.pop_back();
361 }
362 
364  const byte_extract_exprt &lhs,
365  const expr_skeletont &full_lhs,
366  const exprt &rhs,
367  exprt::operandst &guard)
368 {
369  // we have byte_extract_X(object, offset)=value
370  // turn into object=byte_update_X(object, offset, value)
371 
373  if(lhs.id()==ID_byte_extract_little_endian)
374  byte_update_id = ID_byte_update_little_endian;
375  else if(lhs.id()==ID_byte_extract_big_endian)
376  byte_update_id = ID_byte_update_big_endian;
377  else
378  UNREACHABLE;
379 
380  const byte_update_exprt new_rhs{byte_update_id, lhs.op(), lhs.offset(), rhs};
381  const expr_skeletont new_skeleton =
382  full_lhs.compose(expr_skeletont::remove_op0(lhs));
383  assign_rec(lhs.op(), new_skeleton, new_rhs, guard);
384 }
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3050
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
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:1749
make_and
exprt make_and(exprt a, exprt b)
Conjunction of two expressions.
Definition: expr_util.cpp:291
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2021
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:51
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:81
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:76
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
typet
The type of an expression, extends irept.
Definition: type.h:29
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:1347
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3029
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:127
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:284
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:2964
member_designatort
Definition: std_expr.h:3183
complex_real_exprt
Real part of the expression describing a complex number.
Definition: std_expr.h:1740
exprt
Base class for all expressions.
Definition: expr.h:53
ssa_exprt::get_object_name
irep_idt get_object_name() const
goto_symex_statet::source
symex_targett::sourcet source
Definition: goto_symex_state.h:64
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:249
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:363
to_complex_type
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1815
byte_update_id
irep_idt byte_update_id()
Definition: byte_operators.cpp:30
field_sensitivityt::apply
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:21
use_update
constexpr bool use_update()
Definition: symex_assign.cpp:26
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3001
assignmentt::original_lhs_skeleton
expr_skeletont original_lhs_skeleton
Skeleton to reconstruct the original lhs in the assignment.
Definition: symex_assign.cpp:112
goto_statet::propagation
sharing_mapt< irep_idt, exprt > propagation
Definition: goto_state.h:63
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:1766
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1633
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:81
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
byte_operators.h
Expression classes for byte-level operators.
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:233
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:148
byte_extract_exprt::op
exprt & op()
Definition: byte_operators.h:43
guard_exprt::as_expr
exprt as_expr() const
Definition: guard_expr.h:49
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:3435
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
goto_symex.h
Symbolic Execution.
goto_statet::guard
guardt guard
Definition: goto_state.h:50
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:109
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:346
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:247
symex_configt::simplify_opt
bool simplify_opt
Definition: symex_config.h:31
assignmentt::rhs
exprt rhs
Definition: symex_assign.cpp:113
irept::id_string
const std::string & id_string() const
Definition: irep.h:421
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2698
index_exprt::index
exprt & index()
Definition: std_expr.h:1319
index_exprt::array
exprt & array()
Definition: std_expr.h:1309
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:169
irept::id
const irep_idt & id() const
Definition: irep.h:418
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
complex_exprt
Complex constructor from a pair of numbers.
Definition: std_expr.h:1672
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:35
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
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:149
index_designatort
Definition: std_expr.h:3130
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:1811
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:124
update_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3234
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:219
byte_extract_exprt::offset
exprt & offset()
Definition: byte_operators.h:44
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
expr_util.h
Deprecated expression utility functions.
format_expr.h
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2991
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:341
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
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:442
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:2047
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2981
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:209
complex_imag_exprt
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:1785
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:212
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3489
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:3419
exprt::operands
operandst & operands()
Definition: expr.h:95
symex_targett::assignment_typet::HIDDEN
@ HIDDEN
index_exprt
Array index operator.
Definition: std_expr.h:1293
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:2013
assignmentt::lhs
ssa_exprt lhs
Definition: symex_assign.cpp:110
with_exprt::where
exprt & where()
Definition: std_expr.h:3070
goto_statet::value_set
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
Definition: goto_state.h:43
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:1656
validation_modet::INVARIANT
@ INVARIANT
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:220
not_exprt
Boolean negation.
Definition: std_expr.h:2843