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< std::pair< exprt, exprt > > assertionst
 
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 exprt &, const guardt &)
 
void bounds_check_index (const index_exprt &, const guardt &)
 
void bounds_check_bit_count (const unary_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_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...
 
optionalt< goto_checkt::conditiontget_pointer_is_null_condition (const exprt &address, const exprt &size)
 
conditionst get_pointer_points_to_valid_memory_conditions (const exprt &address, const exprt &size)
 
exprt is_in_bounds_of_some_explicit_allocation (const exprt &pointer, const exprt &size)
 
conditionst get_pointer_dereferenceable_conditions (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, w_ok and rw_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 45 of file goto_check.cpp.

Member Typedef Documentation

◆ allocationst

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

Definition at line 282 of file goto_check.cpp.

◆ allocationt

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

Definition at line 281 of file goto_check.cpp.

◆ assertionst

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

Definition at line 247 of file goto_check.cpp.

◆ conditionst

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

Definition at line 173 of file goto_check.cpp.

◆ error_labelst

Definition at line 276 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 48 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 1543 of file goto_check.cpp.

◆ array_name()

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

Definition at line 1342 of file goto_check.cpp.

◆ bounds_check()

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

Definition at line 1347 of file goto_check.cpp.

◆ bounds_check_bit_count()

void goto_checkt::bounds_check_bit_count ( const unary_exprt expr,
const guardt guard 
)
protected

Definition at line 1521 of file goto_check.cpp.

◆ bounds_check_index()

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

Definition at line 1368 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 1806 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 1725 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 1581 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 1700 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 1687 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 1626 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 1604 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 1649 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 288 of file goto_check.cpp.

◆ conversion_check()

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

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

◆ enum_range_check()

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

Definition at line 377 of file goto_check.cpp.

◆ float_overflow_check()

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

Definition at line 938 of file goto_check.cpp.

◆ get_pointer_dereferenceable_conditions()

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

Definition at line 1329 of file goto_check.cpp.

◆ get_pointer_is_null_condition()

optionalt< goto_checkt::conditiont > goto_checkt::get_pointer_is_null_condition ( const exprt address,
const exprt size 
)
protected

Definition at line 2321 of file goto_check.cpp.

◆ get_pointer_points_to_valid_memory_conditions()

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

Definition at line 2238 of file goto_check.cpp.

◆ goto_check()

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

Definition at line 1875 of file goto_check.cpp.

◆ integer_overflow_check()

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

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

◆ is_in_bounds_of_some_explicit_allocation()

exprt goto_checkt::is_in_bounds_of_some_explicit_allocation ( const exprt pointer,
const exprt size 
)
protected

Definition at line 2348 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 1318 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 473 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 495 of file goto_check.cpp.

◆ nan_check()

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

Definition at line 1048 of file goto_check.cpp.

◆ pointer_overflow_check()

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

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

◆ pointer_rel_check()

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

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

◆ rw_ok_check()

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

expand the r_ok, w_ok and rw_ok predicates

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

Member Data Documentation

◆ allocations

allocationst goto_checkt::allocations
protected

Definition at line 283 of file goto_check.cpp.

◆ assertions

assertionst goto_checkt::assertions
protected

Definition at line 248 of file goto_check.cpp.

◆ current_target

goto_programt::const_targett goto_checkt::current_target
protected

Definition at line 99 of file goto_check.cpp.

◆ enable_assert_to_assume

bool goto_checkt::enable_assert_to_assume
protected

Definition at line 270 of file goto_check.cpp.

◆ enable_assertions

bool goto_checkt::enable_assertions
protected

Definition at line 271 of file goto_check.cpp.

◆ enable_assumptions

bool goto_checkt::enable_assumptions
protected

Definition at line 273 of file goto_check.cpp.

◆ enable_bounds_check

bool goto_checkt::enable_bounds_check
protected

Definition at line 256 of file goto_check.cpp.

◆ enable_built_in_assertions

bool goto_checkt::enable_built_in_assertions
protected

Definition at line 272 of file goto_check.cpp.

◆ enable_conversion_check

bool goto_checkt::enable_conversion_check
protected

Definition at line 264 of file goto_check.cpp.

◆ enable_div_by_zero_check

bool goto_checkt::enable_div_by_zero_check
protected

Definition at line 259 of file goto_check.cpp.

◆ enable_enum_range_check

bool goto_checkt::enable_enum_range_check
protected

Definition at line 260 of file goto_check.cpp.

◆ enable_float_overflow_check

bool goto_checkt::enable_float_overflow_check
protected

Definition at line 266 of file goto_check.cpp.

◆ enable_memory_leak_check

bool goto_checkt::enable_memory_leak_check
protected

Definition at line 258 of file goto_check.cpp.

◆ enable_nan_check

bool goto_checkt::enable_nan_check
protected

Definition at line 268 of file goto_check.cpp.

◆ enable_pointer_check

bool goto_checkt::enable_pointer_check
protected

Definition at line 257 of file goto_check.cpp.

◆ enable_pointer_overflow_check

bool goto_checkt::enable_pointer_overflow_check
protected

Definition at line 263 of file goto_check.cpp.

◆ enable_pointer_primitive_check

bool goto_checkt::enable_pointer_primitive_check
protected

Definition at line 274 of file goto_check.cpp.

◆ enable_signed_overflow_check

bool goto_checkt::enable_signed_overflow_check
protected

Definition at line 261 of file goto_check.cpp.

◆ enable_simplify

bool goto_checkt::enable_simplify
protected

Definition at line 267 of file goto_check.cpp.

◆ enable_undefined_shift_check

bool goto_checkt::enable_undefined_shift_check
protected

Definition at line 265 of file goto_check.cpp.

◆ enable_unsigned_overflow_check

bool goto_checkt::enable_unsigned_overflow_check
protected

Definition at line 262 of file goto_check.cpp.

◆ error_labels

error_labelst goto_checkt::error_labels
protected

Definition at line 277 of file goto_check.cpp.

◆ guard_manager

guard_managert goto_checkt::guard_manager
protected

Definition at line 100 of file goto_check.cpp.

◆ local_bitvector_analysis

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

Definition at line 98 of file goto_check.cpp.

◆ mode

irep_idt goto_checkt::mode
protected

Definition at line 285 of file goto_check.cpp.

◆ new_code

goto_programt goto_checkt::new_code
protected

Definition at line 246 of file goto_check.cpp.

◆ no_enum_check

bool goto_checkt::no_enum_check
protected

Definition at line 101 of file goto_check.cpp.

◆ ns

const namespacet& goto_checkt::ns
protected

Definition at line 97 of file goto_check.cpp.

◆ retain_trivial

bool goto_checkt::retain_trivial
protected

Definition at line 269 of file goto_check.cpp.


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