|
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...
|
|
void | insert_before_and_update_jumps (goto_programt &destination, goto_programt::targett &target, const goto_programt::instructiont &i) |
| Insert a goto instruction before a target instruction iterator and update targets of all jumps that points to the iterator to jumping to the inserted instruction. More...
|
|
void | simplify_gotos (goto_programt &goto_program, const 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, const 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...
|
|
void | infer_loop_assigns (const local_may_aliast &local_may_alias, const loopt &loop, assignst &assigns) |
| Infer loop assigns using alias analysis result local_may_alias . More...
|
|
void | widen_assigns (assignst &assigns, const namespacet &ns) |
| Widen expressions in assigns with the following strategy. More...
|
|
replace_history_parametert | replace_history_old (symbol_table_baset &symbol_table, const exprt &expr, const source_locationt &location, const irep_idt &mode) |
| This function recursively identifies the "old" expressions within expr and replaces them with corresponding history variables. More...
|
|
replace_history_parametert | replace_history_loop_entry (symbol_table_baset &symbol_table, const exprt &expr, const source_locationt &location, const irep_idt &mode) |
| This function recursively identifies the "loop_entry" expressions within expr and replaces them with corresponding history variables. More...
|
|
void | generate_history_variables_initialization (symbol_table_baset &symbol_table, exprt &clause, const irep_idt &mode, goto_programt &program) |
| This function generates all the instructions required to initialize history variables. More...
|
|
bool | is_transformed_loop_head (const goto_programt::const_targett &target) |
| Return true if target is the head of some transformed loop. More...
|
|
bool | is_transformed_loop_end (const goto_programt::const_targett &target) |
| Return true if target is the end of some transformed loop. More...
|
|
bool | is_assignment_to_instrumented_variable (const goto_programt::const_targett &target, std::string var_name) |
| Return true if target is an assignment to an instrumented variable with name var_name . More...
|
|
unsigned | get_suffix_unsigned (const std::string &str, const std::string &prefix) |
| Convert the suffix digits right after prefix of str into unsigned. More...
|
|
goto_programt::targett | get_loop_end_from_loop_head_and_content_mutable (const goto_programt::targett &loop_head, const loop_templatet< goto_programt::targett, goto_programt::target_less_than > &loop) |
| Find the goto instruction of loop that jumps to loop_head More...
|
|
goto_programt::const_targett | get_loop_end_from_loop_head_and_content (const goto_programt::const_targett &loop_head, const loop_templatet< goto_programt::const_targett, goto_programt::target_less_than > &loop) |
|
goto_programt::targett | get_loop_head_or_end (const unsigned int loop_number, goto_functiont &function, bool finding_head) |
| Return loop head if finding_head is true, Otherwise return loop end. More...
|
|
goto_programt::targett | get_loop_end (const unsigned int loop_number, goto_functiont &function) |
| Find and return the last instruction of the natural loop with loop_number in function . More...
|
|
goto_programt::targett | get_loop_head (const unsigned int loop_number, goto_functiont &function) |
| Find and return the first instruction of the natural loop with loop_number in function . More...
|
|
exprt | get_loop_invariants (const goto_programt::const_targett &loop_end, const bool check_side_effect=true) |
| Extract loop invariants from annotated loop end. More...
|
|
exprt | get_loop_assigns (const goto_programt::const_targett &loop_end) |
| Extract loop assigns from annotated loop end. More...
|
|
exprt | get_loop_decreases (const goto_programt::const_targett &loop_end, const bool check_side_effect=true) |
| Extract loop decreases from annotated loop end. More...
|
|
void | annotate_invariants (const invariant_mapt &invariant_map, goto_modelt &goto_model) |
| Annotate the invariants in invariant_map to their corresponding loops. More...
|
|
void | annotate_assigns (const std::map< loop_idt, std::set< exprt >> &assigns_map, goto_modelt &goto_model) |
| Annotate the assigns in assigns_map to their corresponding loops. More...
|
|
void | annotate_assigns (const std::map< loop_idt, exprt > &assigns_map, goto_modelt &goto_model) |
|
void | annotate_decreases (const std::map< loop_idt, std::vector< exprt >> &decreases_map, goto_modelt &goto_model) |
| Annotate the decreases in decreases_map to their corresponding loops. More...
|
|
Insert a goto instruction before a target instruction iterator and update targets of all jumps that points to the iterator to jumping to the inserted instruction.
This method is intended to keep external instruction::targett stable, i.e. they will still point to the same instruction after inserting the new one
This function inserts a instruction i
into a destination program destination
immediately before a specified instruction iterator target
. After insertion, update all jumps that pointing to target
to jumping to i
instead.
Different from insert_before_swap_and_advance
, this function doesn't invalidate the iterator target
after insertion. That is, target
and all other instruction iterators same as target
will still point to the same instruction after insertion.
- Parameters
-
destination | The destination program for inserting the i . |
target | The instruction iterator at which to insert the i . |
i | The goto instruction to be inserted into the destination . |
Definition at line 247 of file utils.cpp.