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/byte_operators.h>
16 #include <util/c_types.h>
17 #include <util/exception_utils.h>
18 #include <util/fresh_symbol.h>
19 #include <util/invariant.h>
20 #include <util/prefix.h>
21 #include <util/range.h>
22 
23 #include "expr_skeleton.h"
24 #include "symex_assign.h"
25 
26 static void locality(
27  const irep_idt &function_identifier,
28  goto_symext::statet &state,
29  path_storaget &path_storage,
30  const goto_functionst::goto_functiont &goto_function,
31  const namespacet &ns);
32 
33 bool goto_symext::get_unwind_recursion(const irep_idt &, unsigned, unsigned)
34 {
35  return false;
36 }
37 
39  const irep_idt &function_identifier,
40  const goto_functionst::goto_functiont &goto_function,
41  statet &state,
42  const exprt::operandst &arguments)
43 {
44  const code_typet &function_type=goto_function.type;
45 
46  // iterates over the arguments
47  exprt::operandst::const_iterator it1=arguments.begin();
48 
49  // iterates over the types of the parameters
50  for(const auto &identifier : goto_function.parameter_identifiers)
51  {
52  INVARIANT(
53  !identifier.empty(), "function parameter must have an identifier");
54  state.call_stack().top().parameter_names.push_back(identifier);
55 
56  const symbolt &symbol=ns.lookup(identifier);
57  symbol_exprt lhs=symbol.symbol_expr();
58 
59  // this is the type that the n-th argument should have
60  const typet &parameter_type = symbol.type;
61 
62  exprt rhs;
63 
64  // if you run out of actual arguments there was a mismatch
65  if(it1==arguments.end())
66  {
67  log.warning() << state.source.pc->source_location.as_string()
68  << ": "
69  "call to '"
70  << id2string(function_identifier)
71  << "': "
72  "not enough arguments, inserting non-deterministic value"
73  << log.eom;
74 
76  parameter_type, state.source.pc->source_location);
77  }
78  else
79  rhs=*it1;
80 
81  if(rhs.is_nil())
82  {
83  // 'nil' argument doesn't get assigned
84  }
85  else
86  {
87  // It should be the same exact type.
88  if(parameter_type != rhs.type())
89  {
90  const typet &rhs_type = rhs.type();
91 
92  // But we are willing to do some limited conversion.
93  // This is highly dubious, obviously.
94  // clang-format off
95  if(
96  (parameter_type.id() == ID_signedbv ||
97  parameter_type.id() == ID_unsignedbv ||
98  parameter_type.id() == ID_c_enum_tag ||
99  parameter_type.id() == ID_bool ||
100  parameter_type.id() == ID_pointer ||
101  parameter_type.id() == ID_union ||
102  parameter_type.id() == ID_union_tag) &&
103  (rhs_type.id() == ID_signedbv ||
104  rhs_type.id() == ID_unsignedbv ||
105  rhs_type.id() == ID_c_bit_field ||
106  rhs_type.id() == ID_c_enum_tag ||
107  rhs_type.id() == ID_bool ||
108  rhs_type.id() == ID_pointer ||
109  rhs_type.id() == ID_union ||
110  rhs_type.id() == ID_union_tag))
111  {
112  rhs=
114  byte_extract_id(),
115  rhs,
116  from_integer(0, index_type()),
117  parameter_type);
118  }
119  // clang-format on
120  else
121  {
122  std::ostringstream error;
123  error << state.source.pc->source_location.as_string() << ": "
124  << "function call: parameter \"" << identifier
125  << "\" type mismatch:\ngot " << rhs.type().pretty()
126  << "\nexpected " << parameter_type.pretty();
127  throw unsupported_operation_exceptiont(error.str());
128  }
129  }
130 
131  assignment_typet assignment_type;
132 
133  // We hide if we are in a hidden function.
134  if(state.call_stack().top().hidden_function)
135  assignment_type =
137  else
138  assignment_type =
140 
141  lhs = to_symbol_expr(clean_expr(std::move(lhs), state, true));
142  rhs = clean_expr(std::move(rhs), state, false);
143 
144  exprt::operandst lhs_conditions;
145  symex_assignt{state, assignment_type, ns, symex_config, target}
146  .assign_rec(lhs, expr_skeletont{}, rhs, lhs_conditions);
147  }
148 
149  if(it1!=arguments.end())
150  it1++;
151  }
152 
153  if(function_type.has_ellipsis())
154  {
155  // These are va_arg arguments; their types may differ from call to call
156  for(; it1 != arguments.end(); it1++)
157  {
158  symbolt &va_arg = get_fresh_aux_symbol(
159  it1->type(),
160  id2string(function_identifier),
161  "va_arg",
162  state.source.pc->source_location,
163  ns.lookup(function_identifier).mode,
164  state.symbol_table);
165  va_arg.is_parameter = true;
166 
167  state.call_stack().top().parameter_names.push_back(va_arg.name);
168 
169  symex_assign(state, code_assignt{va_arg.symbol_expr(), *it1});
170  }
171  }
172  else if(it1!=arguments.end())
173  {
174  // we got too many arguments, but we will just ignore them
175  }
176 }
177 
179  const get_goto_functiont &get_goto_function,
180  statet &state,
181  const code_function_callt &code)
182 {
183  const exprt &function=code.function();
184 
185  // If at some point symex_function_call can support more
186  // expression ids(), like ID_Dereference, please expand the
187  // precondition appropriately.
188  PRECONDITION(function.id() == ID_symbol);
190 }
191 
193  const get_goto_functiont &get_goto_function,
194  statet &state,
195  const code_function_callt &original_code)
196 {
197  code_function_callt code = original_code;
198 
199  if(code.lhs().is_not_nil())
200  code.lhs() = clean_expr(std::move(code.lhs()), state, true);
201 
202  code.function() = clean_expr(std::move(code.function()), state, false);
203 
204  Forall_expr(it, code.arguments())
205  *it = clean_expr(std::move(*it), state, false);
206 
207  target.location(state.guard.as_expr(), state.source);
208 
209  PRECONDITION(code.function().id() == ID_symbol);
210 
211  const irep_idt &identifier=
213 
214  if(has_prefix(id2string(identifier), CPROVER_FKT_PREFIX))
215  {
216  symex_fkt(state, code);
217  }
218  else
220 }
221 
223  const get_goto_functiont &get_goto_function,
224  statet &state,
225  const code_function_callt &call)
226 {
227  const irep_idt &identifier=
229 
230  const goto_functionst::goto_functiont &goto_function =
231  get_goto_function(identifier);
232 
233  path_storage.dirty.populate_dirty_for_function(identifier, goto_function);
234 
235  auto emplace_safe_pointers_result =
236  path_storage.safe_pointers.emplace(identifier, local_safe_pointerst{});
237  if(emplace_safe_pointers_result.second)
238  emplace_safe_pointers_result.first->second(goto_function.body);
239 
240  const bool stop_recursing = get_unwind_recursion(
241  identifier,
242  state.source.thread_nr,
243  state.call_stack().top().loop_iterations[identifier].count);
244 
245  // see if it's too much
246  if(stop_recursing)
247  {
249  {
250  // it's ok, ignore
251  }
252  else
253  {
255  vcc(false_exprt(), "recursion unwinding assertion", state);
256 
257  // Rule out this path:
258  symex_assume_l2(state, false_exprt());
259  }
260 
261  symex_transition(state);
262  return;
263  }
264 
265  // read the arguments -- before the locality renaming
266  const exprt::operandst &arguments = call.arguments();
267  const std::vector<renamedt<exprt, L2>> renamed_arguments =
268  make_range(arguments).map(
269  [&](const exprt &a) { return state.rename(a, ns); });
270 
271  // we hide the call if the caller and callee are both hidden
272  const bool callee_is_hidden = ns.lookup(identifier).is_hidden();
273  const bool hidden =
274  state.call_stack().top().hidden_function && callee_is_hidden;
275 
276  // record the call
278  state.guard.as_expr(), identifier, renamed_arguments, state.source, hidden);
279 
280  if(!goto_function.body_available())
281  {
282  no_body(identifier);
283 
284  // record the return
286  state.guard.as_expr(), identifier, state.source, hidden);
287 
288  if(call.lhs().is_not_nil())
289  {
290  const auto rhs =
292  code_assignt code(call.lhs(), rhs);
293  symex_assign(state, code);
294  }
295 
296  symex_transition(state);
297  return;
298  }
299 
300  // produce a new frame
301  PRECONDITION(!state.call_stack().empty());
302  framet &frame = state.call_stack().new_frame(state.source, state.guard);
303 
304  // Only enable loop analysis when complexity is enabled.
306  {
307  // Analyzes loops if required.
308  path_storage.add_function_loops(identifier, goto_function.body);
309  frame.loops_info = path_storage.get_loop_analysis(identifier);
310  }
311 
312  // preserve locality of local variables
313  locality(identifier, state, path_storage, goto_function, ns);
314 
315  // assign actuals to formal parameters
316  parameter_assignments(identifier, goto_function, state, arguments);
317 
318  frame.end_of_function=--goto_function.body.instructions.end();
319  frame.return_value=call.lhs();
320  frame.function_identifier=identifier;
321  frame.hidden_function = callee_is_hidden;
322 
323  const framet &p_frame = state.call_stack().previous_frame();
324  for(const auto &pair : p_frame.loop_iterations)
325  {
326  if(pair.second.is_recursion)
327  frame.loop_iterations.insert(pair);
328  }
329 
330  // increase unwinding counter
331  frame.loop_iterations[identifier].is_recursion=true;
332  frame.loop_iterations[identifier].count++;
333 
334  state.source.function_id = identifier;
335  symex_transition(state, goto_function.body.instructions.begin(), false);
336 }
337 
339 static void pop_frame(
340  goto_symext::statet &state,
341  const path_storaget &path_storage,
342  bool doing_path_exploration)
343 {
344  PRECONDITION(!state.call_stack().empty());
345 
346  {
347  const framet &frame = state.call_stack().top();
348 
349  // restore program counter
350  symex_transition(state, frame.calling_location.pc, false);
352 
353  // restore L1 renaming
354  state.level1.restore_from(frame.old_level1);
355 
356  // If the program is multi-threaded then the state guard is used to
357  // accumulate assumptions (in symex_assume_l2) and must be left alone.
358  // If however it is single-threaded then we should restore the guard, as the
359  // guard coming out of the function may be more complex (e.g. if the callee
360  // was { if(x) while(true) { } } then the guard may still be `!x`),
361  // but at this point all control-flow paths have either converged or been
362  // proven unviable, so we can stop specifying the callee's constraints when
363  // we generate an assumption or VCC.
364 
365  // If we're doing path exploration then we do tail-duplication, and we
366  // actually *are* in a more-restricted context than we were when the
367  // function began.
368  if(state.threads.size() == 1 && !doing_path_exploration)
369  {
370  state.guard = frame.guard_at_function_start;
371  }
372 
374  state.get_level2().current_names.get_view(view);
375 
376  std::vector<irep_idt> keys_to_erase;
377 
378  for(const auto &pair : view)
379  {
380  const irep_idt l1_o_id = pair.second.first.get_l1_object_identifier();
381 
382  // could use iteration over local_objects as l1_o_id is prefix
383  if(
384  frame.local_objects.find(l1_o_id) == frame.local_objects.end() ||
385  (state.threads.size() > 1 &&
386  path_storage.dirty(pair.second.first.get_object_name())))
387  {
388  continue;
389  }
390 
391  keys_to_erase.push_back(pair.first);
392  }
393 
394  for(const irep_idt &key : keys_to_erase)
395  {
396  state.drop_existing_l1_name(key);
397  }
398  }
399 
400  state.call_stack().pop();
401 }
402 
405 {
406  const bool hidden = state.call_stack().top().hidden_function;
407 
408  // first record the return
410  state.guard.as_expr(), state.source.function_id, state.source, hidden);
411 
412  // then get rid of the frame
414 }
415 
418 static void locality(
419  const irep_idt &function_identifier,
420  goto_symext::statet &state,
421  path_storaget &path_storage,
422  const goto_functionst::goto_functiont &goto_function,
423  const namespacet &ns)
424 {
425  unsigned &frame_nr=
426  state.threads[state.source.thread_nr].function_frame[function_identifier];
427  frame_nr++;
428 
429  for(const auto &param : goto_function.parameter_identifiers)
430  {
431  (void)state.add_object(
432  ns.lookup(param).symbol_expr(),
433  [&path_storage, &frame_nr](const irep_idt &l0_name) {
434  return path_storage.get_unique_l1_index(l0_name, frame_nr);
435  },
436  ns);
437  }
438 }
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:37
symex_targett::assignment_typet
assignment_typet
Definition: symex_target.h:70
code_typet::has_ellipsis
bool has_ellipsis() const
Definition: std_types.h:813
Forall_expr
#define Forall_expr(it, expr)
Definition: expr.h:33
goto_symext::symex_assume_l2
void symex_assume_l2(statet &, const exprt &cond)
Definition: symex_main.cpp:219
CPROVER_FKT_PREFIX
#define CPROVER_FKT_PREFIX
Definition: cprover_prefix.h:16
symex_configt::partial_loops
bool partial_loops
Definition: symex_config.h:35
symex_assign.h
symex_level1t::restore_from
void restore_from(const symex_level1t &other)
Insert the content of other into this renaming.
Definition: renaming_level.cpp:121
goto_symex_statet::level1
symex_level1t level1
Definition: goto_symex_state.h:75
arith_tools.h
symex_target_equationt::function_return
virtual void function_return(const exprt &guard, const irep_idt &function_id, const sourcet &source, bool hidden)
Record return from a function.
Definition: symex_target_equation.cpp:193
goto_symext::symex_function_call_code
virtual void symex_function_call_code(const get_goto_functiont &get_goto_function, statet &state, const code_function_callt &call)
Symbolic execution of a function call by inlining.
Definition: symex_function_call.cpp:222
typet
The type of an expression, extends irept.
Definition: type.h:29
fresh_symbol.h
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:488
symex_targett::sourcet::pc
goto_programt::const_targett pc
Definition: symex_target.h:43
expr_skeleton.h
goto_symext::target
symex_target_equationt & target
The equation that this execution is building up.
Definition: goto_symex.h:264
path_storaget
Storage for symbolic execution paths to be resumed later.
Definition: path_storage.h:38
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
goto_symext::path_storage
path_storaget & path_storage
Symbolic execution paths to be resumed later.
Definition: goto_symex.h:796
goto_symex_statet
Central data structure: state.
Definition: goto_symex_state.h:46
framet::function_identifier
irep_idt function_identifier
Definition: frame.h:27
call_stackt::pop
void pop()
Definition: call_stack.h:36
unsupported_operation_exceptiont
Thrown when we encounter an instruction, parameters to an instruction etc.
Definition: exception_utils.h:144
framet::calling_location
symex_targett::sourcet calling_location
Definition: frame.h:29
local_safe_pointerst
A very simple, cheap analysis to determine when dereference operations are trivially guarded by a che...
Definition: local_safe_pointers.h:25
symex_targett::sourcet::thread_nr
unsigned thread_nr
Definition: symex_target.h:39
goto_symext::symex_fkt
virtual void symex_fkt(statet &state, const code_function_callt &code)
Symbolically execute a FUNCTION_CALL instruction for a function whose name starts with CPROVER_FKT_PR...
Definition: symex_builtin_functions.cpp:549
prefix.h
invariant.h
exprt
Base class for all expressions.
Definition: expr.h:53
framet::guard_at_function_start
guardt guard_at_function_start
Definition: frame.h:31
goto_symex_statet::source
symex_targett::sourcet source
Definition: goto_symex_state.h:64
symex_assignt
Functor for symex assignment.
Definition: symex_assign.h:26
messaget::eom
static eomt eom
Definition: message.h:283
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
framet::hidden_function
bool hidden_function
Definition: frame.h:34
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1211
goto_symext::symex_assign
void symex_assign(statet &state, const code_assignt &code)
Symbolically execute an ASSIGN instruction or simulate such an execution for a synthetic assignment.
Definition: goto_symex.cpp:38
goto_symext::get_unwind_recursion
virtual bool get_unwind_recursion(const irep_idt &identifier, unsigned thread_nr, unsigned unwind)
Definition: symex_function_call.cpp:33
symex_targett::assignment_typet::VISIBLE_ACTUAL_PARAMETER
@ VISIBLE_ACTUAL_PARAMETER
goto_symext::log
messaget log
The messaget to write log messages to.
Definition: goto_symex.h:276
symex_target_equationt::location
virtual void location(const exprt &guard, const sourcet &source)
Record a location.
Definition: symex_target_equation.cpp:162
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
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:81
call_stackt::new_frame
framet & new_frame(symex_targett::sourcet calling_location, const guardt &guard)
Definition: call_stack.h:30
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1186
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
sharing_mapt< irep_idt, std::pair< ssa_exprt, std::size_t > >::viewt
std::vector< view_itemt > viewt
View of the key-value pairs in the map.
Definition: sharing_map.h:365
goto_symex_statet::threads
std::vector< threadt > threads
Definition: goto_symex_state.h:198
framet::parameter_names
std::vector< irep_idt > parameter_names
Definition: frame.h:30
path_storaget::get_loop_analysis
std::shared_ptr< lexical_loopst > get_loop_analysis(const irep_idt &function_id)
Definition: path_storage.h:131
goto_symext::parameter_assignments
void parameter_assignments(const irep_idt &function_identifier, const goto_functionst::goto_functiont &goto_function, statet &state, const exprt::operandst &arguments)
Iterates over arguments and assigns them to the parameters, which are symbols whose name and type are...
Definition: symex_function_call.cpp:38
byte_operators.h
Expression classes for byte-level operators.
framet::loops_info
std::shared_ptr< lexical_loopst > loops_info
Definition: frame.h:68
goto_symex_statet::call_stack
call_stackt & call_stack()
Definition: goto_symex_state.h:147
call_stackt::top
framet & top()
Definition: call_stack.h:17
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:69
symex_targett::assignment_typet::HIDDEN_ACTUAL_PARAMETER
@ HIDDEN_ACTUAL_PARAMETER
pop_frame
static void pop_frame(goto_symext::statet &state, const path_storaget &path_storage, bool doing_path_exploration)
pop one call frame
Definition: symex_function_call.cpp:339
guard_exprt::as_expr
exprt as_expr() const
Definition: guard_expr.h:49
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
symex_configt::doing_path_exploration
bool doing_path_exploration
Definition: symex_config.h:23
symex_configt::unwinding_assertions
bool unwinding_assertions
Definition: symex_config.h:33
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:77
goto_symex.h
goto_statet::guard
guardt guard
Definition: goto_state.h:50
framet::loop_iterations
std::unordered_map< irep_idt, loop_infot > loop_iterations
Definition: frame.h:71
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
goto_symext::symex_end_of_function
virtual void symex_end_of_function(statet &)
Symbolically execute a END_FUNCTION instruction.
Definition: symex_function_call.cpp:404
framet::return_value
exprt return_value
Definition: frame.h:33
path_storaget::dirty
incremental_dirtyt dirty
Local variables are considered 'dirty' if they've had an address taken and therefore may be referred ...
Definition: path_storage.h:116
goto_symext::symex_function_call_symbol
virtual void symex_function_call_symbol(const get_goto_functiont &get_goto_function, statet &state, const code_function_callt &code)
Symbolic execution of a call to a function call.
Definition: symex_function_call.cpp:192
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
code_typet
Base type of functions.
Definition: std_types.h:736
symbolt::is_parameter
bool is_parameter
Definition: symbol.h:67
irept::is_nil
bool is_nil() const
Definition: irep.h:398
irept::id
const irep_idt & id() const
Definition: irep.h:418
framet::end_of_function
goto_programt::const_targett end_of_function
Definition: frame.h:32
range.h
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
path_storaget::add_function_loops
void add_function_loops(const irep_idt &identifier, const goto_programt &body)
Generates a loop analysis for the instructions in goto_programt and keys it against function ID.
Definition: path_storage.h:120
goto_symext::clean_expr
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
Definition: symex_clean_expr.cpp:229
false_exprt
The Boolean constant false.
Definition: std_expr.h:3993
framet
Stack frames – these are used for function calls and for exceptions.
Definition: frame.h:21
framet::old_level1
symex_level1t old_level1
Definition: frame.h:36
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1231
symex_transition
void symex_transition(goto_symext::statet &state)
Transition to the next instruction, which increments the internal program counter and initializes the...
Definition: symex_main.cpp:147
sharing_mapt::get_view
void get_view(viewt &view) const
Get a view of the elements in the map A view is a list of pairs with the components being const refer...
Definition: sharing_map.h:782
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1955
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:256
symex_configt::complexity_limits_active
bool complexity_limits_active
Whether this run of symex is under complexity limits.
Definition: symex_config.h:53
call_stackt::previous_frame
const framet & previous_frame()
Definition: call_stack.h:42
symex_level2t::current_names
symex_renaming_levelt current_names
Definition: renaming_level.h:83
path_storaget::safe_pointers
std::unordered_map< irep_idt, local_safe_pointerst > safe_pointers
Map function identifiers to local_safe_pointerst instances.
Definition: path_storage.h:100
symex_target_equationt::function_call
virtual void function_call(const exprt &guard, const irep_idt &function_id, const std::vector< renamedt< exprt, L2 >> &ssa_function_arguments, const sourcet &source, bool hidden)
Record a function call.
Definition: symex_target_equation.cpp:174
symbolt
Symbol table entry.
Definition: symbol.h:28
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
goto_statet::get_level2
const symex_level2t & get_level2() const
Definition: goto_state.h:37
goto_symext::vcc
virtual void vcc(const exprt &, const std::string &msg, statet &)
Definition: symex_main.cpp:182
goto_symext::get_goto_function
static get_goto_functiont get_goto_function(abstract_goto_modelt &goto_model)
Return a function to get/load a goto function from the given goto model Create a default delegate to ...
Definition: symex_main.cpp:491
goto_symext::symex_config
const symex_configt symex_config
The configuration to use for this symbolic execution.
Definition: goto_symex.h:183
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
framet::local_objects
std::set< irep_idt > local_objects
Definition: frame.h:38
path_storaget::get_unique_l1_index
std::size_t get_unique_l1_index(const irep_idt &id, std::size_t minimum_index)
Provide a unique L1 index for a given id, starting from minimum_index.
Definition: path_storage.h:104
goto_symext::get_goto_functiont
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
The type of delegate functions that retrieve a goto_functiont for a particular function identifier.
Definition: goto_symex.h:95
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
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...
goto_symext::no_body
virtual void no_body(const irep_idt &identifier)
Log a warning that a function has no body.
Definition: goto_symex.h:432
locality
static void locality(const irep_idt &function_identifier, goto_symext::statet &state, path_storaget &path_storage, const goto_functionst::goto_functiont &goto_function, const namespacet &ns)
Preserves locality of parameters of a given function by applying L1 renaming to them.
Definition: symex_function_call.cpp:418
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:298
goto_symext::symex_function_call
virtual void symex_function_call(const get_goto_functiont &get_goto_function, statet &state, const code_function_callt &code)
Symbolically execute a FUNCTION_CALL instruction.
Definition: symex_function_call.cpp:178
symex_targett::sourcet::function_id
irep_idt function_id
Definition: symex_target.h:40
messaget::warning
mstreamt & warning() const
Definition: message.h:390
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:252
goto_symex_statet::add_object
ssa_exprt add_object(const symbol_exprt &expr, std::function< std::size_t(const irep_idt &)> index_generator, const namespacet &ns)
Instantiate the object expr.
Definition: goto_symex_state.cpp:784
make_range
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
c_types.h
get_fresh_aux_symbol
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Definition: fresh_symbol.cpp:32
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
code_function_callt::function
exprt & function()
Definition: std_code.h:1221
goto_symex_statet::drop_existing_l1_name
void drop_existing_l1_name(const irep_idt &l1_identifier)
Drops an L1 name from the local L2 map.
Definition: goto_symex_state.h:232
expr_skeletont
Expression in which some part is missing and can be substituted for another expression.
Definition: expr_skeleton.h:26
validation_modet::INVARIANT
@ INVARIANT