#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/byte_operators.h>#include <util/message.h>
Include dependency graph for utils.h: This graph shows which files directly or indirectly include this file: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 | cleanert |
| Allows to clean expressions of side effects. More... | |
Functions | |
| exprt | all_dereferences_are_valid (const exprt &expr, const namespacet &ns) |
| Generate a validity check over all dereferences in an expression. More... | |
| 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. More... | |
| 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. More... | |
| 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. More... | |
| 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. More... | |
| bool | is_loop_free (const goto_programt &goto_program, namespacet &ns, messaget &log) |
| Returns true iff the given program is loop-free, i.e. More... | |
| 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. More... | |
| 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. More... | |
Function Documentation
◆ all_dereferences_are_valid()
| 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.
- 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.
◆ generate_lexicographic_less_than_check()
| 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.
- Parameters
-
lhs A vector of variables representing the LHS of the comparison. rhs A vector of variables representing the RHS of the comparison.
- Returns
- A lexicographic less-than comparison expression: LHS < RHS.
◆ insert_before_swap_and_advance()
| 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.
- Parameters
-
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.
◆ is_assigns_clause_replacement_tracking_comment()
| 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.
◆ is_loop_free()
| bool is_loop_free | ( | const goto_programt & | goto_program, |
| namespacet & | ns, | ||
| messaget & | log | ||
| ) |
◆ make_assigns_clause_replacement_tracking_comment()
| irep_idt make_assigns_clause_replacement_tracking_comment | ( | const exprt & | target, |
| const irep_idt & | function_id, | ||
| const namespacet & | ns | ||
| ) |
◆ new_tmp_symbol()
| 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.
- Parameters
-
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)
- Returns
- The new symbolt object.
◆ simplify_gotos()
| void simplify_gotos | ( | goto_programt & | goto_program, |
| namespacet & | ns | ||
| ) |
