39 exprt normalized_expr = expr;
42 bool checked_when_taken =
true;
45 while(normalized_expr.
id() == ID_not)
47 normalized_expr = normalized_expr.
op0();
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, base_type_comparet> checked_expressions(
91 if(instruction.incoming_edges.size() > 1)
92 checked_expressions.clear();
94 else if(instruction.is_target())
98 checked_expressions = findit->second;
101 checked_expressions =
107 if(!checked_expressions.empty())
109 non_null_expressions.emplace(
110 instruction.location_number, checked_expressions);
113 switch(instruction.type)
131 if(assume_check->checked_when_taken)
132 checked_expressions.insert(assume_check->checked_expr);
138 if(!instruction.is_backwards_goto())
142 auto target_emplace_result =
143 non_null_expressions.emplace(
144 instruction.get_target()->location_number, checked_expressions);
148 if(target_emplace_result.second)
154 if(conditional_check->checked_when_taken)
156 target_emplace_result.first->second.insert(
157 conditional_check->checked_expr);
160 checked_expressions.insert(conditional_check->checked_expr);
170 checked_expressions.clear();
185 out <<
"**** " << i_it->location_number <<
" " 186 << i_it->source_location <<
"\n";
188 out <<
"Non-null expressions: ";
197 for(
const exprt &expr : findit->second)
226 out <<
"**** " << i_it->location_number <<
" " 227 << i_it->source_location <<
"\n";
229 out <<
"Safe (known-not-null) dereferences: ";
238 for(
auto subexpr_it = i_it->code.depth_begin(),
239 subexpr_end = i_it->code.depth_end();
240 subexpr_it != subexpr_end;
243 if(subexpr_it->id() == ID_dereference)
269 const exprt *tocheck = &expr;
270 while(tocheck->
id() == ID_typecast)
271 tocheck = &tocheck->
op0();
272 return findit->second.count(*tocheck) != 0;
exprt checked_expr
Null-tested pointer expression.
void output_safe_dereferences(std::ostream &stream, const goto_programt &program)
Output safely dereferenced expressions per instruction in human-readable format.
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Deprecated expression utility functions.
The null pointer constant.
typet & type()
Return the type of the expression.
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
Forward depth-first search iterators These iterators' copy operations are expensive, so use auto&, and avoid std::next(), std::prev() and post-increment iterator.
static optionalt< goto_null_checkt > get_null_checked_expr(const exprt &expr)
Check if expr tests if a pointer is null.
void operator()(const goto_programt &goto_program)
Compute safe dereference expressions for a given GOTO program.
const irep_idt & id() const
nonstd::optional< T > optionalt
instructionst instructions
The list of instructions in the 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...
instructionst::const_iterator const_targett
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
void output(std::ostream &stream, const goto_programt &program)
Output non-null expressions per instruction in human-readable format.
A generic container class for the GOTO intermediate representation of one function.
Return structure for get_null_checked_expr and get_conditional_checked_expr
Base class for all expressions.
bool operator()(const exprt &e1, const exprt &e2) const
bool checked_when_taken
If true, the given GOTO/ASSUME tests that a pointer expression is non-null on the taken branch or pas...
Local safe pointer analysis.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define forall_goto_program_instructions(it, program)
Comparator that regards base_type_eq expressions as equal, and otherwise uses the natural (operator<)...
std::map< unsigned, std::set< exprt, base_type_comparet > > non_null_expressions