cprover
path_symex_class.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 #ifndef CPROVER_PATH_SYMEX_PATH_SYMEX_CLASS_H
13 #define CPROVER_PATH_SYMEX_PATH_SYMEX_CLASS_H
14 
15 #include "path_symex.h"
16 
18 {
19 public:
21  {
22  }
23 
24  virtual void operator()(
25  path_symex_statet &state,
26  std::list<path_symex_statet> &furter_states);
27 
28  virtual void operator()(path_symex_statet &state);
29 
30  void do_goto(
31  path_symex_statet &state,
32  bool taken);
33 
34  virtual void do_assert_fail(path_symex_statet &state)
35  {
36  const goto_programt::instructiont &instruction=
37  *state.get_instruction();
38 
39  state.record_step();
40  state.next_pc();
41  exprt guard=state.read(not_exprt(instruction.guard));
42  state.history->guard=guard;
43  }
44 
46 
47 protected:
48  void do_goto(
49  path_symex_statet &state,
50  std::list<path_symex_statet> &further_states);
51 
53  path_symex_statet &state,
54  const code_function_callt &call,
55  std::list<path_symex_statet> &further_states)
56  {
57  exprt f=state.read(call.function());
58  function_call_rec(state, call, f, further_states);
59  }
60 
61  void function_call_rec(
62  path_symex_statet &state,
64  const exprt &function,
65  std::list<path_symex_statet> &further_states);
66 
68 
69  void set_return_value(path_symex_statet &, const exprt &);
70 
71  void symex_malloc(
72  path_symex_statet &state,
73  const exprt &lhs,
74  const side_effect_exprt &code);
75 
76  void symex_va_arg_next(
77  path_symex_statet &state,
78  const exprt &lhs,
79  const side_effect_exprt &code);
80 
81  void assign(
82  path_symex_statet &state,
83  const exprt &lhs,
84  const exprt &rhs);
85 
86  void assign(
87  path_symex_statet &state,
88  const code_assignt &assignment)
89  {
90  assign(state, assignment.lhs(), assignment.rhs());
91  }
92 
93  void assign_rec(
94  path_symex_statet &state,
95  exprt::operandst &guard, // instantiated
96  const exprt &ssa_lhs, // instantiated, recursion here
97  const exprt &ssa_rhs); // instantiated
98 
99  static bool propagate(const exprt &src);
100 };
101 
102 
103 #endif // CPROVER_PATH_SYMEX_PATH_SYMEX_CLASS_H
virtual void operator()(path_symex_statet &state, std::list< path_symex_statet > &furter_states)
Definition: path_symex.cpp:943
Boolean negation.
Definition: std_expr.h:2648
void assign(path_symex_statet &state, const code_assignt &assignment)
path_symex_stept stept
void assign_rec(path_symex_statet &state, exprt::operandst &guard, const exprt &ssa_lhs, const exprt &ssa_rhs)
Definition: path_symex.cpp:347
void symex_malloc(path_symex_statet &state, const exprt &lhs, const side_effect_exprt &code)
Definition: path_symex.cpp:156
void function_call(path_symex_statet &state, const code_function_callt &call, std::list< path_symex_statet > &further_states)
void do_goto(path_symex_statet &state, bool taken)
Definition: path_symex.cpp:907
virtual void do_assert_fail(path_symex_statet &state)
exprt & lhs()
Definition: std_code.h:157
exprt read(const exprt &src)
exprt & rhs()
Definition: std_code.h:162
void symex_va_arg_next(path_symex_statet &state, const exprt &lhs, const side_effect_exprt &code)
Definition: path_symex.cpp:288
void assign(path_symex_statet &state, const exprt &lhs, const exprt &rhs)
Definition: path_symex.cpp:92
A function call.
Definition: std_code.h:657
void return_from_function(path_symex_statet &state)
Definition: path_symex.cpp:815
std::vector< exprt > operandst
Definition: expr.h:49
static bool propagate(const exprt &src)
Definition: path_symex.cpp:33
goto_programt::const_targett get_instruction() const
exprt & function()
Definition: std_code.h:677
Base class for all expressions.
Definition: expr.h:46
Concrete Symbolic Transformer.
void function_call_rec(path_symex_statet &state, const code_function_callt &function_call, const exprt &function, std::list< path_symex_statet > &further_states)
Definition: path_symex.cpp:632
void set_return_value(path_symex_statet &, const exprt &)
Definition: path_symex.cpp:850
An expression containing a side effect.
Definition: std_code.h:997
path_symex_step_reft history
Assignment.
Definition: std_code.h:144