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 {
17  // there are two variants: 'push' and 'pop'
18 
19  #if 0
20  const goto_programt::instructiont &instruction=*state.source.pc;
21 
22  if(instruction.targets.empty()) // pop
23  {
24  if(state.call_stack.empty())
25  throw "catch-pop on empty call stack";
26 
27  if(state.top().catch_map.empty())
28  throw "catch-pop on function frame";
29 
30  // pop the stack frame
31  state.call_stack.pop_back();
32  }
33  else // push
34  {
35  state.catch_stack.push_back(goto_symex_statet::catch_framet());
36  goto_symex_statet::catch_framet &frame=state.catch_stack.back();
37 
38  // copy targets
39  const irept::subt &exception_list=
40  instruction.code.find(ID_exception_list).get_sub();
41 
42  assert(exception_list.size()==instruction.targets.size());
43 
44  unsigned i=0;
45 
46  for(goto_programt::targetst::const_iterator
47  it=instruction.targets.begin();
48  it!=instruction.targets.end();
49  it++, i++)
50  frame.target_map[exception_list[i].id()]=*it;
51  }
52  #endif
53 }
std::vector< irept > subt
Definition: irep.h:160
subt & get_sub()
Definition: irep.h:317
targetst targets
The list of successor instructions.
Definition: goto_program.h:198
void symex_catch(statet &)
Definition: symex_catch.cpp:14
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
Symbolic Execution.
#define UNREACHABLE
Definition: invariant.h:271
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285