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...
 
void pointer_primitive_check (const exprt &expr, const guardt &guard)
 Generates VCCs to check that pointers passed to pointer primitives are either null or valid. More...
 
bool is_pointer_primitive (const exprt &expr)
 Returns true if the given expression is a pointer primitive such as __CPROVER_r_ok() 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
 
bool enable_pointer_primitive_check
 
error_labelst error_labels
 
allocationst allocations
 
irep_idt mode
 

Detailed Description

Definition at line 42 of file goto_check.cpp.

Member Typedef Documentation

◆ allocationst

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

Definition at line 266 of file goto_check.cpp.

◆ allocationt

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

Definition at line 265 of file goto_check.cpp.

◆ assertionst

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

Definition at line 231 of file goto_check.cpp.

◆ conditionst

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

Definition at line 170 of file goto_check.cpp.

◆ error_labelst

Definition at line 260 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 45 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 1581 of file goto_check.cpp.

◆ address_check()

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

Definition at line 1257 of file goto_check.cpp.

◆ array_name()

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

Definition at line 1375 of file goto_check.cpp.

◆ bounds_check()

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

Definition at line 1380 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 1831 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 1755 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 1619 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 1738 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 1725 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 1664 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 1642 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 1687 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 272 of file goto_check.cpp.

◆ conversion_check()

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

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

◆ enum_range_check()

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

Definition at line 351 of file goto_check.cpp.

◆ float_overflow_check()

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

Definition at line 883 of file goto_check.cpp.

◆ goto_check()

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

Definition at line 1900 of file goto_check.cpp.

◆ integer_overflow_check()

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

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

◆ is_pointer_primitive()

bool goto_checkt::is_pointer_primitive ( const exprt expr)
protected

Returns true if the given expression is a pointer primitive such as __CPROVER_r_ok()

Parameters
exprexpression
Returns
true if the given expression is a pointer primitive

Definition at line 1246 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 447 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 469 of file goto_check.cpp.

◆ nan_check()

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

Definition at line 993 of file goto_check.cpp.

◆ pointer_overflow_check()

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

Definition at line 1131 of file goto_check.cpp.

◆ pointer_primitive_check()

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

Generates VCCs to check that pointers passed to pointer primitives are either null or valid.

Parameters
exprthe pointer primitive expression
guardthe condition under which the operation happens

Definition at line 1198 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 1104 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 1157 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 1838 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 380 of file goto_check.cpp.

Member Data Documentation

◆ allocations

allocationst goto_checkt::allocations
protected

Definition at line 267 of file goto_check.cpp.

◆ assertions

assertionst goto_checkt::assertions
protected

Definition at line 232 of file goto_check.cpp.

◆ current_target

goto_programt::const_targett goto_checkt::current_target
protected

Definition at line 96 of file goto_check.cpp.

◆ enable_assert_to_assume

bool goto_checkt::enable_assert_to_assume
protected

Definition at line 254 of file goto_check.cpp.

◆ enable_assertions

bool goto_checkt::enable_assertions
protected

Definition at line 255 of file goto_check.cpp.

◆ enable_assumptions

bool goto_checkt::enable_assumptions
protected

Definition at line 257 of file goto_check.cpp.

◆ enable_bounds_check

bool goto_checkt::enable_bounds_check
protected

Definition at line 240 of file goto_check.cpp.

◆ enable_built_in_assertions

bool goto_checkt::enable_built_in_assertions
protected

Definition at line 256 of file goto_check.cpp.

◆ enable_conversion_check

bool goto_checkt::enable_conversion_check
protected

Definition at line 248 of file goto_check.cpp.

◆ enable_div_by_zero_check

bool goto_checkt::enable_div_by_zero_check
protected

Definition at line 243 of file goto_check.cpp.

◆ enable_enum_range_check

bool goto_checkt::enable_enum_range_check
protected

Definition at line 244 of file goto_check.cpp.

◆ enable_float_overflow_check

bool goto_checkt::enable_float_overflow_check
protected

Definition at line 250 of file goto_check.cpp.

◆ enable_memory_leak_check

bool goto_checkt::enable_memory_leak_check
protected

Definition at line 242 of file goto_check.cpp.

◆ enable_nan_check

bool goto_checkt::enable_nan_check
protected

Definition at line 252 of file goto_check.cpp.

◆ enable_pointer_check

bool goto_checkt::enable_pointer_check
protected

Definition at line 241 of file goto_check.cpp.

◆ enable_pointer_overflow_check

bool goto_checkt::enable_pointer_overflow_check
protected

Definition at line 247 of file goto_check.cpp.

◆ enable_pointer_primitive_check

bool goto_checkt::enable_pointer_primitive_check
protected

Definition at line 258 of file goto_check.cpp.

◆ enable_signed_overflow_check

bool goto_checkt::enable_signed_overflow_check
protected

Definition at line 245 of file goto_check.cpp.

◆ enable_simplify

bool goto_checkt::enable_simplify
protected

Definition at line 251 of file goto_check.cpp.

◆ enable_undefined_shift_check

bool goto_checkt::enable_undefined_shift_check
protected

Definition at line 249 of file goto_check.cpp.

◆ enable_unsigned_overflow_check

bool goto_checkt::enable_unsigned_overflow_check
protected

Definition at line 246 of file goto_check.cpp.

◆ error_labels

error_labelst goto_checkt::error_labels
protected

Definition at line 261 of file goto_check.cpp.

◆ guard_manager

guard_managert goto_checkt::guard_manager
protected

Definition at line 97 of file goto_check.cpp.

◆ local_bitvector_analysis

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

Definition at line 95 of file goto_check.cpp.

◆ mode

irep_idt goto_checkt::mode
protected

Definition at line 269 of file goto_check.cpp.

◆ new_code

goto_programt goto_checkt::new_code
protected

Definition at line 230 of file goto_check.cpp.

◆ no_enum_check

bool goto_checkt::no_enum_check
protected

Definition at line 98 of file goto_check.cpp.

◆ ns

const namespacet& goto_checkt::ns
protected

Definition at line 94 of file goto_check.cpp.

◆ retain_trivial

bool goto_checkt::retain_trivial
protected

Definition at line 253 of file goto_check.cpp.


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