cprover
symex_throw.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
14
void
goto_symext::symex_throw
(
statet
&state)
15
{
16
#if 0
17
const
goto_programt::instructiont
&instruction=*state.
source
.
pc
;
18
19
// get the list of exceptions thrown
20
const
irept::subt
&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();
37
e_it!=exceptions_thrown.end();
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);
52
symex_assume
(state,
false_exprt
());
53
}
symex_targett::sourcet::pc
goto_programt::const_targett pc
Definition:
symex_target.h:41
goto_symex_statet
Definition:
goto_symex_state.h:34
irept::find
const irept & find(const irep_namet &name) const
Definition:
irep.cpp:284
goto_symex_statet::source
symex_targett::sourcet source
Definition:
goto_symex_state.h:58
goto_symex_statet::framet::catch_map
std::map< irep_idt, goto_programt::targett > catch_map
Definition:
goto_symex_state.h:190
goto_symex_statet::call_stack
call_stackt & call_stack()
Definition:
goto_symex_state.h:203
goto_programt::instructiont::code
codet code
Definition:
goto_program.h:181
goto_symex.h
false_exprt
The Boolean constant false.
Definition:
std_expr.h:4452
goto_symext::symex_assume
virtual void symex_assume(statet &, const exprt &cond)
Definition:
symex_main.cpp:101
goto_symext::symex_throw
void symex_throw(statet &)
Definition:
symex_throw.cpp:14
goto_symex_statet::framet
Definition:
goto_symex_state.h:174
irept::get_sub
subt & get_sub()
Definition:
irep.h:317
irept::subt
std::vector< irept > subt
Definition:
irep.h:160
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition:
goto_program.h:178
goto-symex
symex_throw.cpp
Generated by
1.8.17