26 if(type.
id() == ID_array)
28 else if(type.
id() == ID_vector)
41 goto_functionst::function_mapt::value_type &,
49 goto_functionst::function_mapt::value_type &f,
55 if(expr.
id() == ID_index)
62 else if(expr.
id() == ID_member)
78 goto_functionst::function_mapt::value_type &f,
85 if(expr.
id() == ID_address_of)
91 else if(expr.
id() == ID_and)
93 auto new_guards = guards;
97 f, new_guards, op, access_type, ns, dest);
98 new_guards.push_back(op);
102 else if(expr.
id() == ID_or)
104 auto new_guards = guards;
108 f, new_guards, op, access_type, ns, dest);
113 else if(expr.
id() == ID_if)
118 auto new_guards = guards;
119 new_guards.push_back(if_expr.cond());
121 f, new_guards, if_expr.true_case(), access_type, ns, dest);
122 new_guards.pop_back();
123 new_guards.push_back(
not_exprt(if_expr.cond()));
125 f, new_guards, if_expr.false_case(), access_type, ns, dest);
128 else if(expr.
id() == ID_forall || expr.
id() == ID_exists)
137 if(expr.
id() == ID_dereference)
139 if(expr.
type().
id() == ID_code)
146 if(size_opt.has_value())
155 auto pointer_text =
expr2c(pointer, ns);
156 assertion_source_location.set_comment(
157 "pointer " + pointer_text +
" safe");
159 guard(guards, condition), assertion_source_location));
163 else if(expr.
id() == ID_div)
167 div_expr.divisor().is_constant() &&
179 source_location.set_comment(
"division by zero in " +
expr2c(expr, ns));
181 guard(guards, condition), source_location));
184 else if(expr.
id() == ID_mod)
188 mod_expr.divisor().is_constant() &&
199 source_location.set_comment(
"division by zero in " +
expr2c(expr, ns));
201 guard(guards, condition), source_location));
204 else if(expr.
id() == ID_index)
218 source_location.set_comment(
"array bounds in " +
expr2c(expr, ns));
225 goto_functionst::function_mapt::value_type &f,
238 return equal_exprt(std::move(offset), std::move(zero));
242 goto_functionst::function_mapt::value_type &f,
245 auto &body = f.second.body;
248 for(
auto it = body.instructions.begin(); it != body.instructions.end(); it++)
255 else if(it->is_function_call())
259 for(
const auto &argument : it->call_arguments())
264 it->apply([&f, &ns, &dest](
const exprt &expr) {
269 if(it->is_function_call())
271 const auto &
function = it->call_function();
272 if(
function.
id() == ID_symbol)
275 if(identifier ==
"free")
278 it->call_arguments().size() == 1 &&
279 it->call_arguments()[0].type().id() == ID_pointer)
283 const auto &pointer = it->call_arguments()[0];
291 auto source_location = it->source_location();
292 source_location.set_property_class(
"free");
293 source_location.set_comment(
294 "free argument must be valid dynamic object");
298 else if(identifier ==
"realloc")
301 it->call_arguments().size() == 2 &&
302 it->call_arguments()[0].type().id() == ID_pointer)
306 const auto &pointer = it->call_arguments()[0];
314 auto source_location = it->source_location();
315 source_location.set_property_class(
"realloc");
316 source_location.set_comment(
317 "realloc argument must be valid dynamic object");
321 else if(identifier ==
"memcmp")
324 it->call_arguments().size() == 3 &&
325 it->call_arguments()[0].type().id() == ID_pointer &&
326 it->call_arguments()[1].type().id() == ID_pointer &&
327 it->call_arguments()[2].type().id() == ID_unsignedbv)
330 const auto &p1 = it->call_arguments()[0];
331 const auto &p2 = it->call_arguments()[1];
332 const auto &size = it->call_arguments()[2];
335 auto source_location = it->source_location();
336 source_location.set_property_class(
"memcmp");
337 source_location.set_comment(
"memcmp regions must be valid");
341 else if(identifier ==
"memchr")
344 it->call_arguments().size() == 3 &&
345 it->call_arguments()[0].type().id() == ID_pointer &&
346 it->call_arguments()[2].type().id() == ID_unsignedbv)
349 const auto &p = it->call_arguments()[0];
350 const auto &size = it->call_arguments()[2];
352 auto source_location = it->source_location();
353 source_location.set_property_class(
"memchr");
354 source_location.set_comment(
"memchr source must be valid");
358 else if(identifier ==
"memset")
361 it->call_arguments().size() == 3 &&
362 it->call_arguments()[0].type().id() == ID_pointer &&
363 it->call_arguments()[2].type().id() == ID_unsignedbv)
366 const auto &pointer = it->call_arguments()[0];
367 const auto &size = it->call_arguments()[2];
369 auto source_location = it->source_location();
370 source_location.set_property_class(
"memset");
371 source_location.set_comment(
"memset destination must be valid");
375 else if(identifier ==
"strlen")
378 it->call_arguments().size() == 1 &&
379 it->call_arguments()[0].type().id() == ID_pointer)
381 const auto &address = it->call_arguments()[0];
383 auto source_location = it->source_location();
384 source_location.set_property_class(
"strlen");
385 source_location.set_comment(
"strlen argument must be C string");
389 else if(identifier ==
"__builtin___memset_chk")
392 it->call_arguments().size() == 4 &&
393 it->call_arguments()[0].type().id() == ID_pointer &&
394 it->call_arguments()[2].type().id() == ID_unsignedbv)
396 const auto &pointer = it->call_arguments()[0];
397 const auto &size = it->call_arguments()[2];
399 auto source_location = it->source_location();
400 source_location.set_property_class(
"memset");
401 source_location.set_comment(
"memset destination must be valid");
411 body.insert_before_swap(it, dest);
413 it = std::next(it, n);
431 auto &body = f.second.body;
433 for(
auto it = body.instructions.begin(); it != body.instructions.end(); it++)
437 it->source_location().get_property_class() == ID_assertion)
439 it->turn_into_skip();
static exprt guard(const exprt::operandst &guards, exprt cond)
void c_safety_checks_address_rec(goto_functionst::function_mapt::value_type &f, const exprt::operandst &guards, const exprt &expr, const namespacet &ns, goto_programt &dest)
exprt index_array_size(const typet &type)
void c_safety_checks(goto_functionst::function_mapt::value_type &f, const exprt &expr, access_typet access_type, const namespacet &ns, goto_programt &dest)
void no_assertions(goto_functionst::function_mapt::value_type &f)
static exprt offset_is_zero(const exprt &pointer)
void c_safety_checks_rec(goto_functionst::function_mapt::value_type &, const exprt::operandst &guards, const exprt &, access_typet, const namespacet &, goto_programt &)
Checks for Errors in C/C++ Programs.
const exprt & size() const
A base class for relations, i.e., binary predicates whose two operands have the same type.
Base class for all expressions.
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
std::vector< exprt > operandst
const source_locationt & source_location() const
bool is_zero() const
Return whether the expression is a constant representing 0.
typet & type()
Return the type of the expression.
function_mapt function_map
void compute_location_numbers()
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
void clear()
Clear the goto program.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
const irep_idt & id() const
A predicate that indicates that a zero-terminated string starts at the given address.
Evaluates to true if the operand is a pointer to a dynamic object.
A predicate that indicates that the object pointed to is live.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The null pointer constant.
A predicate that indicates that an address range is ok to read.
A base class for a predicate that indicates that an address range is ok to read or write or both.
void set_property_class(const irep_idt &property_class)
const irep_idt & get_identifier() const
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
const constant_exprt & size() const
A predicate that indicates that an address range is ok to write.
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
exprt pointer_offset(const exprt &pointer)
Various predicates over pointers in programs.
#define PRECONDITION(CONDITION)
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.