cprover
symex_catch.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 
15 {
16  // there are two variants: 'push' and 'pop'
17 
18  #if 0
19  const goto_programt::instructiont &instruction=*state.source.pc;
20 
21  if(instruction.targets.empty()) // pop
22  {
23  if(state.call_stack.empty())
24  throw "catch-pop on empty call stack";
25 
26  if(state.top().catch_map.empty())
27  throw "catch-pop on function frame";
28 
29  // pop the stack frame
30  state.call_stack.pop_back();
31  }
32  else // push
33  {
34  state.catch_stack.push_back(goto_symex_statet::catch_framet());
35  goto_symex_statet::catch_framet &frame=state.catch_stack.back();
36 
37  // copy targets
38  const irept::subt &exception_list=
39  instruction.code.find(ID_exception_list).get_sub();
40 
41  assert(exception_list.size()==instruction.targets.size());
42 
43  unsigned i=0;
44 
45  for(goto_programt::targetst::const_iterator
46  it=instruction.targets.begin();
47  it!=instruction.targets.end();
48  it++, i++)
49  frame.target_map[exception_list[i].id()]=*it;
50  }
51  #endif
52 }
goto_programt::const_targett pc
Definition: symex_target.h:32
std::vector< irept > subt
Definition: irep.h:91
Symbolic Execution.
call_stackt & call_stack()
void symex_catch(statet &state)
Definition: symex_catch.cpp:14
symex_targett::sourcet source