Loading...

Searching...

No Matches

remove_exceptions.h

Go to the documentation of this file.

1/*******************************************************************\

2

3Module: Remove function exceptional returns

4

5Author: Cristina David

6

7Date: December 2016

8

9\*******************************************************************/

10

13

14#ifndef CPROVER_JAVA_BYTECODE_REMOVE_EXCEPTIONS_H

15#define CPROVER_JAVA_BYTECODE_REMOVE_EXCEPTIONS_H

16

17#include <util/irep.h>

18

19class class_hierarchyt;

20class goto_modelt;

21class goto_programt;

22class message_handlert;

23class symbol_table_baset;

24

25 #define INFLIGHT_EXCEPTION_VARIABLE_BASENAME "@inflight_exception"

26 #define INFLIGHT_EXCEPTION_VARIABLE_NAME \

27 "java::" INFLIGHT_EXCEPTION_VARIABLE_BASENAME

28

32void remove_exceptions_using_instanceof(

33 const irep_idt &function_identifier,

34 goto_programt &,

35 symbol_table_baset &,

36 message_handlert &);

37

41void remove_exceptions_using_instanceof(goto_modelt &, message_handlert &);

42

46void remove_exceptions(

47 const irep_idt &function_identifier,

48 goto_programt &,

49 symbol_table_baset &,

50 const class_hierarchyt &,

51 message_handlert &);

52

56void remove_exceptions(

57 goto_modelt &,

58 const class_hierarchyt &,

59 message_handlert &);

60

61#endif

class_hierarchyt

Non-graph-based representation of the class hierarchy.

Definition class_hierarchy.h:41

dstringt

dstringt has one field, an unsigned integer no which is an index into a static table of strings.

Definition dstring.h:38

goto_modelt

Definition goto_model.h:27

goto_programt

A generic container class for the GOTO intermediate representation of one function.

Definition goto_program.h:72

message_handlert

Definition message.h:27

symbol_table_baset

The symbol table base class interface.

Definition symbol_table_base.h:23

irep.h

remove_exceptions

void remove_exceptions(const irep_idt &function_identifier, goto_programt &, symbol_table_baset &, const class_hierarchyt &, message_handlert &)

Removes 'throw x' and CATCH-PUSH/CATCH-POP and adds the required instrumentation (GOTOs and assignmen...

Definition remove_exceptions.cpp:723

remove_exceptions_using_instanceof

void remove_exceptions_using_instanceof(const irep_idt &function_identifier, goto_programt &, symbol_table_baset &, message_handlert &)

Removes 'throw x' and CATCH-PUSH/CATCH-POP and adds the required instrumentation (GOTOs and assignmen...

Definition remove_exceptions.cpp:656

CBMC: /home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/remove_exceptions.h Source File