CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
symex_catch.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "goto_symex.h"
13
15{
16 // TODO: uncomment this line when TG-4667 is done
17 // UNREACHABLE;
18 // there are two variants: 'push' and 'pop'
19
20 #if 0
21 const goto_programt::instructiont &instruction=*state.source.pc;
22
23 if(instruction.targets.empty()) // pop
24 {
25 if(state.call_stack.empty())
26 throw "catch-pop on empty call stack";
27
28 if(state.top().catch_map.empty())
29 throw "catch-pop on function frame";
30
31 // pop the stack frame
32 state.call_stack.pop_back();
33 }
34 else // push
35 {
36 state.catch_stack.push_back(goto_symex_statet::catch_framet());
37 goto_symex_statet::catch_framet &frame=state.catch_stack.back();
38
39 // copy targets
40 const irept::subt &exception_list=
41 instruction.code.find(ID_exception_list).get_sub();
42
43 assert(exception_list.size()==instruction.targets.size());
44
45 unsigned i=0;
46
47 for(goto_programt::targetst::const_iterator
48 it=instruction.targets.begin();
49 it!=instruction.targets.end();
50 it++, i++)
51 frame.target_map[exception_list[i].id()]=*it;
52 }
53 #endif
54}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
This class represents an instruction in the GOTO intermediate representation.
const goto_instruction_codet & code() const
Get the code represented by this instruction.
targetst targets
The list of successor instructions.
Central data structure: state.
void symex_catch(statet &state)
Symbolically execute a CATCH instruction.
Symbolic Execution.