CBMC
Loading...
Searching...
No Matches
Classes | Functions
remove_exceptions.cpp File Reference

Remove exception handling. More...

#include "remove_exceptions.h"
#include "remove_instanceof.h"
#include <util/c_types.h>
#include <util/pointer_expr.h>
#include <util/std_code.h>
#include <goto-programs/goto_model.h>
#include <goto-programs/remove_skip.h>
#include <analyses/uncaught_exceptions_analysis.h>
#include <linking/static_lifetime_init.h>
#include "java_expr.h"
#include "java_types.h"
+ Include dependency graph for remove_exceptions.cpp:

Go to the source code of this file.

Classes

class   remove_exceptionst
  Lowers high-level exception descriptions into low-level operations suitable for symex and other analyses that don't understand the THROW or CATCH GOTO instructions. More...
 

Functions

void  remove_exceptions_using_instanceof (symbol_table_baset &symbol_table, goto_functionst &goto_functions, message_handlert &message_handler)
  removes throws/CATCH-POP/CATCH-PUSH
 
void  remove_exceptions_using_instanceof (const irep_idt &function_identifier, goto_programt &goto_program, symbol_table_baset &symbol_table, message_handlert &message_handler)
  removes throws/CATCH-POP/CATCH-PUSH from a single GOTO program, replacing them with explicit exception propagation.
 
void  remove_exceptions_using_instanceof (goto_modelt &goto_model, message_handlert &message_handler)
  removes throws/CATCH-POP/CATCH-PUSH, replacing them with explicit exception propagation.
 
void  remove_exceptions (symbol_table_baset &symbol_table, goto_functionst &goto_functions, const class_hierarchyt &class_hierarchy, message_handlert &message_handler)
  removes throws/CATCH-POP/CATCH-PUSH
 
void  remove_exceptions (const irep_idt &function_identifier, goto_programt &goto_program, symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, message_handlert &message_handler)
  removes throws/CATCH-POP/CATCH-PUSH from a single GOTO program, replacing them with explicit exception propagation.
 
void  remove_exceptions (goto_modelt &goto_model, const class_hierarchyt &class_hierarchy, message_handlert &message_handler)
  removes throws/CATCH-POP/CATCH-PUSH, replacing them with explicit exception propagation.
 

Detailed Description

Remove exception handling.

Definition in file remove_exceptions.cpp.

Function Documentation

◆  remove_exceptions() [1/3]

void remove_exceptions ( const irep_idt &  function_identifier,
goto_programt &  goto_program,
symbol_table_baset &  symbol_table,
const class_hierarchyt &  class_hierarchy,
message_handlert &  message_handler 
)

removes throws/CATCH-POP/CATCH-PUSH from a single GOTO program, replacing them with explicit exception propagation.

Removes 'throw x' and CATCH-PUSH/CATCH-POP and adds the required instrumentation (GOTOs and assignments) This does not introduce instanceof expressions.

Note this is somewhat less accurate than the whole-goto-model version, because we can't inspect other functions to determine whether they throw or not, and therefore must assume they do and always introduce post-call exception dispatch.

Parameters
function_identifier name of the goto function being processed
goto_program program to remove exceptions from
symbol_table global symbol table. The @inflight_exception global may be added if not already present. It will not be initialised; that is the caller's responsibility.
class_hierarchy class hierarchy analysis of symbol_table. Only needed if type == REMOVE_ADDED_INSTANCEOF; otherwise may be null.
message_handler logging output

Definition at line 723 of file remove_exceptions.cpp.

◆  remove_exceptions() [2/3]

void remove_exceptions ( goto_modelt &  goto_model,
const class_hierarchyt &  class_hierarchy,
message_handlert &  message_handler 
)

removes throws/CATCH-POP/CATCH-PUSH, replacing them with explicit exception propagation.

Removes 'throw x' and CATCH-PUSH/CATCH-POP and adds the required instrumentation (GOTOs and assignments) This does not introduce instanceof expressions.

Parameters
goto_model model to remove exceptions from. The @inflight_exception global may be added to its symbol table if not already present. It will not be initialised; that is the caller's responsibility.
class_hierarchy class hierarchy analysis of symbol_table. Only needed if type == REMOVE_ADDED_INSTANCEOF; otherwise may be null.
message_handler logging output

Definition at line 752 of file remove_exceptions.cpp.

◆  remove_exceptions() [3/3]

void remove_exceptions ( symbol_table_baset &  symbol_table,
goto_functionst &  goto_functions,
const class_hierarchyt &  class_hierarchy,
message_handlert &  message_handler 
)

removes throws/CATCH-POP/CATCH-PUSH

Definition at line 687 of file remove_exceptions.cpp.

◆  remove_exceptions_using_instanceof() [1/3]

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

removes throws/CATCH-POP/CATCH-PUSH from a single GOTO program, replacing them with explicit exception propagation.

Removes 'throw x' and CATCH-PUSH/CATCH-POP and adds the required instrumentation (GOTOs and assignments) This introduces instanceof expressions.

Note this is somewhat less accurate than the whole-goto-model version, because we can't inspect other functions to determine whether they throw or not, and therefore must assume they do and always introduce post-call exception dispatch.

Parameters
function_identifier name of the goto function being processed
goto_program program to remove exceptions from
symbol_table global symbol table. The @inflight_exception global may be added if not already present. It will not be initialised; that is the caller's responsibility.
message_handler logging output

Definition at line 656 of file remove_exceptions.cpp.

◆  remove_exceptions_using_instanceof() [2/3]

void remove_exceptions_using_instanceof ( goto_modelt &  goto_model,
message_handlert &  message_handler 
)

removes throws/CATCH-POP/CATCH-PUSH, replacing them with explicit exception propagation.

Removes 'throw x' and CATCH-PUSH/CATCH-POP and adds the required instrumentation (GOTOs and assignments) This introduces instanceof expressions.

Parameters
goto_model model to remove exceptions from. The @inflight_exception global may be added to its symbol table if not already present. It will not be initialised; that is the caller's responsibility.
message_handler logging output

Definition at line 678 of file remove_exceptions.cpp.

◆  remove_exceptions_using_instanceof() [3/3]

void remove_exceptions_using_instanceof ( symbol_table_baset &  symbol_table,
goto_functionst &  goto_functions,
message_handlert &  message_handler 
)

removes throws/CATCH-POP/CATCH-PUSH

Definition at line 623 of file remove_exceptions.cpp.

AltStyle によって変換されたページ (->オリジナル) /