CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
symex_throw.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 #if 0
17 const goto_programt::instructiont &instruction=*state.source.pc;
18
19 // get the list of exceptions thrown
21 instruction.code.find(ID_exception_list).get_sub();
22
23 // go through the call stack, beginning with the top
24
25 for(goto_symex_statet::call_stackt::const_reverse_iterator
26 s_it=state.call_stack.rbegin();
27 s_it!=state.call_stack.rend();
28 s_it++)
29 {
30 const goto_symex_statet::framet &frame=*s_it;
31
32 if(frame.catch_map.empty())
33 continue;
34
35 for(irept::subt::const_iterator
36 e_it=exceptions_thrown.begin();
38 e_it++)
39 {
40 goto_symex_statet::framet::catch_mapt::const_iterator
41 c_it=frame.catch_map.find(e_it->id());
42
43 if(c_it!=frame.catch_map.end())
44 {
45 // found -- these are always forward gotos
46 }
47 }
48 }
49 #endif
50
51 // An un-caught exception. Behaves like assume(0);
53}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
The Boolean constant false.
Definition std_expr.h:3199
This class represents an instruction in the GOTO intermediate representation.
const goto_instruction_codet & code() const
Get the code represented by this instruction.
Central data structure: state.
call_stackt & call_stack()
symex_targett::sourcet source
void symex_throw(statet &state)
Symbolically execute a THROW instruction.
void symex_assume_l2(statet &, const exprt &cond)
Symbolic Execution.
goto_programt::const_targett pc