ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
goto_checkt Class Reference

Public Member Functions

 goto_checkt (const namespacet &_ns, optionst &_options)
void goto_check (goto_programt &goto_program)

Protected Member Functions

void check (const expr2tc &expr, const locationt &location)
void check_rec (const expr2tc &expr, guard2tc &guard, const locationt &loc, bool address)
void div_by_zero_check (const expr2tc &expr, const guard2tc &guard, const locationt &loc)
void bounds_check (const expr2tc &expr, const guard2tc &guard, const locationt &loc)
void pointer_rel_check (const expr2tc &expr, const guard2tc &guard, const locationt &loc)
void overflow_check (const expr2tc &expr, const guard2tc &guard, const locationt &loc)
void float_overflow_check (const expr2tc &expr, const guard2tc &guard, const locationt &loc)
void cast_overflow_check (const expr2tc &expr, const guard2tc &guard, const locationt &loc)
void fp_to_int_range_check (const expr2tc &expr, const guard2tc &guard, const locationt &loc)
 check a floating-point value converts into the destination integer type
void input_overflow_check (const expr2tc &expr, const locationt &loc)
 check for the buffer overflow in scanf/fscanf
void clz_zero_check (const expr2tc &code, const locationt &loc)
 check __builtin_clz* is not called with a zero argument (UB)
void input_overflow_check_int (const BigInt &width, const BigInt &limit, bool &buf_overflow)
void input_overflow_check_arr (const BigInt &width, const BigInt &limit, bool &buf_overflow)
void shift_check (const expr2tc &expr, const guard2tc &guard, const locationt &loc)
void nan_check (const expr2tc &expr, const guard2tc &guard, const locationt &loc)
void is_instance_check (goto_programt::targett target, goto_programt &goto_program, const expr2tc &lhs, const expr2tc &rhs, const locationt &loc)
expr2tc build_python_type_assertion (const expr2tc &value_expr, const symbolt &symbol) const
expr2tc build_python_isinstance_check (const expr2tc &value_expr, const typet &annotated_type) const
expr2tc build_python_is_none_check (const expr2tc &value_expr) const
bool python_should_skip_type_assertion (const typet &annotated_type) const
typet resolve_python_effective_type (const typet &annotated_type) const
expr2tc build_python_type_operand (const typet &type) const
void add_guarded_claim (const expr2tc &expr, const std::string &comment, const std::string &property, const locationt &location, const guard2tc &guard)

Protected Attributes

const namespacet & ns
optionst & options
goto_programt new_code
std::set< expr2tc > assertions
bool disable_bounds_check
bool disable_pointer_check
bool disable_div_by_zero_check
bool disable_pointer_relation_check
bool disable_unlimited_scanf_check
bool enable_overflow_check
bool enable_unsigned_overflow_check
bool enable_ub_shift_check
bool enable_nan_check
bool enable_is_instance_check
bool enable_clz_zero_check
bool disable_fp_conversion_check

Constructor & Destructor Documentation

◆ goto_checkt()

goto_checkt::goto_checkt ( const namespacet & _ns,
optionst & _options )
inline

Member Function Documentation

◆ add_guarded_claim()

void goto_checkt::add_guarded_claim ( const expr2tc & expr,
const std::string & comment,
const std::string & property,
const locationt & location,
const guard2tc & guard )
protected

◆ bounds_check()

void goto_checkt::bounds_check ( const expr2tc & expr,
const guard2tc & guard,
const locationt & loc )
protected

◆ build_python_is_none_check()

expr2tc goto_checkt::build_python_is_none_check ( const expr2tc & value_expr) const
protected

◆ build_python_isinstance_check()

expr2tc goto_checkt::build_python_isinstance_check ( const expr2tc & value_expr,
const typet & annotated_type ) const
protected

◆ build_python_type_assertion()

expr2tc goto_checkt::build_python_type_assertion ( const expr2tc & value_expr,
const symbolt & symbol ) const
protected

◆ build_python_type_operand()

expr2tc goto_checkt::build_python_type_operand ( const typet & type) const
protected

◆ cast_overflow_check()

void goto_checkt::cast_overflow_check ( const expr2tc & expr,
const guard2tc & guard,
const locationt & loc )
protected

◆ check()

void goto_checkt::check ( const expr2tc & expr,
const locationt & location )
protected

◆ check_rec()

void goto_checkt::check_rec ( const expr2tc & expr,
guard2tc & guard,
const locationt & loc,
bool address )
protected

◆ clz_zero_check()

void goto_checkt::clz_zero_check ( const expr2tc & code,
const locationt & loc )
protected

check __builtin_clz* is not called with a zero argument (UB)

◆ div_by_zero_check()

void goto_checkt::div_by_zero_check ( const expr2tc & expr,
const guard2tc & guard,
const locationt & loc )
protected

◆ float_overflow_check()

void goto_checkt::float_overflow_check ( const expr2tc & expr,
const guard2tc & guard,
const locationt & loc )
protected

◆ fp_to_int_range_check()

void goto_checkt::fp_to_int_range_check ( const expr2tc & expr,
const guard2tc & guard,
const locationt & loc )
protected

check a floating-point value converts into the destination integer type

C11 6.3.1.4p1 and [conv.fpint]/1: converting a floating value whose integral part is not representable in the destination integer type is undefined.

cast_overflow_check's bitvector check is gated on –int-encoding, so in the default mode this conversion went unchecked (#7572). A NaN operand fails both comparisons, which is right – it is equally undefined.

–no-fp-conversion-check exists for SV-COMP: its no-overflow property is only about signed-integer arithmetic, and the rules say so explicitly – "Hence, conversions to signed-integer types do not violate this property." esbmc-wrapper.py reports any violated property under that run as FALSE_OVERFLOW, so leaving this on turns a real conversion UB into a wrong competition verdict.

◆ goto_check()

void goto_checkt::goto_check ( goto_programt & goto_program)

◆ input_overflow_check()

void goto_checkt::input_overflow_check ( const expr2tc & expr,
const locationt & loc )
protected

check for the buffer overflow in scanf/fscanf

◆ input_overflow_check_arr()

void goto_checkt::input_overflow_check_arr ( const BigInt & width,
const BigInt & limit,
bool & buf_overflow )
protected

◆ input_overflow_check_int()

void goto_checkt::input_overflow_check_int ( const BigInt & width,
const BigInt & limit,
bool & buf_overflow )
protected

◆ is_instance_check()

void goto_checkt::is_instance_check ( goto_programt::targett target,
goto_programt & goto_program,
const expr2tc & lhs,
const expr2tc & rhs,
const locationt & loc )
protected

◆ nan_check()

void goto_checkt::nan_check ( const expr2tc & expr,
const guard2tc & guard,
const locationt & loc )
protected

◆ overflow_check()

void goto_checkt::overflow_check ( const expr2tc & expr,
const guard2tc & guard,
const locationt & loc )
protected

◆ pointer_rel_check()

void goto_checkt::pointer_rel_check ( const expr2tc & expr,
const guard2tc & guard,
const locationt & loc )
protected

◆ python_should_skip_type_assertion()

bool goto_checkt::python_should_skip_type_assertion ( const typet & annotated_type) const
protected

◆ resolve_python_effective_type()

typet goto_checkt::resolve_python_effective_type ( const typet & annotated_type) const
protected

◆ shift_check()

void goto_checkt::shift_check ( const expr2tc & expr,
const guard2tc & guard,
const locationt & loc )
protected

Member Data Documentation

◆ assertions

std::set<expr2tc> goto_checkt::assertions
protected

◆ disable_bounds_check

bool goto_checkt::disable_bounds_check
protected

◆ disable_div_by_zero_check

bool goto_checkt::disable_div_by_zero_check
protected

◆ disable_fp_conversion_check

bool goto_checkt::disable_fp_conversion_check
protected

◆ disable_pointer_check

bool goto_checkt::disable_pointer_check
protected

◆ disable_pointer_relation_check

bool goto_checkt::disable_pointer_relation_check
protected

◆ disable_unlimited_scanf_check

bool goto_checkt::disable_unlimited_scanf_check
protected

◆ enable_clz_zero_check

bool goto_checkt::enable_clz_zero_check
protected

◆ enable_is_instance_check

bool goto_checkt::enable_is_instance_check
protected

◆ enable_nan_check

bool goto_checkt::enable_nan_check
protected

◆ enable_overflow_check

bool goto_checkt::enable_overflow_check
protected

◆ enable_ub_shift_check

bool goto_checkt::enable_ub_shift_check
protected

◆ enable_unsigned_overflow_check

bool goto_checkt::enable_unsigned_overflow_check
protected

◆ new_code

goto_programt goto_checkt::new_code
protected

◆ ns

const namespacet& goto_checkt::ns
protected

◆ options

optionst& goto_checkt::options
protected
The documentation for this class was generated from the following file: