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  if(expr.id()==ID_side_effect &&
28  expr.get(ID_statement)==ID_nondet)
29  {
30  exprt new_expr(ID_nondet_symbol, expr.type());
31  new_expr.set(ID_identifier, "symex::nondet"+std::to_string(nondet_count++));
32  new_expr.add_source_location()=expr.source_location();
33  expr.swap(new_expr);
34  }
35  else
36  Forall_operands(it, expr)
37  replace_nondet(*it);
38 }
virtual void do_simplify(exprt &expr)
Definition: goto_symex.cpp:19
optionst options
Definition: goto_symex.h:96
typet & type()
Definition: expr.h:60
void replace_nondet(exprt &expr)
Definition: goto_symex.cpp:25
const irep_idt & id() const
Definition: irep.h:189
static unsigned nondet_count
Definition: goto_symex.h:333
static unsigned dynamic_counter
Definition: goto_symex.h:334
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
Base class for all expressions.
Definition: expr.h:46
const source_locationt & source_location() const
Definition: expr.h:142
void swap(irept &irep)
Definition: irep.h:231
#define Forall_operands(it, expr)
Definition: expr.h:23
const namespacet & ns
Definition: goto_symex.h:104
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
bool simplify(exprt &expr, const namespacet &ns)