39 exprt normalized_expr = expr;
42 bool checked_when_taken =
true;
45 while(normalized_expr.
id() == ID_not)
48 checked_when_taken = !checked_when_taken;
51 if(normalized_expr.
id() == ID_equal)
53 normalized_expr.
id(ID_notequal);
54 checked_when_taken = !checked_when_taken;
57 if(normalized_expr.
id() == ID_notequal)
62 if(op0.
type().
id() == ID_pointer &&
65 return { { checked_when_taken, op1 } };
68 if(op1.
type().
id() == ID_pointer &&
71 return { { checked_when_taken, op0 } };
85 std::set<exprt, type_comparet> checked_expressions(
type_comparet{});
90 if(instruction.incoming_edges.size() > 1)
91 checked_expressions.clear();
93 else if(instruction.is_target())
97 checked_expressions = findit->second;
100 checked_expressions = std::set<exprt, type_comparet>(
type_comparet{});
105 if(!checked_expressions.empty())
108 instruction.location_number, checked_expressions);
111 switch(instruction.type())
132 if(assume_check->checked_when_taken)
133 checked_expressions.insert(assume_check->checked_expr);
139 if(!instruction.is_backwards_goto())
143 auto target_emplace_result =
145 instruction.get_target()->location_number, checked_expressions);
149 if(target_emplace_result.second)
152 auto conditional_check =
157 if(conditional_check->checked_when_taken)
159 target_emplace_result.first->second.insert(
160 conditional_check->checked_expr);
163 checked_expressions.insert(conditional_check->checked_expr);
179 checked_expressions.clear();
195 for(
const auto &instruction : goto_program.
instructions)
197 out <<
"**** " << instruction.location_number <<
" "
198 << instruction.source_location() <<
"\n";
200 out <<
"Non-null expressions: ";
209 for(
const exprt &expr : findit->second)
239 for(
const auto &instruction : goto_program.
instructions)
241 out <<
"**** " << instruction.location_number <<
" "
242 << instruction.source_location() <<
"\n";
244 out <<
"Safe (known-not-null) dereferences: ";
253 instruction.apply([&first, &out](
const exprt &e) {
255 subexpr_it != subexpr_end;
258 if(subexpr_it->id() == ID_dereference)
263 format_rec(out, to_dereference_expr(*subexpr_it).pointer());
Base class for all expressions.
depth_iteratort depth_end()
depth_iteratort depth_begin()
typet & type()
Return the type of the expression.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
instructionst::const_iterator const_targett
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
const irep_idt & id() const
void output_safe_dereferences(std::ostream &stream, const goto_programt &program, const namespacet &ns)
Output safely dereferenced expressions per instruction in human-readable format.
void operator()(const goto_programt &goto_program)
Compute safe dereference expressions for a given GOTO program.
bool is_non_null_at_program_point(const exprt &expr, goto_programt::const_targett program_point)
Return true if the local-safe-pointers analysis has determined expr cannot be null as of program_poin...
void output(std::ostream &stream, const goto_programt &program, const namespacet &ns)
Output non-null expressions per instruction in human-readable format.
std::map< unsigned, std::set< exprt, type_comparet > > non_null_expressions
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The null pointer constant.
Forward depth-first search iterators These iterators' copy operations are expensive,...
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Deprecated expression utility functions.
static optionalt< goto_null_checkt > get_null_checked_expr(const exprt &expr)
Check if expr tests if a pointer is null.
Local safe pointer analysis.
nonstd::optional< T > optionalt
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Return structure for get_null_checked_expr and get_conditional_checked_expr
bool checked_when_taken
If true, the given GOTO/ASSUME tests that a pointer expression is non-null on the taken branch or pas...
exprt checked_expr
Null-tested pointer expression.
Comparator that regards type-equal expressions as equal, and otherwise uses the natural (operator<) o...