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: