CBMC
goto_convert.cpp File Reference

Program Transformation. More...

+ Include dependency graph for goto_convert.cpp:

Go to the source code of this file.

Classes

struct  build_declaration_hops_inputst
 

Functions

static bool is_empty (const goto_programt &goto_program)
 
static void finish_catch_push_targets (goto_programt &dest)
 Populate the CATCH instructions with the targets corresponding to their associated labels. More...
 
static bool is_size_one (const goto_programt &g)
 This is (believed to be) faster than using std::list.size. More...
 
static bool has_and_or (const exprt &expr)
 if(guard) goto target; More...
 
void goto_convert (const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
 
void goto_convert (symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler)
 

Detailed Description

Program Transformation.

Definition in file goto_convert.cpp.

Function Documentation

◆ finish_catch_push_targets()

static void finish_catch_push_targets ( goto_programt dest)
static

Populate the CATCH instructions with the targets corresponding to their associated labels.

Definition at line 42 of file goto_convert.cpp.

◆ goto_convert() [1/2]

void goto_convert ( const codet code,
symbol_table_baset symbol_table,
goto_programt dest,
message_handlert message_handler,
const irep_idt mode 
)

Definition at line 2187 of file goto_convert.cpp.

◆ goto_convert() [2/2]

void goto_convert ( symbol_table_baset symbol_table,
goto_programt dest,
message_handlert message_handler 
)

Definition at line 2200 of file goto_convert.cpp.

◆ has_and_or()

static bool has_and_or ( const exprt expr)
static

if(guard) goto target;

Definition at line 1920 of file goto_convert.cpp.

◆ is_empty()

static bool is_empty ( const goto_programt goto_program)
static

Definition at line 31 of file goto_convert.cpp.

◆ is_size_one()

static bool is_size_one ( const goto_programt g)
inlinestatic

This is (believed to be) faster than using std::list.size.

parameters: Goto program 'g'
Returns
True if 'g' has one instruction

Definition at line 1747 of file goto_convert.cpp.