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())
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 =
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;