cprover
|
#include "utils.h"
#include <goto-programs/cfg.h>
#include <util/fresh_symbol.h>
#include <util/graph.h>
#include <util/message.h>
#include <util/pointer_expr.h>
#include <util/pointer_predicates.h>
#include <util/simplify_expr.h>
#include <langapi/language_util.h>
Go to the source code of this file.
Functions | |
static void | append_safe_havoc_code_for_expr (const source_locationt location, const namespacet &ns, const exprt &expr, goto_programt &dest, const std::function< void()> &havoc_code_impl) |
void | add_pragma_disable_pointer_checks (source_locationt &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 &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, bool is_auxiliary) |
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. | |
Variables | |
static const char | ASSIGNS_CLAUSE_REPLACEMENT_TRACKING [] |
Prefix for comments added to track assigns clause replacement. | |
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 & | 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
.
|
static |
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 | ||
) |