55 const exprt &denominator,
63 const exprt &tested_expr,
78 "java.lang.ArithmeticException",
79 "java.lang.ArrayIndexOutOfBoundsException",
80 "java.lang.ClassCastException",
81 "java.lang.NegativeArraySizeException",
82 "java.lang.NullPointerException"};
138 const exprt &denominator,
148 "java.lang.ArithmeticException");
183 "java.lang.ArrayIndexOutOfBoundsException");
189 low_check_loc.set_property_class(
"array-index-out-of-bounds-low");
193 high_check_loc.set_property_class(
"array-index-out-of-bounds-high");
212 const exprt &tested_expr,
228 "java.lang.ClassCastException");
233 check_loc.set_comment(
"Dynamic cast check");
234 check_loc.set_property_class(
"bad-dynamic-cast");
269 check_loc.set_comment(
"Null pointer check");
270 check_loc.set_property_class(
"null-pointer-exception");
295 "java.lang.NegativeArraySizeException");
298 check_loc.set_comment(
"Array size should be >= 0");
299 check_loc.set_property_class(
"array-create-negative-size");
479 result.
add(std::move(bounds_check));
522 return std::move(result);
546 const bool throw_runtime_exceptions,
551 throw_runtime_exceptions,
555 "java_bytecode_instrument expects a code-typed symbol but was called with"
556 " " +
id2string(symbol.
name) +
" which has a value with an id of " +
595 const bool throw_runtime_exceptions,
600 throw_runtime_exceptions,
pointer_typet pointer_type(const typet &subtype)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A base class for relations, i.e., binary predicates whose two operands have the same type.
A non-fatal assertion, which checks a condition then permits execution to continue.
A codet representing an assignment in the program.
A codet representing sequential composition of program statements.
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
void add(const codet &code)
codet representation of an expression statement.
codet representation of a function call statement.
codet representation of an if-then-else statement.
codet representation of a label for branch targets.
codet representation of a "return from a function" statement.
codet representing a switch statement.
Data structure for representing an arbitrary statement in a program.
const irep_idt & get_statement() const
A constant literal expression.
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
There are a large number of kinds of tree structured or tree-like data in CPROVER.
bool get_bool(const irep_idt &name) const
const irep_idt & id() const
java_bytecode_instrumentt(symbol_table_baset &_symbol_table, const bool _throw_runtime_exceptions, message_handlert &_message_handler)
codet check_array_access(const exprt &array_struct, const exprt &idx, const source_locationt &original_loc)
Checks whether the array access array_struct[idx] is out-of-bounds, and throws ArrayIndexOutofBoundsE...
void operator()(codet &code)
Instruments code.
void prepend_instrumentation(codet &code, code_blockt &instrumentation)
Appends code to instrumentation and overwrites reference code with the augmented block if instrumenta...
void add_expr_instrumentation(code_blockt &block, const exprt &expr)
Checks whether expr requires instrumentation, and if so adds it to block.
codet check_arithmetic_exception(const exprt &denominator, const source_locationt &original_loc)
Checks whether there is a division by zero and throws ArithmeticException if necessary.
const bool throw_runtime_exceptions
message_handlert & message_handler
codet check_array_length(const exprt &length, const source_locationt &original_loc)
Checks whether length >= 0 and throws NegativeArraySizeException/ generates an assertion when necessa...
void instrument_code(codet &code)
Augments code with instrumentation in the form of either assertions or runtime exceptions.
code_ifthenelset throw_exception(const exprt &cond, const source_locationt &original_loc, const irep_idt &exc_name)
Creates a class stub for exc_name and generates a conditional GOTO such that exc_name is thrown when ...
code_ifthenelset check_class_cast(const exprt &tested_expr, const struct_tag_typet &target_type, const source_locationt &original_loc)
Checks whether class1 is an instance of class2 and throws ClassCastException/generates an assertion w...
codet check_null_dereference(const exprt &expr, const source_locationt &original_loc)
Checks whether expr is null and throws NullPointerException/ generates an assertion when necessary; E...
symbol_table_baset & symbol_table
optionalt< codet > instrument_expr(const exprt &expr)
Computes the instrumentation for expr in the form of either assertions or runtime exceptions.
Extract member of struct or union.
The null pointer constant.
The plus expression Associativity is not specified.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
A side_effect_exprt representation of a side effect that throws an exception.
An expression containing a side effect.
A struct tag type, i.e., struct_typet with an identifier.
std::vector< componentt > componentst
The symbol table base class interface.
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
irep_idt name
The unique identifier.
exprt value
Initial value of symbol.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
#define forall_operands(it, expr)
#define Forall_operands(it, expr)
const code_function_callt & to_code_function_call(const codet &code)
const code_assignt & to_code_assign(const codet &code)
const code_returnt & to_code_return(const codet &code)
const std::string & id2string(const irep_idt &d)
void java_bytecode_instrument_symbol(symbol_table_baset &symbol_table, symbolt &symbol, const bool throw_runtime_exceptions, message_handlert &message_handler)
Instruments the code attached to symbol with runtime exceptions or corresponding assertions.
void java_bytecode_instrument_uncaught_exceptions(code_blockt &init_code, const symbolt &exc_symbol, const source_locationt &source_location)
Instruments the start function with an assertion that checks whether an exception has escaped the ent...
void java_bytecode_instrument(symbol_tablet &symbol_table, const bool throw_runtime_exceptions, message_handlert &message_handler)
Instruments all the code in the symbol_table with runtime exceptions or corresponding assertions.
const std::vector< std::string > exception_needed_classes
Java-specific exprt subclasses.
const java_instanceof_exprt & to_java_instanceof_expr(const exprt &expr)
Cast an exprt to a java_instanceof_exprt.
signedbv_typet java_int_type()
empty_typet java_void_type()
const java_method_typet & to_java_method_type(const typet &type)
void generate_class_stub(const irep_idt &class_name, symbol_table_baset &symbol_table, message_handlert &message_handler, const struct_union_typet::componentst &componentst)
symbolt & fresh_java_symbol(const typet &type, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &function_name, symbol_table_baset &symbol_table)
void merge_source_location_rec(exprt &expr, const source_locationt &source_location)
Attaches a source location to an expression and all of its subexpressions.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
code_blockt create_fatal_assertion(const exprt &condition, const source_locationt &loc)
Create a fatal assertion, which checks a condition and then halts if it does not hold.
side_effect_exprt & to_side_effect_expr(exprt &expr)
const code_assertt & to_code_assert(const codet &code)
const code_labelt & to_code_label(const codet &code)
const code_blockt & to_code_block(const codet &code)
const code_ifthenelset & to_code_ifthenelse(const codet &code)
const code_switcht & to_code_switch(const codet &code)
code_expressiont & to_code_expression(codet &code)
const codet & to_code(const exprt &expr)
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
void check_code(const codet &code, const validation_modet vm)
Check that the given code statement is well-formed (shallow checks only, i.e., enclosed statements,...