cprover
path_symex.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Concrete Symbolic Transformer
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 // NOLINT(build/header_guard) as this file is also symlinked
13 #ifndef CPROVER_PATH_SYMEX_PATH_SYMEX_H
14 #define CPROVER_PATH_SYMEX_PATH_SYMEX_H
15 
16 #include "path_symex_state.h"
17 
18 // Transform a state by executing a single statement.
19 // May occasionally yield more than one successor state
20 // (branches, function calls with ternary operator),
21 // which are put into "further_states".
22 
23 // \pre: "!further_states.empty()" because "state" must
24 // be stored inside "further_states"
25 void path_symex(
26  path_symex_statet &state,
27  std::list<path_symex_statet> &further_states);
28 
29 // Transform a state by executing a single statement.
30 // Will fail if there is more than one successor state.
31 void path_symex(path_symex_statet &state);
32 
33 // Transforms a state by executing a goto statement;
34 // the 'taken' argument indicates which way.
35 void path_symex_goto(
36  path_symex_statet &state,
37  bool taken);
38 
39 // Transforms a state by executing an assertion statement;
40 // it is enforced that the assertion fails.
42  path_symex_statet &state);
43 
44 #endif // CPROVER_PATH_SYMEX_PATH_SYMEX_H
void path_symex_assert_fail(path_symex_statet &state)
State of path-based symbolic simulator.
void path_symex(path_symex_statet &state, std::list< path_symex_statet > &further_states)
void path_symex_goto(path_symex_statet &state, bool taken)