62 "symbol is not tracked :" +
from_expr(
ns,
"", symbol_expr));
96 .get_directed_graph();
101 if(
sym.is_static_lifetime)
103 auto fname =
sym.location.get_function();
153 for(
const auto &target :
group.targets())
181 const std::string &suffix,
190 const exprt &condition,
191 const exprt &target)
const
194 const auto &valid_var =
198 const auto &lower_bound_var =
202 const auto &upper_bound_var =
226 "no definite size for lvalue target:\n" + target.
pretty());
262 car.lower_bound_var(),
car.target_start_address(), source_location));
267 car.upper_bound_var(),
308 std::string
comment =
"Check that ";
311 if(!
car.condition().is_true())
343 std::string
comment =
"Check that ";
346 if(!
car.condition().is_true())
374 pointer_offset(car.lower_bound_var())},
376 pointer_offset(car.upper_bound_var()),
377 pointer_offset(candidate_car.upper_bound_var())}}},
433 const exprt &condition,
440 log.
warning() <<
"Ignored duplicate expression '"
442 <<
"' in assigns clause spec at "
444 return found->second;
459 log.
warning() <<
"Ignored duplicate stack-allocated target '"
462 return found->second;
477 log.
warning() <<
"Ignored duplicate heap-allocated target '"
480 return found->second;
501 not_exprt{same_object(
502 tracked_car.lower_bound_var(), freed_car.lower_bound_var())}},
pointer_typet pointer_type(const typet &subtype)
signedbv_typet signed_size_type()
bitvector_typet char_type()
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
static call_grapht create_from_root_function(const goto_modelt &model, const irep_idt &root, bool collect_callsites)
Class that represents a normalized conditional address range, with:
Allows to clean expressions of side effects.
Class that represents a single conditional target.
A class for an expression that represents a conditional target or a list of targets sharing a common ...
Base class for all expressions.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
The Boolean constant false.
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
void invalidate_stack_allocated(const symbol_exprt &symbol_expr, goto_programt &dest)
Generate instructions to invalidate a stack-allocated object that goes DEAD in dest.
const goto_functionst & functions
Other functions of the model.
void track_spec_target(const exprt &expr, goto_programt &dest)
Track an assigns clause target and generate snaphsot instructions and well-definedness assertions in ...
symbol_exprt_to_car_mapt from_stack_alloc
Map to from DECL symbols to corresponding conditional address ranges.
void track_stack_allocated(const symbol_exprt &symbol_expr, goto_programt &dest)
Track a stack-allocated object and generate snaphsot instructions in dest.
void inclusion_check_assertion(const car_exprt &lhs, bool allow_null_lhs, bool include_stack_allocated, optionalt< cfg_infot > &cfg_info_opt, goto_programt &dest) const
Returns an inclusion check assertion of lhs over all tracked cars.
cond_target_exprt_to_car_mapt from_spec_assigns
Map to from conditional target expressions of assigns clauses to corresponding conditional address ra...
void track_heap_allocated(const exprt &expr, goto_programt &dest)
Track a whole heap-alloc object and generate snaphsot instructions in dest.
const car_exprt & create_car_from_spec_assigns(const exprt &condition, const exprt &target)
void invalidate_car(const car_exprt &tracked_car, const car_exprt &freed_car, goto_programt &result) const
Adds an assignment in dest to invalidate the tracked car if was valid before and was pointing to the ...
exprt_to_car_mapt from_heap_alloc
Map to from malloc'd symbols to corresponding conditional address ranges.
car_exprt create_car_expr(const exprt &condition, const exprt &target) const
Creates a conditional address range expression from a cleaned-up condition and target expression.
void track_spec_target_group(const conditional_target_group_exprt &group, goto_programt &dest)
Track and generate snaphsot instructions and target validity checking assertions for a conditional ta...
void target_validity_assertion(const car_exprt &car, bool allow_null_target, goto_programt &dest) const
Generates the target validity assertion for the given car and adds it to dest.
exprt inclusion_check_full(const car_exprt &lhs, bool allow_null_lhs, bool include_stack_allocated, optionalt< cfg_infot > &cfg_info_opt) const
Returns an inclusion check expression of lhs over all tracked cars.
void track_static_locals(goto_programt &dest)
Search the call graph reachable from the instrumented function to identify local static variables use...
void track_plain_spec_target(const exprt &expr, goto_programt &dest)
Track and generate snaphsot instructions and target validity checking assertions for a conditional ta...
const symbolt create_fresh_symbol(const std::string &suffix, const typet &type, const source_locationt &location) const
Creates a fresh symbolt with given suffix, scoped to function_id.
void invalidate_heap_and_spec_aliases(const car_exprt &freed_car, goto_programt &dest) const
Generates instructions to invalidate all targets aliased with a car that was passed to free,...
const car_exprt & create_car_from_stack_alloc(const symbol_exprt &target)
const car_exprt & create_car_from_heap_alloc(const exprt &target)
exprt inclusion_check_single(const car_exprt &lhs, const car_exprt &candidate_car) const
Returns inclusion check expression for a single candidate location.
const namespacet ns
Program namespace.
exprt target_validity_expr(const car_exprt &car, bool allow_null_target) const
Returns the target validity expression for a car_exprt.
void create_snapshot(const car_exprt &car, goto_programt &dest) const
Returns snapshot instructions for a car_exprt.
symbol_tablet & st
Program symbol table.
const irep_idt & function_id
Name of the instrumented function.
void check_inclusion_assignment(const exprt &lhs, optionalt< cfg_infot > &cfg_info_opt, goto_programt &dest)
Generates inclusion check instructions for an assignment, havoc or havoc_object instruction.
bool stack_allocated_is_tracked(const symbol_exprt &symbol_expr) const
Returns true if the expression is tracked.
void check_inclusion_heap_allocated_and_invalidate_aliases(const exprt &expr, optionalt< cfg_infot > &cfg_info_opt, goto_programt &dest)
Generates inclusion check instructions for an argument passed to free.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const irept & find(const irep_idt &name) const
const irep_idt & id() const
Binary less than or equal operator expression.
message_handlert & get_message_handler()
mstreamt & warning() const
The plus expression Associativity is not specified.
void set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
const irep_idt & get_function() const
std::string as_string() const
const irep_idt & get_comment() const
void set_function(const irep_idt &function)
Expression to hold a symbol (variable)
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
irep_idt mode
Language mode.
The Boolean constant true.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
A predicate that indicates that an address range is ok to write.
bool is_assignable(const exprt &expr)
Returns true iff the argument is one of the following:
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Deprecated expression utility functions.
Specify write set in function contracts.
const std::string & id2string(const irep_idt &d)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
exprt pointer_offset(const exprt &pointer)
exprt object_size(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
exprt null_pointer(const exprt &pointer)
Various predicates over pointers in programs.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
exprt simplify_expr(exprt src, const namespacet &ns)
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
#define UNREACHABLE
This should be used to mark dead code.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
void add_pragma_disable_pointer_checks(source_locationt &location)
Adds a pragma on a source location disable all pointer checks.
const symbolt & new_tmp_symbol(const typet &type, const source_locationt &location, const irep_idt &mode, symbol_table_baset &symtab, std::string suffix, bool is_auxiliary)
Adds a fresh and uniquely named symbol to the symbol table.
bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment)
Returns true if the given comment matches the type of comments created by make_assigns_clause_replace...
void add_pragma_disable_assigns_check(source_locationt &location)
Adds a pragma on a source_locationt to disable inclusion checking.