cprover
symex_function_call.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution of ANSI-C
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "goto_symex.h"
13 
14 #include <util/arith_tools.h>
15 #include <util/base_type.h>
16 #include <util/byte_operators.h>
17 #include <util/c_types.h>
18 #include <util/exception_utils.h>
19 #include <util/invariant.h>
20 
22  const irep_idt &,
23  const unsigned,
24  unsigned)
25 {
26  return false;
27 }
28 
30  const irep_idt &function_identifier,
31  const goto_functionst::goto_functiont &goto_function,
32  statet &state,
33  const exprt::operandst &arguments)
34 {
35  const code_typet &function_type=goto_function.type;
36 
37  // iterates over the arguments
38  exprt::operandst::const_iterator it1=arguments.begin();
39 
40  // these are the types of the parameters
41  const code_typet::parameterst &parameter_types=
42  function_type.parameters();
43 
44  // iterates over the types of the parameters
45  for(code_typet::parameterst::const_iterator
46  it2=parameter_types.begin();
47  it2!=parameter_types.end();
48  it2++)
49  {
50  const code_typet::parametert &parameter=*it2;
51 
52  // this is the type that the n-th argument should have
53  const typet &parameter_type=parameter.type();
54 
55  const irep_idt &identifier=parameter.get_identifier();
56 
57  INVARIANT(
58  !identifier.empty(),
59  "function pointer parameter must have an identifier");
60 
61  const symbolt &symbol=ns.lookup(identifier);
62  symbol_exprt lhs=symbol.symbol_expr();
63 
64  exprt rhs;
65 
66  // if you run out of actual arguments there was a mismatch
67  if(it1==arguments.end())
68  {
69  log.warning() << state.source.pc->source_location.as_string()
70  << ": "
71  "call to `"
72  << id2string(function_identifier)
73  << "': "
74  "not enough arguments, inserting non-deterministic value"
75  << log.eom;
76 
78  parameter_type, state.source.pc->source_location);
79  }
80  else
81  rhs=*it1;
82 
83  if(rhs.is_nil())
84  {
85  // 'nil' argument doesn't get assigned
86  }
87  else
88  {
89  // It should be the same exact type.
90  if(!base_type_eq(parameter_type, rhs.type(), ns))
91  {
92  const typet &f_parameter_type=ns.follow(parameter_type);
93  const typet &f_rhs_type=ns.follow(rhs.type());
94 
95  // But we are willing to do some limited conversion.
96  // This is highly dubious, obviously.
97  if((f_parameter_type.id()==ID_signedbv ||
98  f_parameter_type.id()==ID_unsignedbv ||
99  f_parameter_type.id()==ID_c_enum_tag ||
100  f_parameter_type.id()==ID_bool ||
101  f_parameter_type.id()==ID_pointer ||
102  f_parameter_type.id()==ID_union) &&
103  (f_rhs_type.id()==ID_signedbv ||
104  f_rhs_type.id()==ID_unsignedbv ||
105  f_rhs_type.id()==ID_c_bit_field ||
106  f_rhs_type.id()==ID_c_enum_tag ||
107  f_rhs_type.id()==ID_bool ||
108  f_rhs_type.id()==ID_pointer ||
109  f_rhs_type.id()==ID_union))
110  {
111  rhs=
113  byte_extract_id(),
114  rhs,
115  from_integer(0, index_type()),
116  parameter_type);
117  }
118  else
119  {
120  std::ostringstream error;
121  error << "function call: parameter \"" << identifier
122  << "\" type mismatch: got " << rhs.type().pretty()
123  << ", expected " << parameter_type.pretty();
124  throw unsupported_operation_exceptiont(error.str());
125  }
126  }
127 
128  assignment_typet assignment_type;
129 
130  // We hide if we are in a hidden function.
131  if(state.top().hidden_function)
132  assignment_type =
134  else
135  assignment_type =
137 
138  clean_expr(lhs, state, true);
139  clean_expr(rhs, state, false);
140 
141  guardt guard;
142  symex_assign_rec(state, lhs, nil_exprt(), rhs, guard, assignment_type);
143  }
144 
145  if(it1!=arguments.end())
146  it1++;
147  }
148 
149  if(function_type.has_ellipsis())
150  {
151  // These are va_arg arguments; their types may differ from call to call
152  std::size_t va_count=0;
153  const symbolt *va_sym=nullptr;
154  while(!ns.lookup(
155  id2string(function_identifier)+"::va_arg"+std::to_string(va_count),
156  va_sym))
157  ++va_count;
158 
159  for( ; it1!=arguments.end(); it1++, va_count++)
160  {
161  irep_idt id=
162  id2string(function_identifier)+"::va_arg"+std::to_string(va_count);
163 
164  // add to symbol table
165  symbolt symbol;
166  symbol.name=id;
167  symbol.base_name="va_arg"+std::to_string(va_count);
168  symbol.mode=ID_C;
169  symbol.type=it1->type();
170 
171  state.symbol_table.insert(std::move(symbol));
172 
173  symbol_exprt lhs=symbol_exprt(id, it1->type());
174 
175  symex_assign(state, code_assignt(lhs, *it1));
176  }
177  }
178  else if(it1!=arguments.end())
179  {
180  // we got too many arguments, but we will just ignore them
181  }
182 }
183 
185  const get_goto_functiont &get_goto_function,
186  statet &state,
187  const code_function_callt &code)
188 {
189  const exprt &function=code.function();
190 
191  // If at some point symex_function_call can support more
192  // expression ids(), like ID_Dereference, please expand the
193  // precondition appropriately.
194  PRECONDITION(function.id() == ID_symbol);
195  symex_function_call_symbol(get_goto_function, state, code);
196 }
197 
199  const get_goto_functiont &get_goto_function,
200  statet &state,
201  const code_function_callt &code)
202 {
203  target.location(state.guard.as_expr(), state.source);
204 
205  PRECONDITION(code.function().id() == ID_symbol);
206 
207  const irep_idt &identifier=
208  to_symbol_expr(code.function()).get_identifier();
209 
210  if(identifier=="CBMC_trace")
211  {
212  symex_trace(state, code);
213  }
214  else if(has_prefix(id2string(identifier), CPROVER_FKT_PREFIX))
215  {
216  symex_fkt(state, code);
217  }
218  else if(has_prefix(id2string(identifier), CPROVER_MACRO_PREFIX))
219  {
220  symex_macro(state, code);
221  }
222  else
223  symex_function_call_code(get_goto_function, state, code);
224 }
225 
228  const get_goto_functiont &get_goto_function,
229  statet &state,
230  const code_function_callt &call)
231 {
232  const irep_idt &identifier=
233  to_symbol_expr(call.function()).get_identifier();
234 
235  const goto_functionst::goto_functiont &goto_function =
236  get_goto_function(identifier);
237 
238  state.dirty.populate_dirty_for_function(identifier, goto_function);
239 
240  auto emplace_safe_pointers_result =
241  state.safe_pointers.emplace(identifier, local_safe_pointerst{ns});
242  if(emplace_safe_pointers_result.second)
243  emplace_safe_pointers_result.first->second(goto_function.body);
244 
245  const bool stop_recursing=get_unwind_recursion(
246  identifier,
247  state.source.thread_nr,
248  state.top().loop_iterations[identifier].count);
249 
250  // see if it's too much
251  if(stop_recursing)
252  {
254  {
255  // it's ok, ignore
256  }
257  else
258  {
260  vcc(false_exprt(), "recursion unwinding assertion", state);
261 
262  // add to state guard to prevent further assignments
263  state.guard.add(false_exprt());
264  }
265 
266  symex_transition(state);
267  return;
268  }
269 
270  // read the arguments -- before the locality renaming
271  exprt::operandst arguments = call.arguments();
272  for(auto &a : arguments)
273  state.rename(a, ns);
274 
275  // we hide the call if the caller and callee are both hidden
276  const bool hidden = state.top().hidden_function && goto_function.is_hidden();
277 
278  // record the call
280  state.guard.as_expr(), identifier, arguments, state.source, hidden);
281 
282  if(!goto_function.body_available())
283  {
284  no_body(identifier);
285 
286  // record the return
287  target.function_return(state.guard.as_expr(), state.source, hidden);
288 
289  if(call.lhs().is_not_nil())
290  {
291  const auto rhs =
293  code_assignt code(call.lhs(), rhs);
294  symex_assign(state, code);
295  }
296 
297  symex_transition(state);
298  return;
299  }
300 
301  // produce a new frame
302  PRECONDITION(!state.call_stack().empty());
303  goto_symex_statet::framet &frame=state.new_frame();
304 
305  // preserve locality of local variables
306  locality(identifier, state, goto_function);
307 
308  // assign actuals to formal parameters
309  parameter_assignments(identifier, goto_function, state, arguments);
310 
311  frame.end_of_function=--goto_function.body.instructions.end();
312  frame.return_value=call.lhs();
313  frame.calling_location=state.source;
314  frame.function_identifier=identifier;
315  frame.hidden_function=goto_function.is_hidden();
316 
317  const goto_symex_statet::framet &p_frame=state.previous_frame();
318  for(const auto &pair : p_frame.loop_iterations)
319  {
320  if(pair.second.is_recursion)
321  frame.loop_iterations.insert(pair);
322  }
323 
324  // increase unwinding counter
325  frame.loop_iterations[identifier].is_recursion=true;
326  frame.loop_iterations[identifier].count++;
327 
328  state.source.is_set=true;
329  state.source.function = identifier;
330  symex_transition(state, goto_function.body.instructions.begin(), false);
331 }
332 
335 {
336  PRECONDITION(!state.call_stack().empty());
337 
338  {
339  statet::framet &frame=state.top();
340 
341  // restore program counter
342  symex_transition(state, frame.calling_location.pc, false);
344 
345  // restore L1 renaming
346  state.level1.restore_from(frame.old_level1);
347 
348  // clear function-locals from L2 renaming
349  for(auto c_it = state.level2.current_names.begin();
350  c_it != state.level2.current_names.end();) // no ++c_it
351  {
352  const irep_idt l1_o_id=c_it->second.first.get_l1_object_identifier();
353  // could use iteration over local_objects as l1_o_id is prefix
354  if(
355  frame.local_objects.find(l1_o_id) == frame.local_objects.end() ||
356  (state.threads.size() > 1 &&
357  state.dirty(c_it->second.first.get_object_name())))
358  {
359  ++c_it;
360  continue;
361  }
362  auto cur = c_it;
363  ++c_it;
364  state.level2.current_names.erase(cur);
365  }
366  }
367 
368  state.pop_frame();
369 }
370 
373 {
374  const bool hidden = state.top().hidden_function;
375 
376  // first record the return
377  target.function_return(state.guard.as_expr(), state.source, hidden);
378 
379  // then get rid of the frame
380  pop_frame(state);
381 }
382 
386  const irep_idt &function_identifier,
387  statet &state,
388  const goto_functionst::goto_functiont &goto_function)
389 {
390  unsigned &frame_nr=
391  state.threads[state.source.thread_nr].function_frame[function_identifier];
392  frame_nr++;
393 
394  std::set<irep_idt> local_identifiers;
395 
396  get_local_identifiers(goto_function, local_identifiers);
397 
398  statet::framet &frame=state.top();
399 
400  for(std::set<irep_idt>::const_iterator
401  it=local_identifiers.begin();
402  it!=local_identifiers.end();
403  it++)
404  {
405  // get L0 name
406  ssa_exprt ssa(ns.lookup(*it).symbol_expr());
407  state.rename(ssa, ns, goto_symex_statet::L0);
408  const irep_idt l0_name=ssa.get_identifier();
409 
410  // save old L1 name for popping the frame
411  auto c_it = state.level1.current_names.find(l0_name);
412 
413  if(c_it != state.level1.current_names.end())
414  {
415  frame.old_level1[l0_name]=c_it->second;
416  c_it->second = std::make_pair(ssa, frame_nr);
417  }
418  else
419  {
420  c_it = state.level1.current_names
421  .emplace(l0_name, std::make_pair(ssa, frame_nr))
422  .first;
423  }
424 
425  // do L1 renaming -- these need not be unique, as
426  // identifiers may be shared among functions
427  // (e.g., due to inlining or other code restructuring)
428 
429  state.rename(ssa, ns, goto_symex_statet::L1);
430 
431  irep_idt l1_name=ssa.get_identifier();
432  unsigned offset=0;
433 
434  while(state.l1_history.find(l1_name)!=state.l1_history.end())
435  {
437  ++offset;
438  ssa.set_level_1(frame_nr+offset);
439  l1_name=ssa.get_identifier();
440  }
441 
442  // now unique -- store
443  frame.local_objects.insert(l1_name);
444  state.l1_history.insert(l1_name);
445  }
446 }
447 
449 {
450  statet::framet &frame=state.top();
451 
452  const goto_programt::instructiont &instruction=*state.source.pc;
453  PRECONDITION(instruction.is_return());
454  const code_returnt &code=to_code_return(instruction.code);
455 
456  target.location(state.guard.as_expr(), state.source);
457 
458  PRECONDITION(code.operands().size() == 1 || frame.return_value.is_nil());
459 
460  exprt value = code.return_value();
461 
462  if(frame.return_value.is_not_nil())
463  {
464  code_assignt assignment(frame.return_value, value);
465 
466  INVARIANT(
467  base_type_eq(assignment.lhs().type(), assignment.rhs().type(), ns),
468  "goto_symext::return_assignment type mismatch");
469 
470  symex_assign(state, assignment);
471  }
472 }
exception_utils.h
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
symex_targett::assignment_typet
assignment_typet
Definition: symex_target.h:64
code_typet::has_ellipsis
bool has_ellipsis() const
Definition: std_types.h:849
symex_targett::sourcet::is_set
bool is_set
Definition: symex_target.h:42
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
CPROVER_FKT_PREFIX
#define CPROVER_FKT_PREFIX
Definition: cprover_prefix.h:16
symex_configt::partial_loops
bool partial_loops
Definition: goto_symex.h:61
goto_symext::symex_function_call_code
virtual void symex_function_call_code(const get_goto_functiont &, statet &, const code_function_callt &)
do function call by inlining
Definition: symex_function_call.cpp:227
goto_symex_statet::guard
guardt guard
Definition: goto_symex_state.h:57
goto_symext::symex_assign
void symex_assign(statet &, const code_assignt &)
Definition: symex_assign.cpp:24
goto_symex_statet::level1
symex_level1t level1
Definition: goto_symex_state.h:65
arith_tools.h
goto_symex_statet::framet::old_level1
symex_renaming_levelt::current_namest old_level1
Definition: goto_symex_state.h:185
typet
The type of an expression, extends irept.
Definition: type.h:27
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:274
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:754
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:640
symex_targett::sourcet::pc
goto_programt::const_targett pc
Definition: symex_target.h:41
goto_symext::target
symex_target_equationt & target
Definition: goto_symex.h:216
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
goto_symex_statet
Definition: goto_symex_state.h:34
unsupported_operation_exceptiont
Thrown when we encounter an instruction, parameters to an instruction etc.
Definition: exception_utils.h:143
guardt::add
void add(const exprt &expr)
Definition: guard.cpp:43
local_safe_pointerst
A very simple, cheap analysis to determine when dereference operations are trivially guarded by a che...
Definition: local_safe_pointers.h:24
goto_symext::clean_expr
void clean_expr(exprt &, statet &, bool write)
Definition: symex_clean_expr.cpp:154
symex_targett::sourcet::thread_nr
unsigned thread_nr
Definition: symex_target.h:37
goto_symex_statet::L1
Definition: goto_symex_state.h:72
goto_symex_statet::framet::calling_location
symex_targett::sourcet calling_location
Definition: goto_symex_state.h:179
goto_symex_statet::rename
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
Definition: goto_symex_state.cpp:273
goto_symext::symex_macro
virtual void symex_macro(statet &, const code_function_callt &)
Definition: symex_builtin_functions.cpp:517
exprt
Base class for all expressions.
Definition: expr.h:54
goto_symex_statet::source
symex_targett::sourcet source
Definition: goto_symex_state.h:58
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
goto_symex_statet::l1_history
std::set< irep_idt > l1_history
Definition: goto_symex_state.h:62
invariant.h
symex_renaming_levelt::increase_counter
static void increase_counter(const current_namest::iterator &it)
Increase the counter corresponding to an identifier.
Definition: renaming_level.h:41
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:53
goto_symext::no_body
virtual void no_body(const irep_idt &)
Definition: goto_symex.h:300
messaget::eom
static eomt eom
Definition: message.h:284
goto_symex_statet::framet::loop_iterations
std::unordered_map< irep_idt, loop_infot > loop_iterations
Definition: goto_symex_state.h:198
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
goto_symex_statet::framet::local_objects
std::set< irep_idt > local_objects
Definition: goto_symex_state.h:187
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1089
goto_symext::get_unwind_recursion
virtual bool get_unwind_recursion(const irep_idt &identifier, unsigned thread_nr, unsigned unwind)
Definition: symex_function_call.cpp:21
goto_symex_statet::safe_pointers
std::unordered_map< irep_idt, local_safe_pointerst > safe_pointers
Definition: goto_symex_state.h:105
goto_symext::symex_trace
virtual void symex_trace(statet &, const code_function_callt &)
Definition: symex_builtin_functions.cpp:456
goto_symex_statet::new_frame
framet & new_frame()
Definition: goto_symex_state.h:227
symex_targett::assignment_typet::VISIBLE_ACTUAL_PARAMETER
goto_symext::log
messaget log
Definition: goto_symex.h:219
symex_target_equationt::location
virtual void location(const exprt &guard, const sourcet &source)
Record a location.
Definition: symex_target_equation.cpp:191
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
CPROVER_MACRO_PREFIX
#define CPROVER_MACRO_PREFIX
Definition: cprover_prefix.h:18
byte_extract_id
irep_idt byte_extract_id()
Definition: byte_operators.cpp:13
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
guardt
Definition: guard.h:19
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1036
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:173
goto_symex_statet::dirty
incremental_dirtyt dirty
Definition: goto_symex_state.h:258
goto_symex_statet::threads
std::vector< threadt > threads
Definition: goto_symex_state.h:252
byte_operators.h
Expression classes for byte-level operators.
goto_symex_statet::call_stack
call_stackt & call_stack()
Definition: goto_symex_state.h:203
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
goto_symex_statet::L0
Definition: goto_symex_state.h:72
base_type.h
symex_target_equationt::function_call
virtual void function_call(const exprt &guard, const irep_idt &function_identifier, const std::vector< exprt > &ssa_function_arguments, const sourcet &source, bool hidden)
Record a function call.
Definition: symex_target_equation.cpp:205
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
goto_symex_statet::symbol_table
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc.
Definition: goto_symex_state.h:52
symex_targett::assignment_typet::HIDDEN_ACTUAL_PARAMETER
goto_programt::instructiont::code
codet code
Definition: goto_program.h:181
goto_symex_statet::top
framet & top()
Definition: goto_symex_state.h:215
base_type_eq
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Definition: base_type.cpp:332
nil_exprt
The NIL expression.
Definition: std_expr.h:4461
symex_configt::unwinding_assertions
bool unwinding_assertions
Definition: goto_symex.h:60
incremental_dirtyt::populate_dirty_for_function
void populate_dirty_for_function(const irep_idt &id, const goto_functionst::goto_functiont &function)
Analyse the given function with dirtyt if it hasn't been seen before.
Definition: dirty.cpp:80
goto_symex.h
goto_symext::return_assignment
void return_assignment(statet &)
Definition: symex_function_call.cpp:448
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:269
goto_symex_statet::framet::hidden_function
bool hidden_function
Definition: goto_symex_state.h:183
goto_symext::symex_end_of_function
virtual void symex_end_of_function(statet &)
do function call by inlining
Definition: symex_function_call.cpp:372
goto_symext::symex_function_call
virtual void symex_function_call(const get_goto_functiont &, statet &, const code_function_callt &)
Definition: symex_function_call.cpp:184
symbol_tablet::insert
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Definition: symbol_table.cpp:17
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
code_typet
Base type of functions.
Definition: std_types.h:751
irept::is_nil
bool is_nil() const
Definition: irep.h:172
irept::id
const irep_idt & id() const
Definition: irep.h:259
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
dstringt::empty
bool empty() const
Definition: dstring.h:75
to_code_return
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:1238
false_exprt
The Boolean constant false.
Definition: std_expr.h:4452
get_local_identifiers
void get_local_identifiers(const goto_functiont &goto_function, std::set< irep_idt > &dest)
Return in dest the identifiers of the local variables declared in the goto_function and the identifie...
Definition: goto_function.cpp:18
goto_symext::pop_frame
void pop_frame(statet &)
pop one call frame
Definition: symex_function_call.cpp:334
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:893
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1109
symex_transition
void symex_transition(goto_symext::statet &state)
Definition: symex_main.cpp:66
goto_symext::symex_assign_rec
void symex_assign_rec(statet &, const exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
Definition: symex_assign.cpp:131
goto_symext::locality
void locality(const irep_idt &function_identifier, statet &, const goto_functionst::goto_functiont &)
preserves locality of local variables of a given function by applying L1 renaming to the local identi...
Definition: symex_function_call.cpp:385
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1633
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
goto_symext::ns
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:215
symex_targett::sourcet::function
irep_idt function
Definition: symex_target.h:38
goto_symex_statet::framet
Definition: goto_symex_state.h:174
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1191
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
symbolt
Symbol table entry.
Definition: symbol.h:27
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
goto_symex_statet::pop_frame
void pop_frame()
Definition: goto_symex_state.h:228
goto_symext::vcc
virtual void vcc(const exprt &, const std::string &msg, statet &)
Definition: symex_main.cpp:73
goto_symex_statet::framet::return_value
exprt return_value
Definition: goto_symex_state.h:182
goto_symext::symex_config
const symex_configt symex_config
Definition: goto_symex.h:165
code_typet::parametert::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:828
byte_extract_exprt
TO_BE_DOCUMENTED.
Definition: byte_operators.h:25
code_typet::parametert
Definition: std_types.h:788
guardt::as_expr
exprt as_expr() const
Definition: guard.h:41
symex_level1t::restore_from
void restore_from(const current_namest &other)
Insert the content of other into this renaming.
Definition: renaming_level.cpp:59
goto_symext::symex_function_call_symbol
virtual void symex_function_call_symbol(const get_goto_functiont &, statet &, const code_function_callt &)
Definition: symex_function_call.cpp:198
goto_symext::get_goto_functiont
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
Definition: goto_symex.h:109
goto_symex_statet::previous_frame
const framet & previous_frame()
Definition: goto_symex_state.h:229
goto_symext::symex_fkt
virtual void symex_fkt(statet &, const code_function_callt &)
Definition: symex_builtin_functions.cpp:492
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
symex_target_equationt::function_return
virtual void function_return(const exprt &guard, const sourcet &source, bool hidden)
Record return from a function.
Definition: symex_target_equation.cpp:225
goto_symex_statet::level2
symex_level2t level2
Definition: goto_symex_state.h:66
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:256
messaget::warning
mstreamt & warning() const
Definition: message.h:391
goto_symext::parameter_assignments
void parameter_assignments(const irep_idt &function_identifier, const goto_functionst::goto_functiont &, statet &, const exprt::operandst &arguments)
Definition: symex_function_call.cpp:29
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:228
c_types.h
symex_renaming_levelt::current_names
current_namest current_names
Definition: renaming_level.h:31
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
code_function_callt::function
exprt & function()
Definition: std_code.h:1099
validation_modet::INVARIANT
goto_programt::instructiont::is_return
bool is_return() const
Definition: goto_program.h:306