|
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.
|
|
Adds a pragma on a source location disable all pointer checks.
The disabled checks are: "pointer-check", "pointer-primitive-check", "pointer-overflow-check", "signed-overflow-check",
Definition at line 79 of file utils.cpp.
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
.
- Parameters
-
expr | The expression that contains dereferences to be validated. |
ns | The namespace that defines all symbols appearing in expr . |
- Returns
- A conjunctive expression that checks validity of all pointers that are dereferenced within
expr
.
Definition at line 122 of file utils.cpp.