cprover
Classes | Public Types | Public Member Functions | Protected Types | Protected Member Functions | Protected Attributes | List of all members
goto_checkt Class Reference
+ Collaboration diagram for goto_checkt:

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< exprt > assertionst
 
typedef optionst::value_listt error_labelst
 
typedef std::pair< exprt, exprt > allocationt
 
typedef std::list< allocationt > allocationst
 

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 namespacet & ns
 
std::unique_ptr< local_bitvector_analysist > local_bitvector_analysis
 
goto_programt::const_targett current_target
 
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 40 of file goto_check.cpp.

Member Typedef Documentation

◆ allocationst

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

Definition at line 158 of file goto_check.cpp.

◆ allocationt

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

Definition at line 157 of file goto_check.cpp.

◆ assertionst

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

Definition at line 129 of file goto_check.cpp.

◆ conditionst

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

Definition at line 102 of file goto_check.cpp.

◆ error_labelst

typedef optionst::value_listt goto_checkt::error_labelst
protected

Definition at line 152 of file goto_check.cpp.

◆ goto_functiont

typedef goto_functionst::goto_functiont goto_checkt::goto_functiont

Definition at line 74 of file goto_check.cpp.

Constructor & Destructor Documentation

◆ goto_checkt()

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

Definition at line 43 of file goto_check.cpp.

Member Function Documentation

◆ add_guarded_claim()

void goto_checkt::add_guarded_claim ( const exprt &  expr,
const std::string &  comment,
const std::string &  property_class,
const source_locationt &  source_location,
const exprt &  src_expr,
const guardt &  guard 
)
protected

Definition at line 1242 of file goto_check.cpp.

◆ address_check()

goto_checkt::conditionst goto_checkt::address_check ( const exprt &  address,
const exprt &  size 
)
protected

Definition at line 954 of file goto_check.cpp.

◆ array_name()

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

Definition at line 1065 of file goto_check.cpp.

◆ bounds_check()

void goto_checkt::bounds_check ( const index_exprt &  expr,
const guardt &  guard 
)
protected

Definition at line 1070 of file goto_check.cpp.

◆ check()

void goto_checkt::check ( const exprt &  expr)
protected

Definition at line 1489 of file goto_check.cpp.

◆ check_rec()

void goto_checkt::check_rec ( const exprt &  expr,
guardt &  guard,
bool  address 
)
protected

Definition at line 1290 of file goto_check.cpp.

◆ collect_allocations()

void goto_checkt::collect_allocations ( const goto_functionst &  goto_functions)

Definition at line 164 of file goto_check.cpp.

◆ conversion_check()

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

Definition at line 351 of file goto_check.cpp.

◆ div_by_zero_check()

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

Definition at line 229 of file goto_check.cpp.

◆ float_overflow_check()

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

Definition at line 644 of file goto_check.cpp.

◆ goto_check()

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

Definition at line 1516 of file goto_check.cpp.

◆ integer_overflow_check()

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

Definition at line 523 of file goto_check.cpp.

◆ invalidate()

void goto_checkt::invalidate ( const exprt &  lhs)
protected

Definition at line 196 of file goto_check.cpp.

◆ mod_by_zero_check()

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

Definition at line 326 of file goto_check.cpp.

◆ nan_check()

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

Definition at line 766 of file goto_check.cpp.

◆ pointer_overflow_check()

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

Definition at line 903 of file goto_check.cpp.

◆ pointer_rel_check()

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

Definition at line 873 of file goto_check.cpp.

◆ pointer_validity_check()

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

Definition at line 929 of file goto_check.cpp.

◆ rw_ok_check()

void goto_checkt::rw_ok_check ( exprt &  expr)
protected

expand the r_ok and w_ok predicates

Definition at line 1496 of file goto_check.cpp.

◆ undefined_shift_check()

void goto_checkt::undefined_shift_check ( const shift_exprt &  expr,
const guardt &  guard 
)
protected

Definition at line 254 of file goto_check.cpp.

Member Data Documentation

◆ allocations

allocationst goto_checkt::allocations
protected

Definition at line 159 of file goto_check.cpp.

◆ assertions

assertionst goto_checkt::assertions
protected

Definition at line 130 of file goto_check.cpp.

◆ current_target

goto_programt::const_targett goto_checkt::current_target
protected

Definition at line 83 of file goto_check.cpp.

◆ enable_assert_to_assume

bool goto_checkt::enable_assert_to_assume
protected

Definition at line 147 of file goto_check.cpp.

◆ enable_assertions

bool goto_checkt::enable_assertions
protected

Definition at line 148 of file goto_check.cpp.

◆ enable_assumptions

bool goto_checkt::enable_assumptions
protected

Definition at line 150 of file goto_check.cpp.

◆ enable_bounds_check

bool goto_checkt::enable_bounds_check
protected

Definition at line 134 of file goto_check.cpp.

◆ enable_built_in_assertions

bool goto_checkt::enable_built_in_assertions
protected

Definition at line 149 of file goto_check.cpp.

◆ enable_conversion_check

bool goto_checkt::enable_conversion_check
protected

Definition at line 141 of file goto_check.cpp.

◆ enable_div_by_zero_check

bool goto_checkt::enable_div_by_zero_check
protected

Definition at line 137 of file goto_check.cpp.

◆ enable_float_overflow_check

bool goto_checkt::enable_float_overflow_check
protected

Definition at line 143 of file goto_check.cpp.

◆ enable_memory_leak_check

bool goto_checkt::enable_memory_leak_check
protected

Definition at line 136 of file goto_check.cpp.

◆ enable_nan_check

bool goto_checkt::enable_nan_check
protected

Definition at line 145 of file goto_check.cpp.

◆ enable_pointer_check

bool goto_checkt::enable_pointer_check
protected

Definition at line 135 of file goto_check.cpp.

◆ enable_pointer_overflow_check

bool goto_checkt::enable_pointer_overflow_check
protected

Definition at line 140 of file goto_check.cpp.

◆ enable_signed_overflow_check

bool goto_checkt::enable_signed_overflow_check
protected

Definition at line 138 of file goto_check.cpp.

◆ enable_simplify

bool goto_checkt::enable_simplify
protected

Definition at line 144 of file goto_check.cpp.

◆ enable_undefined_shift_check

bool goto_checkt::enable_undefined_shift_check
protected

Definition at line 142 of file goto_check.cpp.

◆ enable_unsigned_overflow_check

bool goto_checkt::enable_unsigned_overflow_check
protected

Definition at line 139 of file goto_check.cpp.

◆ error_labels

error_labelst goto_checkt::error_labels
protected

Definition at line 153 of file goto_check.cpp.

◆ local_bitvector_analysis

std::unique_ptr<local_bitvector_analysist> goto_checkt::local_bitvector_analysis
protected

Definition at line 82 of file goto_check.cpp.

◆ mode

irep_idt goto_checkt::mode
protected

Definition at line 161 of file goto_check.cpp.

◆ new_code

goto_programt goto_checkt::new_code
protected

Definition at line 128 of file goto_check.cpp.

◆ ns

const namespacet& goto_checkt::ns
protected

Definition at line 81 of file goto_check.cpp.

◆ retain_trivial

bool goto_checkt::retain_trivial
protected

Definition at line 146 of file goto_check.cpp.

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