cprover
|
#include <vector>
#include <analyses/dirty.h>
#include <analyses/locals.h>
#include <goto-instrument/havoc_utils.h>
#include <goto-programs/goto_convert_class.h>
#include <goto-programs/goto_model.h>
#include <util/expr_cast.h>
#include <util/message.h>
Go to the source code of this file.
Classes | |
class | havoc_if_validt |
A class that overrides the low-level havocing functions in the base utility class, to havoc only when expressions point to valid memory, i.e. More... | |
class | havoc_assigns_targetst |
A class that further overrides the "safe" havoc utilities, and adds support for havocing pointer_object expressions. More... | |
class | cfg_infot |
Stores information about a goto function computed from its CFG, together with a target iterator into the instructions of the function. More... | |
class | cleanert |
Allows to clean expressions of side effects. More... | |
Macros | |
#define | CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK "contracts:disable:assigns-check" |
Functions | |
void | add_pragma_disable_pointer_checks (source_locationt &source_location) |
Adds a pragma on a source location disable all pointer checks. | |
goto_programt::instructiont & | add_pragma_disable_pointer_checks (goto_programt::instructiont &instr) |
Adds pragmas on a GOTO instruction to disable all pointer checks. | |
goto_programt & | add_pragma_disable_pointer_checks (goto_programt &prog) |
Adds pragmas on all instructions in a GOTO program to disable all pointer checks. | |
void | add_pragma_disable_assigns_check (source_locationt &source_location) |
Adds a pragma on a source_locationt to disable inclusion checking. | |
goto_programt::instructiont & | add_pragma_disable_assigns_check (goto_programt::instructiont &instr) |
Adds a pragma on a GOTO instruction to disable inclusion checking. | |
goto_programt & | add_pragma_disable_assigns_check (goto_programt &prog) |
Adds pragmas on all instructions in a GOTO program to disable inclusion checking on them. | |
exprt | all_dereferences_are_valid (const exprt &expr, const namespacet &ns) |
Generate a validity check over all dereferences in an expression. | |
exprt | generate_lexicographic_less_than_check (const std::vector< symbol_exprt > &lhs, const std::vector< symbol_exprt > &rhs) |
Generate a lexicographic less-than comparison over ordered tuples. | |
void | insert_before_swap_and_advance (goto_programt &destination, goto_programt::targett &target, goto_programt &payload) |
Insert a goto program before a target instruction iterator and advance the iterator. | |
const symbolt & | new_tmp_symbol (const typet &type, const source_locationt &location, const irep_idt &mode, symbol_table_baset &symtab, std::string suffix="tmp_cc", bool is_auxiliary=true) |
Adds a fresh and uniquely named symbol to the symbol table. | |
void | simplify_gotos (goto_programt &goto_program, namespacet &ns) |
Turns goto instructions IF cond GOTO label where the condition statically simplifies to false into SKIP instructions. | |
bool | is_loop_free (const goto_programt &goto_program, namespacet &ns, messaget &log) |
Returns true iff the given program is loop-free, i.e. | |
irep_idt | make_assigns_clause_replacement_tracking_comment (const exprt &target, const irep_idt &function_id, const namespacet &ns) |
Returns an irep_idt that essentially says that target was assigned by the contract of function_id . | |
bool | is_assigns_clause_replacement_tracking_comment (const irep_idt &comment) |
Returns true if the given comment matches the type of comments created by make_assigns_clause_replacement_tracking_comment. | |
goto_programt & add_pragma_disable_assigns_check | ( | goto_programt & | prog | ) |
goto_programt::instructiont & add_pragma_disable_assigns_check | ( | goto_programt::instructiont & | instr | ) |
void add_pragma_disable_assigns_check | ( | source_locationt & | source_location | ) |
Adds a pragma on a source_locationt to disable inclusion checking.
goto_programt & add_pragma_disable_pointer_checks | ( | goto_programt & | prog | ) |
goto_programt::instructiont & add_pragma_disable_pointer_checks | ( | goto_programt::instructiont & | instr | ) |
void add_pragma_disable_pointer_checks | ( | source_locationt & | source_location | ) |
exprt all_dereferences_are_valid | ( | const exprt & | expr, |
const namespacet & | ns | ||
) |
Generate a validity check over all dereferences in an expression.
This function generates a formula:
good_pointer_def(pexpr_1, ns) && good_pointer_def(pexpr_2, n2) && ...
over all dereferenced pointer expressions *(pexpr_1), *(pexpr_2), ... found in the AST of expr
.
expr | The expression that contains dereferences to be validated. |
ns | The namespace that defines all symbols appearing in expr . |
expr
. exprt generate_lexicographic_less_than_check | ( | const std::vector< symbol_exprt > & | lhs, |
const std::vector< symbol_exprt > & | rhs | ||
) |
Generate a lexicographic less-than comparison over ordered tuples.
This function creates an expression representing a lexicographic less-than comparison, lhs < rhs, between two ordered tuples of variables. This is used in instrumentation of decreases clauses.
lhs | A vector of variables representing the LHS of the comparison. |
rhs | A vector of variables representing the RHS of the comparison. |
void insert_before_swap_and_advance | ( | goto_programt & | destination, |
goto_programt::targett & | target, | ||
goto_programt & | payload | ||
) |
Insert a goto program before a target instruction iterator and advance the iterator.
This function inserts all instruction from a goto program payload
into a destination program destination
immediately before a specified instruction iterator target
. After insertion, target
is advanced by the size of the payload
, and payload
is destroyed.
destination | The destination program for inserting the payload . |
target | The instruction iterator at which to insert the payload . |
payload | The goto program to be inserted into the destination . |
Returns true if the given comment matches the type of comments created by make_assigns_clause_replacement_tracking_comment.
bool is_loop_free | ( | const goto_programt & | goto_program, |
namespacet & | ns, | ||
messaget & | log | ||
) |
irep_idt make_assigns_clause_replacement_tracking_comment | ( | const exprt & | target, |
const irep_idt & | function_id, | ||
const namespacet & | ns | ||
) |
const symbolt & new_tmp_symbol | ( | const typet & | type, |
const source_locationt & | location, | ||
const irep_idt & | mode, | ||
symbol_table_baset & | symtab, | ||
std::string | suffix = "tmp_cc" , |
||
bool | is_auxiliary = true |
||
) |
Adds a fresh and uniquely named symbol to the symbol table.
type | The type of the new symbol. |
location | The source location for the new symbol. |
mode | The mode for the new symbol, e.g. ID_C, ID_java. |
symtab | The symbol table to which the new symbol is to be added. |
suffix | Suffix to use to generate the unique name |
is_auxiliary | Do not print symbol in traces if true (default = true) |
void simplify_gotos | ( | goto_programt & | goto_program, |
namespacet & | ns | ||
) |