CBMC: /home/runner/work/cbmc/cbmc/src/ansi-c/goto-conversion/goto_convert.cpp File Reference

CBMC

Loading...

Searching...

No Matches

Classes | Functions

goto_convert.cpp File Reference

Program Transformation. More...

#include "goto_convert.h"
#include "goto_convert_class.h"
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/cprover_prefix.h>
#include <util/exception_utils.h>
#include <util/expr_util.h>
#include <util/fresh_symbol.h>
#include <util/pointer_expr.h>
#include <util/simplify_expr.h>
#include <util/std_expr.h>
#include <util/string_constant.h>
#include <util/symbol_table_builder.h>
#include <goto-programs/remove_skip.h>
#include "destructor.h"

+ 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.

static bool is_size_one (const goto_programt &g)

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

static bool has_and_or (const exprt &expr)

if(guard) goto target;

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 2189 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 2202 of file goto_convert.cpp.

◆ has_and_or()

static bool has_and_or ( const exprt & expr )

static

if(guard) goto target;

Definition at line 1922 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 1749 of file goto_convert.cpp.