cprover
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 (const irep_idt &function_identifier, goto_functiont &goto_function)
 
void collect_allocations (const goto_functionst &goto_functions)
 Fill the list of allocations allocationst with <address, size> for every allocation instruction. More...
 

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_address (const exprt &expr, guardt &guard)
 Check an address-of expression: if it is a dereference then check the pointer if it is an index then address-check the array and then check the index. More...
 
void check_rec_logical_op (const exprt &expr, guardt &guard)
 Check a logical operation: check each operand in separation while extending the guarding condition as follows. More...
 
void check_rec_if (const if_exprt &if_expr, guardt &guard)
 Check an if expression: check the if-condition alone, and then check the true/false-cases with the guard extended with if-condition and it's negation, respectively. More...
 
bool check_rec_member (const member_exprt &member, guardt &guard)
 Check that a member expression is valid: More...
 
void check_rec_div (const div_exprt &div_expr, guardt &guard)
 Check that a division is valid: check for division by zero, overflow and NaN (for floating point numbers). More...
 
void check_rec_arithmetic_op (const exprt &expr, guardt &guard)
 Check that an arithmetic operation is valid: overflow check, NaN-check (for floating point numbers), and pointer overflow check. More...
 
void check_rec (const exprt &expr, guardt &guard)
 Recursively descend into expr and run the appropriate check for each sub-expression, while collecting the condition for the check in guard. More...
 
void check (const exprt &expr)
 Initiate the recursively analysis of expr with its ‘guard’ set to TRUE. More...
 
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 mod_overflow_check (const mod_exprt &, const guardt &)
 check a mod expression for the case INT_MIN % -1 More...
 
void enum_range_check (const exprt &, const guardt &)
 
void undefined_shift_check (const shift_exprt &, const guardt &)
 
void pointer_rel_check (const binary_relation_exprt &, const guardt &)
 
void pointer_overflow_check (const exprt &, const guardt &)
 
void pointer_validity_check (const dereference_exprt &expr, const exprt &src_expr, const guardt &guard)
 Generates VCCs for the validity of the given dereferencing operation. More...
 
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 &)
 
optionalt< exprtrw_ok_check (exprt)
 expand the r_ok and w_ok predicates More...
 
std::string array_name (const exprt &)
 
void add_guarded_property (const exprt &asserted_expr, const std::string &comment, const std::string &property_class, const source_locationt &source_location, const exprt &src_expr, const guardt &guard)
 Include the asserted_expr in the code conditioned by the guard. More...
 
void invalidate (const exprt &lhs)
 Remove all assertions containing the symbol in lhs as well as all assertions containing dereference. More...
 

Protected Attributes

const namespacetns
 
std::unique_ptr< local_bitvector_analysistlocal_bitvector_analysis
 
goto_programt::const_targett current_target
 
guard_managert guard_manager
 
bool no_enum_check
 
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_enum_range_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 41 of file goto_check.cpp.

Member Typedef Documentation

◆ allocationst

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

Definition at line 248 of file goto_check.cpp.

◆ allocationt

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

Definition at line 247 of file goto_check.cpp.

◆ assertionst

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

Definition at line 214 of file goto_check.cpp.

◆ conditionst

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

Definition at line 167 of file goto_check.cpp.

◆ error_labelst

Definition at line 242 of file goto_check.cpp.

◆ goto_functiont

Constructor & Destructor Documentation

◆ goto_checkt()

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

Definition at line 44 of file goto_check.cpp.

Member Function Documentation

◆ add_guarded_property()

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

Include the asserted_expr in the code conditioned by the guard.

Parameters
asserted_exprexpression to be asserted
commenthuman readable comment
property_classclassification of the property
source_locationthe source location of the original expression
src_exprthe original expression to be included in the comment
guardthe condition under which the asserted expression should be taken into account

Definition at line 1499 of file goto_check.cpp.

◆ address_check()

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

Definition at line 1167 of file goto_check.cpp.

◆ array_name()

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

Definition at line 1293 of file goto_check.cpp.

◆ bounds_check()

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

Definition at line 1298 of file goto_check.cpp.

◆ check()

void goto_checkt::check ( const exprt expr)
protected

Initiate the recursively analysis of expr with its ‘guard’ set to TRUE.

Parameters
exprthe expression to be checked

Definition at line 1745 of file goto_check.cpp.

◆ check_rec()

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

Recursively descend into expr and run the appropriate check for each sub-expression, while collecting the condition for the check in guard.

Parameters
exprthe expression to be checked
guardthe condition for when the check should be made

Definition at line 1673 of file goto_check.cpp.

◆ check_rec_address()

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

Check an address-of expression: if it is a dereference then check the pointer if it is an index then address-check the array and then check the index.

Parameters
exprthe expression to be checked
guardthe condition for the check (unmodified here)

Definition at line 1537 of file goto_check.cpp.

◆ check_rec_arithmetic_op()

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

Check that an arithmetic operation is valid: overflow check, NaN-check (for floating point numbers), and pointer overflow check.

Parameters
exprthe expression to be checked
guardthe condition for the check (unmodified here)

Definition at line 1656 of file goto_check.cpp.

◆ check_rec_div()

void goto_checkt::check_rec_div ( const div_exprt div_expr,
guardt guard 
)
protected

Check that a division is valid: check for division by zero, overflow and NaN (for floating point numbers).

Parameters
div_exprthe expression to be checked
guardthe condition for the check (unmodified here)

Definition at line 1643 of file goto_check.cpp.

◆ check_rec_if()

void goto_checkt::check_rec_if ( const if_exprt if_expr,
guardt guard 
)
protected

Check an if expression: check the if-condition alone, and then check the true/false-cases with the guard extended with if-condition and it's negation, respectively.

Parameters
if_exprthe expression to be checked
guardthe condition for the check (extended with the (negation of the) if-condition for recursively calls)

Definition at line 1582 of file goto_check.cpp.

◆ check_rec_logical_op()

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

Check a logical operation: check each operand in separation while extending the guarding condition as follows.

a /\ b /\ c ==> check(a, TRUE), check(b, a), check (c, a /\ b) a \/ b \/ c ==> check(a, TRUE), check(b, ~a), check (c, ~a /\ ~b)

Parameters
exprthe expression to be checked
guardthe condition for the check (extended with the previous operands (or their negations) for recursively calls)

Definition at line 1560 of file goto_check.cpp.

◆ check_rec_member()

bool goto_checkt::check_rec_member ( const member_exprt member,
guardt guard 
)
protected

Check that a member expression is valid:

  • check the structure this expression is a member of (via pointer of its dereference)
  • run pointer-validity check on ‘*(s+member_offset)’ instead of ‘s->member’ to avoid checking safety of ‘s’
  • check all operands of the expression
    Parameters
    memberthe expression to be checked
    guardthe condition for the check (unmodified here)
    Returns
    true if no more checks are required for member or its sub-expressions

Definition at line 1605 of file goto_check.cpp.

◆ collect_allocations()

void goto_checkt::collect_allocations ( const goto_functionst goto_functions)

Fill the list of allocations allocationst with <address, size> for every allocation instruction.

Also check that each allocation is well-formed.

Parameters
goto_functionsgoto functions from which the allocations are to be collected

Definition at line 254 of file goto_check.cpp.

◆ conversion_check()

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

Definition at line 481 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 312 of file goto_check.cpp.

◆ enum_range_check()

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

Definition at line 333 of file goto_check.cpp.

◆ float_overflow_check()

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

Definition at line 865 of file goto_check.cpp.

◆ goto_check()

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

Definition at line 1814 of file goto_check.cpp.

◆ integer_overflow_check()

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

Definition at line 647 of file goto_check.cpp.

◆ invalidate()

void goto_checkt::invalidate ( const exprt lhs)
protected

Remove all assertions containing the symbol in lhs as well as all assertions containing dereference.

Parameters
lhsthe left-hand-side expression whose symbol should be invalidated

Definition at line 286 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 429 of file goto_check.cpp.

◆ mod_overflow_check()

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

check a mod expression for the case INT_MIN % -1

Definition at line 451 of file goto_check.cpp.

◆ nan_check()

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

Definition at line 975 of file goto_check.cpp.

◆ pointer_overflow_check()

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

Definition at line 1113 of file goto_check.cpp.

◆ pointer_rel_check()

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

Definition at line 1086 of file goto_check.cpp.

◆ pointer_validity_check()

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

Generates VCCs for the validity of the given dereferencing operation.

Parameters
exprthe expression to be checked
src_exprThe expression as found in the program, prior to any rewriting
guardthe condition under which the operation happens

Definition at line 1139 of file goto_check.cpp.

◆ rw_ok_check()

optionalt< exprt > goto_checkt::rw_ok_check ( exprt  expr)
protected

expand the r_ok and w_ok predicates

Definition at line 1752 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 362 of file goto_check.cpp.

Member Data Documentation

◆ allocations

allocationst goto_checkt::allocations
protected

Definition at line 249 of file goto_check.cpp.

◆ assertions

assertionst goto_checkt::assertions
protected

Definition at line 215 of file goto_check.cpp.

◆ current_target

goto_programt::const_targett goto_checkt::current_target
protected

Definition at line 93 of file goto_check.cpp.

◆ enable_assert_to_assume

bool goto_checkt::enable_assert_to_assume
protected

Definition at line 237 of file goto_check.cpp.

◆ enable_assertions

bool goto_checkt::enable_assertions
protected

Definition at line 238 of file goto_check.cpp.

◆ enable_assumptions

bool goto_checkt::enable_assumptions
protected

Definition at line 240 of file goto_check.cpp.

◆ enable_bounds_check

bool goto_checkt::enable_bounds_check
protected

Definition at line 223 of file goto_check.cpp.

◆ enable_built_in_assertions

bool goto_checkt::enable_built_in_assertions
protected

Definition at line 239 of file goto_check.cpp.

◆ enable_conversion_check

bool goto_checkt::enable_conversion_check
protected

Definition at line 231 of file goto_check.cpp.

◆ enable_div_by_zero_check

bool goto_checkt::enable_div_by_zero_check
protected

Definition at line 226 of file goto_check.cpp.

◆ enable_enum_range_check

bool goto_checkt::enable_enum_range_check
protected

Definition at line 227 of file goto_check.cpp.

◆ enable_float_overflow_check

bool goto_checkt::enable_float_overflow_check
protected

Definition at line 233 of file goto_check.cpp.

◆ enable_memory_leak_check

bool goto_checkt::enable_memory_leak_check
protected

Definition at line 225 of file goto_check.cpp.

◆ enable_nan_check

bool goto_checkt::enable_nan_check
protected

Definition at line 235 of file goto_check.cpp.

◆ enable_pointer_check

bool goto_checkt::enable_pointer_check
protected

Definition at line 224 of file goto_check.cpp.

◆ enable_pointer_overflow_check

bool goto_checkt::enable_pointer_overflow_check
protected

Definition at line 230 of file goto_check.cpp.

◆ enable_signed_overflow_check

bool goto_checkt::enable_signed_overflow_check
protected

Definition at line 228 of file goto_check.cpp.

◆ enable_simplify

bool goto_checkt::enable_simplify
protected

Definition at line 234 of file goto_check.cpp.

◆ enable_undefined_shift_check

bool goto_checkt::enable_undefined_shift_check
protected

Definition at line 232 of file goto_check.cpp.

◆ enable_unsigned_overflow_check

bool goto_checkt::enable_unsigned_overflow_check
protected

Definition at line 229 of file goto_check.cpp.

◆ error_labels

error_labelst goto_checkt::error_labels
protected

Definition at line 243 of file goto_check.cpp.

◆ guard_manager

guard_managert goto_checkt::guard_manager
protected

Definition at line 94 of file goto_check.cpp.

◆ local_bitvector_analysis

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

Definition at line 92 of file goto_check.cpp.

◆ mode

irep_idt goto_checkt::mode
protected

Definition at line 251 of file goto_check.cpp.

◆ new_code

goto_programt goto_checkt::new_code
protected

Definition at line 213 of file goto_check.cpp.

◆ no_enum_check

bool goto_checkt::no_enum_check
protected

Definition at line 95 of file goto_check.cpp.

◆ ns

const namespacet& goto_checkt::ns
protected

Definition at line 91 of file goto_check.cpp.

◆ retain_trivial

bool goto_checkt::retain_trivial
protected

Definition at line 236 of file goto_check.cpp.


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