goto_check.cpp File Reference

#include <goto-programs/goto_check.h>
#include <cctype>
#include <util/lang/c_builtins.h>
#include <util/lang/c_expr2string.h>
#include <langapi/language_util.h>
#include <util/arith/arith_tools.h>
#include <util/expr/array_name.h>
#include <util/expr/base_type.h>
#include <util/config/config.h>
#include <util/expr/expr_util.h>
#include <irep2/irep2_guard.h>
#include <util/base/i2string.h>
#include <util/irep/location.h>
#include <util/irep/pad_names.h>
#include <util/irep/migrate.h>
#include <util/arith/mp_arith.h>
#include <util/lang/python_types.h>
#include <util/irep/std_types.h>

Include dependency graph for goto_check.cpp:

Classes
class	goto_checkt

Functions
static expr2tc	narrowing_overflow (const expr2tc &value, const type2tc &dst)
	Whether integer value lies outside dst's range; value must be wider than dst, or unsigned and as wide.
static expr2tc	int_encoding_cast_overflow (const expr2tc &cast, const type2tc &dst_type, const type2tc &src_type)
	Under –ir an integer cast is the identity, but the simplifier folds a constant cast with wrap-around, so a signed destination checks the source rather than the result (#8661).
static bool	solidity_skips_overflow_check (const expr2tc &expr, const locationt &loc)
static expr2tc	overflow_expr (const expr2tc &expr)
static bool	is_trailing_member (const type2tc &t, const irep_idt &name)
static bool	may_be_over_allocated (const expr2tc &expr, const namespacet &ns)
static bool	has_checked_operand (const expr2tc &code)
void	goto_check (const namespacet &ns, optionst &options, goto_programt &goto_program)
void	goto_check (const namespacet &ns, optionst &options, goto_functionst &goto_functions)

Function Documentation

goto_check() [1/2]

void goto_check	(	const namespacet &	ns,
		optionst &	options,
		goto_functionst &	goto_functions )

goto_check() [2/2]

void goto_check	(	const namespacet &	ns,
		optionst &	options,
		goto_programt &	goto_program )

has_checked_operand()

bool has_checked_operand ( const expr2tc & code )

static

int_encoding_cast_overflow()

expr2tc int_encoding_cast_overflow ( const expr2tc & cast, const type2tc & dst_type, const type2tc & src_type )

static

Under –ir an integer cast is the identity, but the simplifier folds a constant cast with wrap-around, so a signed destination checks the source rather than the result (#8661).

Nil when the cast cannot overflow.

is_trailing_member()

bool is_trailing_member ( const type2tc & t, const irep_idt & name )

static

may_be_over_allocated()

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

static

narrowing_overflow()

expr2tc narrowing_overflow ( const expr2tc & value, const type2tc & dst )

static

Whether integer value lies outside dst's range; value must be wider than dst, or unsigned and as wide.

overflow_cast tests only the unsigned range of its width, so a signed destination is spelled out in value's own type (#8661).

overflow_expr()

expr2tc overflow_expr ( const expr2tc & expr )

static

solidity_skips_overflow_check()

bool solidity_skips_overflow_check ( const expr2tc & expr, const locationt & loc )

static