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 
17 
19 {
21  simplify(expr, ns);
22 }
23 
25 {
26  irep_idt identifier = "symex::nondet" + std::to_string(nondet_count++);
27  nondet_symbol_exprt new_expr(identifier, type);
28  return new_expr;
29 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
nondet_symbol_exprt
Expression to hold a nondeterministic choice.
Definition: std_expr.h:277
goto_symext::dynamic_counter
static unsigned dynamic_counter
Definition: goto_symex.h:423
typet
The type of an expression, extends irept.
Definition: type.h:27
exprt
Base class for all expressions.
Definition: expr.h:54
goto_symext::do_simplify
virtual void do_simplify(exprt &)
Definition: goto_symex.cpp:18
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:53
symex_nondet_generatort::operator()
nondet_symbol_exprt operator()(typet &type)
Definition: goto_symex.cpp:24
goto_symex.h
symex_configt::simplify_opt
bool simplify_opt
Definition: goto_symex.h:59
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2320
simplify_expr.h
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_nondet_generatort::nondet_count
unsigned nondet_count
Definition: goto_symex.h:48
goto_symext::symex_config
const symex_configt symex_config
Definition: goto_symex.h:165