goto_convert_functions.cpp File Reference

#include <cassert>
#include <goto-programs/destructor.h>
#include <goto-programs/goto_convert_functions.h>
#include <goto-programs/goto_inline.h>
#include <goto-programs/remove_no_op.h>
#include <util/irep/migrate.h>
#include <util/arith/arith_tools.h>
#include <util/expr/base_type.h>
#include <util/lang/c_types.h>
#include <util/base/i2string.h>
#include <util/base/prefix.h>
#include <util/irep/std_code.h>
#include <util/irep/std_expr.h>
#include <util/expr/type_byte_size.h>

Include dependency graph for goto_convert_functions.cpp:

Enumerations
enum class	assert_foldt { none , emitted , defer }

Functions
static void	stamp_value_locations (exprt &expr, const locationt &loc)
static void	restore_sideeffect_location (exprt &op, const locationt &stmt)
static void	restore_value_locations (exprt &code, const locationt &inherited)
static const locationt &	effective_location (const locationt &own, const locationt &inherited)
static void	stamp_ternary_locations (expr2tc &expr, const locationt &loc)
static bool	has_unlocated_ternary (const expr2tc &expr)
static type2tc	stale_symbol_type (const expr2tc &expr, const namespacet &ns)
static bool	has_stale_symbol_type (const expr2tc &expr, const namespacet &ns)
static void	refresh_symbol_types (expr2tc &expr, const namespacet &ns)
static expr2tc	normalise_native_code (const expr2tc &code2, const locationt &loc, const namespacet &ns)
static bool	condition_coverage_enabled (const optionst &options)
static bool	is_ternary (const expr2tc &e)
static bool	is_lone_false_assert (const goto_programt &p)
static bool	is_or_idiom (const goto_programt &then_p, const goto_programt &else_p)
static assert_foldt	fold_assert_branches (goto_programt &then_p, goto_programt &else_p, const expr2tc &cond, goto_programt &dest)
static locationt	emitted_location (const locationt &own)
static const locationt &	statement_location (const expr2tc &code2)
static void	ensure_nonempty (goto_programt &p, const expr2tc &stmt)
void	goto_convert (contextt &context, optionst &options, goto_functionst &functions)
static bool	denotes_thrashable_subtype (const irep_idt &id)

Enumeration Type Documentation

assert_foldt

enum class assert_foldt

strong

Enumerator
none
emitted
defer

Function Documentation

condition_coverage_enabled()

bool condition_coverage_enabled ( const optionst & options )

static

denotes_thrashable_subtype()

bool denotes_thrashable_subtype ( const irep_idt & id )

static

effective_location()

const locationt & effective_location ( const locationt & own, const locationt & inherited )

static

emitted_location()

locationt emitted_location ( const locationt & own )

static

ensure_nonempty()

void ensure_nonempty ( goto_programt & p, const expr2tc & stmt )

static

fold_assert_branches()

assert_foldt fold_assert_branches ( goto_programt & then_p, goto_programt & else_p, const expr2tc & cond, goto_programt & dest )

static

goto_convert()

void goto_convert	(	contextt &	context,
		optionst &	options,
		goto_functionst &	functions )

has_stale_symbol_type()

bool has_stale_symbol_type ( const expr2tc & expr, const namespacet & ns )

static

has_unlocated_ternary()

bool has_unlocated_ternary ( const expr2tc & expr )

static

is_lone_false_assert()

bool is_lone_false_assert ( const goto_programt & p )

static

is_or_idiom()

bool is_or_idiom ( const goto_programt & then_p, const goto_programt & else_p )

static

is_ternary()

bool is_ternary ( const expr2tc & e )

static

normalise_native_code()

expr2tc normalise_native_code ( const expr2tc & code2, const locationt & loc, const namespacet & ns )

static

refresh_symbol_types()

void refresh_symbol_types ( expr2tc & expr, const namespacet & ns )

static

restore_sideeffect_location()

void restore_sideeffect_location ( exprt & op, const locationt & stmt )

static

restore_value_locations()

void restore_value_locations ( exprt & code, const locationt & inherited )

static

stale_symbol_type()

type2tc stale_symbol_type ( const expr2tc & expr, const namespacet & ns )

static

stamp_ternary_locations()

void stamp_ternary_locations ( expr2tc & expr, const locationt & loc )

static

stamp_value_locations()

void stamp_value_locations ( exprt & expr, const locationt & loc )

static

statement_location()

const locationt & statement_location ( const expr2tc & code2 )

static