cprover
goto_checkt Class Reference
Collaboration diagram for goto_checkt:
[legend]

Classes

struct  conditiont
 

Public Types

typedef goto_functionst::goto_functiont goto_functiont
 

Public Member Functions

 goto_checkt (const namespacet &_ns, const optionst &_options)
 
void goto_check (goto_functiont &goto_function, const irep_idt &mode)
 
void collect_allocations (const goto_functionst &goto_functions)
 

Protected Types

using conditionst = std::list< conditiont >
 
typedef std::set< exprtassertionst
 
typedef optionst::value_listt error_labelst
 
typedef std::pair< exprt, exprtallocationt
 
typedef std::list< allocationtallocationst
 

Protected Member Functions

void check_rec (const exprt &expr, guardt &guard, bool address)
 
void check (const exprt &expr)
 
void bounds_check (const index_exprt &, const guardt &)
 
void div_by_zero_check (const div_exprt &, const guardt &)
 
void mod_by_zero_check (const mod_exprt &, const guardt &)
 
void undefined_shift_check (const shift_exprt &, const guardt &)
 
void pointer_rel_check (const exprt &, const guardt &)
 
void pointer_overflow_check (const exprt &, const guardt &)
 
void pointer_validity_check (const dereference_exprt &, const guardt &)
 
conditionst address_check (const exprt &address, const exprt &size)
 
void integer_overflow_check (const exprt &, const guardt &)
 
void conversion_check (const exprt &, const guardt &)
 
void float_overflow_check (const exprt &, const guardt &)
 
void nan_check (const exprt &, const guardt &)
 
void rw_ok_check (exprt &)
 expand the r_ok and w_ok predicates More...
 
std::string array_name (const exprt &)
 
void add_guarded_claim (const exprt &expr, const std::string &comment, const std::string &property_class, const source_locationt &, const exprt &src_expr, const guardt &guard)
 
void invalidate (const exprt &lhs)
 

Protected Attributes

const namespacetns
 
local_bitvector_analysistlocal_bitvector_analysis
 
goto_programt::const_targett t
 
goto_programt new_code
 
assertionst assertions
 
bool enable_bounds_check
 
bool enable_pointer_check
 
bool enable_memory_leak_check
 
bool enable_div_by_zero_check
 
bool enable_signed_overflow_check
 
bool enable_unsigned_overflow_check
 
bool enable_pointer_overflow_check
 
bool enable_conversion_check
 
bool enable_undefined_shift_check
 
bool enable_float_overflow_check
 
bool enable_simplify
 
bool enable_nan_check
 
bool retain_trivial
 
bool enable_assert_to_assume
 
bool enable_assertions
 
bool enable_built_in_assertions
 
bool enable_assumptions
 
error_labelst error_labels
 
allocationst allocations
 
irep_idt mode
 

Detailed Description

Definition at line 39 of file goto_check.cpp.

Member Typedef Documentation

◆ allocationst

typedef std::list<allocationt> goto_checkt::allocationst
protected

Definition at line 157 of file goto_check.cpp.

◆ allocationt

typedef std::pair<exprt, exprt> goto_checkt::allocationt
protected

Definition at line 156 of file goto_check.cpp.

◆ assertionst

typedef std::set<exprt> goto_checkt::assertionst
protected

Definition at line 128 of file goto_check.cpp.

◆ conditionst

using goto_checkt::conditionst = std::list<conditiont>
protected

Definition at line 101 of file goto_check.cpp.

◆ error_labelst

Definition at line 151 of file goto_check.cpp.

◆ goto_functiont

Constructor & Destructor Documentation

◆ goto_checkt()

Member Function Documentation

◆ add_guarded_claim()

◆ address_check()

◆ array_name()

std::string goto_checkt::array_name ( const exprt expr)
protected

Definition at line 1069 of file goto_check.cpp.

References array_name(), and ns.

Referenced by bounds_check().

◆ bounds_check()

◆ check()

void goto_checkt::check ( const exprt expr)
protected

Definition at line 1497 of file goto_check.cpp.

References check_rec().

Referenced by goto_check().

◆ check_rec()

◆ collect_allocations()

◆ conversion_check()

◆ div_by_zero_check()

void goto_checkt::div_by_zero_check ( const div_exprt expr,
const guardt guard 
)
protected

◆ float_overflow_check()

void goto_checkt::float_overflow_check ( const exprt expr,
const guardt guard 
)
protected

◆ goto_check()

void goto_checkt::goto_check ( goto_functiont goto_function,
const irep_idt mode 
)

Definition at line 1524 of file goto_check.cpp.

References add_guarded_claim(), goto_programt::add_instruction(), code_function_callt::arguments(), ASSERT, assertions, ASSIGN, ASSUME, base_type_eq(), goto_functiont::body, check(), goto_programt::clear(), goto_programt::instructiont::code, CPROVER_PREFIX, local_bitvector_analysist::dirty, enable_assert_to_assume, enable_assertions, enable_assumptions, enable_built_in_assertions, enable_memory_leak_check, enable_pointer_check, goto_functionst::entry_point(), error_labels, Forall_goto_program_instructions, forall_operands, goto_programt::instructiont::function, code_function_callt::function(), local_bitvector_analysist::get(), irept::get(), irept::get_bool(), source_locationt::get_property_class(), codet::get_statement(), goto_program, goto_programt::instructiont::guard, irept::id(), goto_programt::insert_before_swap(), goto_programt::instructions, invalidate(), goto_programt::instructiont::is_assert(), goto_programt::instructiont::is_assign(), goto_programt::instructiont::is_assume(), goto_programt::instructiont::is_dead(), goto_programt::instructiont::is_end_function(), goto_programt::instructiont::is_function_call(), local_bitvector_analysist::flagst::is_null(), goto_programt::instructiont::is_other(), goto_programt::instructiont::is_return(), goto_programt::instructiont::is_target(), goto_programt::instructiont::is_throw(), local_bitvector_analysist::flagst::is_unknown(), goto_programt::instructiont::labels, code_assignt::lhs(), local_bitvector_analysis, namespacet::lookup(), goto_programt::instructiont::make_skip(), exprt::make_typecast(), mode, new_code, ns, exprt::op0(), exprt::operands(), remove_skip(), retain_trivial, code_assignt::rhs(), rw_ok_check(), source_locationt::set_function(), goto_programt::instructiont::source_location, symbolt::symbol_expr(), t, to_code_assign(), to_code_function_call(), to_code_type(), to_pointer_type(), to_symbol_expr(), symbolt::type, and exprt::type().

◆ integer_overflow_check()

◆ invalidate()

void goto_checkt::invalidate ( const exprt lhs)
protected

◆ mod_by_zero_check()

void goto_checkt::mod_by_zero_check ( const mod_exprt expr,
const guardt guard 
)
protected

◆ nan_check()

◆ pointer_overflow_check()

void goto_checkt::pointer_overflow_check ( const exprt expr,
const guardt guard 
)
protected

◆ pointer_rel_check()

void goto_checkt::pointer_rel_check ( const exprt expr,
const guardt guard 
)
protected

◆ pointer_validity_check()

void goto_checkt::pointer_validity_check ( const dereference_exprt expr,
const guardt guard 
)
protected

◆ rw_ok_check()

void goto_checkt::rw_ok_check ( exprt expr)
protected

expand the r_ok and w_ok predicates

Definition at line 1504 of file goto_check.cpp.

References address_check(), conjunction(), DATA_INVARIANT, irept::id(), exprt::op0(), exprt::op1(), and exprt::operands().

Referenced by goto_check().

◆ undefined_shift_check()

Member Data Documentation

◆ allocations

allocationst goto_checkt::allocations
protected

Definition at line 158 of file goto_check.cpp.

Referenced by address_check(), and collect_allocations().

◆ assertions

assertionst goto_checkt::assertions
protected

Definition at line 129 of file goto_check.cpp.

Referenced by add_guarded_claim(), goto_check(), and invalidate().

◆ enable_assert_to_assume

bool goto_checkt::enable_assert_to_assume
protected

Definition at line 146 of file goto_check.cpp.

Referenced by add_guarded_claim(), goto_check(), and goto_checkt().

◆ enable_assertions

bool goto_checkt::enable_assertions
protected

Definition at line 147 of file goto_check.cpp.

Referenced by goto_check(), and goto_checkt().

◆ enable_assumptions

bool goto_checkt::enable_assumptions
protected

Definition at line 149 of file goto_check.cpp.

Referenced by goto_check(), and goto_checkt().

◆ enable_bounds_check

bool goto_checkt::enable_bounds_check
protected

Definition at line 133 of file goto_check.cpp.

Referenced by bounds_check(), and goto_checkt().

◆ enable_built_in_assertions

bool goto_checkt::enable_built_in_assertions
protected

Definition at line 148 of file goto_check.cpp.

Referenced by goto_check(), and goto_checkt().

◆ enable_conversion_check

bool goto_checkt::enable_conversion_check
protected

Definition at line 140 of file goto_check.cpp.

Referenced by conversion_check(), and goto_checkt().

◆ enable_div_by_zero_check

bool goto_checkt::enable_div_by_zero_check
protected

Definition at line 136 of file goto_check.cpp.

Referenced by div_by_zero_check(), goto_checkt(), and mod_by_zero_check().

◆ enable_float_overflow_check

bool goto_checkt::enable_float_overflow_check
protected

Definition at line 142 of file goto_check.cpp.

Referenced by float_overflow_check(), and goto_checkt().

◆ enable_memory_leak_check

bool goto_checkt::enable_memory_leak_check
protected

Definition at line 135 of file goto_check.cpp.

Referenced by goto_check(), and goto_checkt().

◆ enable_nan_check

bool goto_checkt::enable_nan_check
protected

Definition at line 144 of file goto_check.cpp.

Referenced by goto_checkt(), and nan_check().

◆ enable_pointer_check

bool goto_checkt::enable_pointer_check
protected

◆ enable_pointer_overflow_check

bool goto_checkt::enable_pointer_overflow_check
protected

Definition at line 139 of file goto_check.cpp.

Referenced by goto_checkt(), and pointer_overflow_check().

◆ enable_signed_overflow_check

bool goto_checkt::enable_signed_overflow_check
protected

Definition at line 137 of file goto_check.cpp.

Referenced by goto_checkt(), and integer_overflow_check().

◆ enable_simplify

bool goto_checkt::enable_simplify
protected

Definition at line 143 of file goto_check.cpp.

Referenced by add_guarded_claim(), and goto_checkt().

◆ enable_undefined_shift_check

bool goto_checkt::enable_undefined_shift_check
protected

Definition at line 141 of file goto_check.cpp.

Referenced by goto_checkt(), and undefined_shift_check().

◆ enable_unsigned_overflow_check

bool goto_checkt::enable_unsigned_overflow_check
protected

Definition at line 138 of file goto_check.cpp.

Referenced by goto_checkt(), and integer_overflow_check().

◆ error_labels

error_labelst goto_checkt::error_labels
protected

Definition at line 152 of file goto_check.cpp.

Referenced by goto_check(), and goto_checkt().

◆ local_bitvector_analysis

local_bitvector_analysist* goto_checkt::local_bitvector_analysis
protected

Definition at line 81 of file goto_check.cpp.

Referenced by address_check(), and goto_check().

◆ mode

irep_idt goto_checkt::mode
protected

Definition at line 160 of file goto_check.cpp.

Referenced by add_guarded_claim(), address_check(), and goto_check().

◆ new_code

goto_programt goto_checkt::new_code
protected

Definition at line 127 of file goto_check.cpp.

Referenced by add_guarded_claim(), and goto_check().

◆ ns

◆ retain_trivial

bool goto_checkt::retain_trivial
protected

Definition at line 145 of file goto_check.cpp.

Referenced by add_guarded_claim(), goto_check(), and goto_checkt().

◆ t

goto_programt::const_targett goto_checkt::t
protected

Definition at line 82 of file goto_check.cpp.

Referenced by add_guarded_claim(), address_check(), and goto_check().


The documentation for this class was generated from the following file: