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

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

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, const irep_idt &mode)
 
void check (const exprt &expr, const irep_idt &mode)
 
void bounds_check (const index_exprt &expr, const guardt &guard)
 
void div_by_zero_check (const div_exprt &expr, const guardt &guard)
 
void mod_by_zero_check (const mod_exprt &expr, const guardt &guard)
 
void undefined_shift_check (const shift_exprt &expr, const guardt &guard)
 
void pointer_rel_check (const exprt &expr, const guardt &guard)
 
void pointer_overflow_check (const exprt &expr, const guardt &guard)
 
void pointer_validity_check (const dereference_exprt &expr, const guardt &guard, const exprt &access_lb, const exprt &access_ub, const irep_idt &mode)
 
void integer_overflow_check (const exprt &expr, const guardt &guard)
 
void conversion_check (const exprt &expr, const guardt &guard)
 
void float_overflow_check (const exprt &expr, const guardt &guard)
 
void nan_check (const exprt &expr, const guardt &guard)
 
std::string array_name (const exprt &expr)
 
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)
 

Static Protected Member Functions

static bool has_dereference (const exprt &src)
 

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
 

Detailed Description

Definition at line 33 of file goto_check.cpp.

Member Typedef Documentation

◆ allocationst

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

Definition at line 145 of file goto_check.cpp.

◆ allocationt

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

Definition at line 144 of file goto_check.cpp.

◆ assertionst

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

Definition at line 113 of file goto_check.cpp.

◆ error_labelst

Definition at line 141 of file goto_check.cpp.

◆ goto_functiont

typedef goto_functionst::goto_functiont goto_checkt::goto_functiont

Definition at line 67 of file goto_check.cpp.

Constructor & Destructor Documentation

◆ goto_checkt()

Member Function Documentation

◆ add_guarded_claim()

◆ array_name()

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

Definition at line 1076 of file goto_check.cpp.

References array_name(), and ns.

Referenced by bounds_check().

◆ bounds_check()

◆ check()

void goto_checkt::check ( const exprt expr,
const irep_idt mode 
)
protected

Definition at line 1463 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()

◆ has_dereference()

static bool goto_checkt::has_dereference ( const exprt src)
inlinestaticprotected

Definition at line 118 of file goto_check.cpp.

References has_subexpr().

Referenced by invalidate().

◆ 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()

◆ undefined_shift_check()

Member Data Documentation

◆ allocations

allocationst goto_checkt::allocations
protected

Definition at line 146 of file goto_check.cpp.

Referenced by collect_allocations(), and pointer_validity_check().

◆ assertions

assertionst goto_checkt::assertions
protected

Definition at line 114 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 136 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 137 of file goto_check.cpp.

Referenced by goto_check(), and goto_checkt().

◆ enable_assumptions

bool goto_checkt::enable_assumptions
protected

Definition at line 139 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 123 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 138 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 130 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 126 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 132 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 125 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 134 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 129 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 127 of file goto_check.cpp.

Referenced by goto_checkt(), and integer_overflow_check().

◆ enable_simplify

bool goto_checkt::enable_simplify
protected

Definition at line 133 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 131 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 128 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 142 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 75 of file goto_check.cpp.

Referenced by goto_check(), and pointer_validity_check().

◆ new_code

goto_programt goto_checkt::new_code
protected

Definition at line 112 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 135 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 76 of file goto_check.cpp.

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


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