CBMC: /home/runner/work/cbmc/cbmc/src/goto-symex/symex_catch.cpp Source File

14 void goto_symext::symex_catch(statet &)

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

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

Definition ai.h:566

goto_programt::instructiont

This class represents an instruction in the GOTO intermediate representation.

Definition goto_program.h:180

goto_programt::instructiont::code

const goto_instruction_codet & code() const

Get the code represented by this instruction.

Definition goto_program.h:187

goto_programt::instructiont::targets

targetst targets

The list of successor instructions.

Definition goto_program.h:413

goto_symex_statet

Central data structure: state.

Definition goto_symex_state.h:42

goto_symext::symex_catch

void symex_catch(statet &state)

Symbolically execute a CATCH instruction.

Definition symex_catch.cpp:14

sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >::subt

typename dt::subt subt

Definition irep.h:152

goto_symex.h

Symbolic Execution.