36 if(
auto target = expr_try_dynamic_cast<conditional_target_group_exprt>(expr))
62 "symbol is not tracked :" +
from_expr(
ns,
"", symbol_expr));
98 for(
const auto &sym_pair :
st)
100 const auto &sym = sym_pair.second;
101 if(sym.is_static_lifetime)
103 auto fname = sym.location.get_function();
106 (fname ==
function_id || call_graph.get_node_index(fname).has_value()))
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 =
206 if(target.
id() == ID_pointer_object)
226 "no definite size for lvalue target:\n" + target.
pretty());
275 bool allow_null_target)
const
286 if(allow_null_target)
294 bool allow_null_target,
308 std::string
comment =
"Check that ";
326 bool include_stack_allocated,
342 const auto &orig_comment = source_location.
get_comment();
343 std::string
comment =
"Check that ";
358 car, allow_null_lhs, include_stack_allocated, cfg_info_opt),
374 pointer_offset(car.lower_bound_var())},
376 pointer_offset(car.upper_bound_var()),
377 pointer_offset(candidate_car.upper_bound_var())}}},
384 bool include_stack_allocated,
411 if(include_stack_allocated)
417 cfg_info_opt.has_value() &&
418 !cfg_info_opt.value().is_maybe_alive(pair.first))
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.
directed_grapht get_directed_graph() const
Returns a grapht representation of this call graph, suitable for use with generic grapht algorithms.
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:
const symbol_exprt & upper_bound_var() const
Identifier of the upper address bound snapshot variable.
const exprt & target_start_address() const
Start address of the target.
const symbol_exprt & valid_var() const
Identifier of the validity snapshot variable.
const exprt & target() const
The target expression.
const symbol_exprt & lower_bound_var() const
Identifier of the lower address bound snapshot variable.
const exprt & target_size() const
Size of the target in bytes.
const exprt & condition() const
Condition expression. When this condition holds the target is allowed.
Allows to clean expressions of side effects.
void clean(exprt &guard, goto_programt &dest, const irep_idt &mode)
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 ...
const exprt::operandst & targets() const
const exprt & condition() const
Base class for all expressions.
std::vector< exprt > operandst
bool is_true() const
Return whether the expression is a constant representing true.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
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 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)
nonstd::optional< T > optionalt
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.
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.