cprover
Loading...
Searching...
No Matches
goto_check_javat Class Reference
+ Collaboration diagram for goto_check_javat:

Classes

struct  conditiont
 

Public Types

typedef goto_functionst::goto_functiont goto_functiont
 

Public Member Functions

 goto_check_javat (const namespacet &_ns, const optionst &_options, message_handlert &_message_handler)
 
void goto_check (const irep_idt &function_identifier, goto_functiont &goto_function)
 

Protected Types

using conditionst = std::list< conditiont >
 
typedef std::set< std::pair< exprt, exprt > > assertionst
 
typedef optionst::value_listt error_labelst
 

Protected Member Functions

void check_rec_address (const exprt &expr)
 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.
 
bool check_rec_member (const member_exprt &member)
 Check that a member expression is valid:
 
void check_rec_div (const div_exprt &div_expr)
 Check that a division is valid: check for division by zero, overflow and NaN (for floating point numbers).
 
void check_rec_arithmetic_op (const exprt &expr)
 Check that an arithmetic operation is valid: overflow check, NaN-check (for floating point numbers), and pointer overflow check.
 
void check_rec (const exprt &expr)
 Recursively descend into expr and run the appropriate check for each sub-expression, while collecting the condition for the check in guard.
 
void check (const exprt &expr)
 Initiate the recursively analysis of expr with its ‘guard’ set to TRUE.
 
void bounds_check (const exprt &)
 
void bounds_check_index (const index_exprt &)
 
void div_by_zero_check (const div_exprt &)
 
void mod_overflow_check (const mod_exprt &)
 check a mod expression for the case INT_MIN % -1
 
void pointer_validity_check (const dereference_exprt &expr, const exprt &src_expr)
 Generates VCCs for the validity of the given dereferencing operation.
 
optionalt< goto_check_javat::conditiontget_pointer_is_null_condition (const exprt &address, const exprt &size)
 
conditionst get_pointer_dereferenceable_conditions (const exprt &address, const exprt &size)
 
void integer_overflow_check (const exprt &)
 
void conversion_check (const exprt &)
 
void float_overflow_check (const exprt &)
 
void nan_check (const exprt &)
 
optionalt< exprtrw_ok_check (exprt)
 expand the r_ok, w_ok and rw_ok predicates
 
std::string array_name (const exprt &)
 
void add_property (const exprt &asserted_expr, const std::string &comment, const std::string &property_class, const source_locationt &source_location, const exprt &src_expr)
 Include the asserted_expr in the code conditioned by the guard.
 
void invalidate (const exprt &lhs)
 Remove all assertions containing the symbol in lhs as well as all assertions containing dereference.
 

Protected Attributes

const namespacetns
 
std::unique_ptr< local_bitvector_analysistlocal_bitvector_analysis
 
goto_programt::const_targett current_target
 
messaget log
 
goto_programt new_code
 
assertionst assertions
 
bool enable_bounds_check
 
bool enable_pointer_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_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
 

Detailed Description

Definition at line 46 of file goto_check_java.cpp.

Member Typedef Documentation

◆ assertionst

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

Definition at line 178 of file goto_check_java.cpp.

◆ conditionst

Definition at line 136 of file goto_check_java.cpp.

◆ error_labelst

◆ goto_functiont

Constructor & Destructor Documentation

◆ goto_check_javat()

goto_check_javat::goto_check_javat ( const namespacet _ns,
const optionst _options,
message_handlert _message_handler 
)
inline

Definition at line 49 of file goto_check_java.cpp.

Member Function Documentation

◆ add_property()

void goto_check_javat::add_property ( const exprt asserted_expr,
const std::string &  comment,
const std::string &  property_class,
const source_locationt source_location,
const exprt src_expr 
)
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

Definition at line 1077 of file goto_check_java.cpp.

◆ array_name()

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

Definition at line 920 of file goto_check_java.cpp.

◆ bounds_check()

void goto_check_javat::bounds_check ( const exprt expr)
protected

Definition at line 925 of file goto_check_java.cpp.

◆ bounds_check_index()

void goto_check_javat::bounds_check_index ( const index_exprt expr)
protected

Definition at line 941 of file goto_check_java.cpp.

◆ check()

void goto_check_javat::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 1250 of file goto_check_java.cpp.

◆ check_rec()

void goto_check_javat::check_rec ( const exprt expr)
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

Definition at line 1197 of file goto_check_java.cpp.

◆ check_rec_address()

void goto_check_javat::check_rec_address ( const exprt expr)
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

Definition at line 1110 of file goto_check_java.cpp.

◆ check_rec_arithmetic_op()

void goto_check_javat::check_rec_arithmetic_op ( const exprt expr)
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

Definition at line 1184 of file goto_check_java.cpp.

◆ check_rec_div()

void goto_check_javat::check_rec_div ( const div_exprt div_expr)
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

Definition at line 1171 of file goto_check_java.cpp.

◆ check_rec_member()

bool goto_check_javat::check_rec_member ( const member_exprt member)
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
    Returns
    true if no more checks are required for member or its sub-expressions

Definition at line 1133 of file goto_check_java.cpp.

◆ conversion_check()

void goto_check_javat::conversion_check ( const exprt expr)
protected

Definition at line 285 of file goto_check_java.cpp.

◆ div_by_zero_check()

void goto_check_javat::div_by_zero_check ( const div_exprt expr)
protected

Definition at line 237 of file goto_check_java.cpp.

◆ float_overflow_check()

void goto_check_javat::float_overflow_check ( const exprt expr)
protected

Definition at line 657 of file goto_check_java.cpp.

◆ get_pointer_dereferenceable_conditions()

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

Definition at line 908 of file goto_check_java.cpp.

◆ get_pointer_is_null_condition()

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

Definition at line 1588 of file goto_check_java.cpp.

◆ goto_check()

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

Definition at line 1292 of file goto_check_java.cpp.

◆ integer_overflow_check()

void goto_check_javat::integer_overflow_check ( const exprt expr)
protected

Definition at line 441 of file goto_check_java.cpp.

◆ invalidate()

void goto_check_javat::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 207 of file goto_check_java.cpp.

◆ mod_overflow_check()

void goto_check_javat::mod_overflow_check ( const mod_exprt expr)
protected

check a mod expression for the case INT_MIN % -1

Definition at line 256 of file goto_check_java.cpp.

◆ nan_check()

void goto_check_javat::nan_check ( const exprt expr)
protected

Definition at line 761 of file goto_check_java.cpp.

◆ pointer_validity_check()

void goto_check_javat::pointer_validity_check ( const dereference_exprt expr,
const exprt src_expr 
)
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

Definition at line 868 of file goto_check_java.cpp.

◆ rw_ok_check()

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

expand the r_ok, w_ok and rw_ok predicates

Definition at line 1256 of file goto_check_java.cpp.

Member Data Documentation

◆ assertions

assertionst goto_check_javat::assertions
protected

Definition at line 179 of file goto_check_java.cpp.

◆ current_target

goto_programt::const_targett goto_check_javat::current_target
protected

Definition at line 85 of file goto_check_java.cpp.

◆ enable_assert_to_assume

bool goto_check_javat::enable_assert_to_assume
protected

Definition at line 198 of file goto_check_java.cpp.

◆ enable_assertions

bool goto_check_javat::enable_assertions
protected

Definition at line 199 of file goto_check_java.cpp.

◆ enable_assumptions

bool goto_check_javat::enable_assumptions
protected

Definition at line 201 of file goto_check_java.cpp.

◆ enable_bounds_check

bool goto_check_javat::enable_bounds_check
protected

Definition at line 187 of file goto_check_java.cpp.

◆ enable_built_in_assertions

bool goto_check_javat::enable_built_in_assertions
protected

Definition at line 200 of file goto_check_java.cpp.

◆ enable_conversion_check

bool goto_check_javat::enable_conversion_check
protected

Definition at line 193 of file goto_check_java.cpp.

◆ enable_div_by_zero_check

bool goto_check_javat::enable_div_by_zero_check
protected

Definition at line 189 of file goto_check_java.cpp.

◆ enable_float_overflow_check

bool goto_check_javat::enable_float_overflow_check
protected

Definition at line 194 of file goto_check_java.cpp.

◆ enable_nan_check

bool goto_check_javat::enable_nan_check
protected

Definition at line 196 of file goto_check_java.cpp.

◆ enable_pointer_check

bool goto_check_javat::enable_pointer_check
protected

Definition at line 188 of file goto_check_java.cpp.

◆ enable_pointer_overflow_check

bool goto_check_javat::enable_pointer_overflow_check
protected

Definition at line 192 of file goto_check_java.cpp.

◆ enable_signed_overflow_check

bool goto_check_javat::enable_signed_overflow_check
protected

Definition at line 190 of file goto_check_java.cpp.

◆ enable_simplify

bool goto_check_javat::enable_simplify
protected

Definition at line 195 of file goto_check_java.cpp.

◆ enable_unsigned_overflow_check

bool goto_check_javat::enable_unsigned_overflow_check
protected

Definition at line 191 of file goto_check_java.cpp.

◆ error_labels

error_labelst goto_check_javat::error_labels
protected

Definition at line 204 of file goto_check_java.cpp.

◆ local_bitvector_analysis

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

Definition at line 84 of file goto_check_java.cpp.

◆ log

messaget goto_check_javat::log
protected

Definition at line 86 of file goto_check_java.cpp.

◆ new_code

goto_programt goto_check_javat::new_code
protected

Definition at line 177 of file goto_check_java.cpp.

◆ ns

const namespacet& goto_check_javat::ns
protected

Definition at line 83 of file goto_check_java.cpp.

◆ retain_trivial

bool goto_check_javat::retain_trivial
protected

Definition at line 197 of file goto_check_java.cpp.


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