cprover
goto_symex.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 "goto_symex.h"
13 
14 #include <util/simplify_expr.h>
15 
16 unsigned goto_symext::nondet_count=0;
18 
20 {
21  if(options.get_bool_option("simplify"))
22  simplify(expr, ns);
23 }
24 
26 {
27  irep_idt identifier = "symex::nondet" + std::to_string(nondet_count++);
28  nondet_symbol_exprt new_expr(identifier, type);
29  return new_expr;
30 }
31 
33 {
34  if(expr.id()==ID_side_effect &&
35  expr.get(ID_statement)==ID_nondet)
36  {
37  nondet_symbol_exprt new_expr = build_symex_nondet(expr.type());
38  new_expr.add_source_location()=expr.source_location();
39  expr.swap(new_expr);
40  }
41  else
42  Forall_operands(it, expr)
43  replace_nondet(*it);
44 }
The type of an expression.
Definition: type.h:22
void replace_nondet(exprt &)
Definition: goto_symex.cpp:32
typet & type()
Definition: expr.h:56
virtual void do_simplify(exprt &)
Definition: goto_symex.cpp:19
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:239
const irep_idt & id() const
Definition: irep.h:259
static unsigned nondet_count
Definition: goto_symex.h:463
static unsigned dynamic_counter
Definition: goto_symex.h:464
Symbolic Execution.
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
const optionst & options
Definition: goto_symex.h:204
Expression to hold a nondeterministic choice.
Definition: std_expr.h:239
Base class for all expressions.
Definition: expr.h:42
std::string to_string(const string_constraintt &expr)
Used for debug printing.
const source_locationt & source_location() const
Definition: expr.h:125
void swap(irept &irep)
Definition: irep.h:303
#define Forall_operands(it, expr)
Definition: expr.h:23
source_locationt & add_source_location()
Definition: expr.h:130
nondet_symbol_exprt build_symex_nondet(typet &type)
Definition: goto_symex.cpp:25
bool simplify(exprt &expr, const namespacet &ns)