ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
add_restrict_assertions.h
Go to the documentation of this file.
1#ifndef CPROVER_GOTO_PROGRAMS_ADD_RESTRICT_ASSERTIONS_H
2#define CPROVER_GOTO_PROGRAMS_ADD_RESTRICT_ASSERTIONS_H
3
4#include <goto-programs/goto_functions.h>
5#include <util/symtab/context.h>
6
30void add_restrict_assertions(
31 contextt &context,
32 goto_functionst &goto_functions);
33
44void add_restrict_assumptions(
45 contextt &context,
46 goto_functionst &goto_functions,
47 const std::string &entry);
48
49#endif
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 parameter...
Definition add_restrict_assertions.cpp:165
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 as...
Definition add_restrict_assertions.cpp:160
contextt
Definition context.h:57
goto_functionst
Definition goto_functions.h:56
goto_functions.h