add_restrict_assertions.h File Reference

#include <goto-programs/goto_functions.h>
#include <util/symtab/context.h>

Include dependency graph for add_restrict_assertions.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions
void	add_restrict_assertions (contextt &context, goto_functionst &goto_functions)
	Instrument every function that has two or more restrict-qualified pointer parameters with an entry assertion that the objects they point at do not overlap.
void	add_restrict_assumptions (contextt &context, goto_functionst &goto_functions, const std::string &entry)
	The dual, for the entry function only: assume the same disjointness of its restrict pointer parameters rather than assert it.

Function Documentation

add_restrict_assertions()

void add_restrict_assertions	(	contextt &	context,
		goto_functionst &	goto_functions )

Instrument every function that has two or more restrict-qualified pointer parameters with an entry assertion that the objects they point at do not overlap.

Aliasing restrict pointers whose accessed regions overlap are undefined behaviour (C11 6.7.3.1); this catches the classic case, e.g. void f(int *restrict a, int *restrict b) called with f(&x, &x).

Only function-parameter aliasing is checked: two non-null restrict pointers must not have overlapping element footprints (sizeof(*p) bytes, or one byte for incomplete/void subtypes) within a shared object. The footprint is an under-approximation of the accessed region, so a genuinely disjoint use is never flagged, and null parameters (which designate no object) are exempt.

The check over-approximates the modification clause of C11 6.7.3.1p4: it fires on overlap regardless of whether the body performs a modifying access. const-qualified targets are intentionally not exempt — 6.7.3.1p4 makes even a const access path undefined once the shared object is modified by any means, which this pass cannot rule out. The pass is opt-in via --restrict-check.

The #restricted qualifier survives only on the legacy code_typet of the function symbol, so the parameter types are read from context, not from the migrated goto_functiont::type.

add_restrict_assumptions()

void add_restrict_assumptions	(	contextt &	context,
		goto_functionst &	goto_functions,
		const std::string &	entry )

The dual, for the entry function only: assume the same disjointness of its restrict pointer parameters rather than assert it.

A conforming caller may not pass aliasing restrict pointers (C11 6.7.3.1p4), but ESBMC synthesises the caller when the entry point takes parameters, so it is free to pick aliasing values and report a counterexample the standard forbids (esbmc/esbmc#1146). Opt-in via --restrict-assume.

Restricted to entry (a function base name) on purpose: assuming this program-wide would discard genuinely aliasing internal call sites, which are exactly the undefined behaviour --restrict-check exists to find.