cprover
Loading...
Searching...
No Matches
havoc_assigns_clause_targets.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Havoc multiple and possibly dependent targets simultaneously
4
5Author: Remi Delmas, delmasrd@amazon.com
6
7\*******************************************************************/
8
11
13
14#include <map>
15
16#include <util/c_types.h>
17#include <util/format_expr.h>
18#include <util/format_type.h>
19#include <util/message.h>
20#include <util/pointer_expr.h>
23#include <util/std_code.h>
24
25#include <ansi-c/c_expr.h>
27
29#include "utils.h"
30
32{
33 // snapshotting instructions and well-definedness checks
35
36 // add spec targets
37 for(const auto &target : targets)
39
40 // add static locals called touched by the replaced function
42
43 // generate havocking instructions for all tracked CARs
45 for(const auto &pair : from_spec_assigns)
47
48 for(const auto &pair : from_stack_alloc)
50
51 for(const auto &pair : from_heap_alloc)
53
54 // append to dest
55 dest.destructive_append(snapshot_program);
56 dest.destructive_append(havoc_program);
57}
58
62{
65 car.target(), function_id, ns);
66
69
71 const auto skip_target =
73
76
77 if(car.target().id() == ID_pointer_object)
78 {
79 // OTHER __CPROVER_havoc_object(target_snapshot_var)
80 codet code(ID_havoc_object, {car.lower_bound_var()});
81 const auto &inst =
83 inst->source_location_nonconst().set_comment(tracking_comment);
84 }
85 else
86 {
87 // ASSIGN *(target.type() *)__car_lb = nondet(car.target().type())
88 const auto &target_type = car.target().type();
92 car.lower_bound_var(), pointer_type(target_type))},
93 nondet,
95 inst->source_location_nonconst().set_comment(tracking_comment);
96 }
97
98 dest.destructive_append(skip_program);
99
100 dest.add(
102
103 dest.add(
105
106 dest.add(
108}
API to expression classes that are internal to the C frontend.
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:253
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Class that represents a normalized conditional address range, with:
Data structure for representing an arbitrary statement in a program.
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
void havoc_if_valid(car_exprt car, goto_programt &dest)
Generates instructions to conditionally havoc the given conditional address range expression car,...
void get_instructions(goto_programt &dest)
Generates the assigns clause replacement instructions in dest.
void track_spec_target(const exprt &expr, goto_programt &dest)
Track an assigns clause target and generate snaphsot instructions and well-definedness assertions in ...
symbol_exprt_to_car_mapt from_stack_alloc
Map to from DECL symbols to corresponding conditional address ranges.
cond_target_exprt_to_car_mapt from_spec_assigns
Map to from conditional target expressions of assigns clauses to corresponding conditional address ra...
exprt_to_car_mapt from_heap_alloc
Map to from malloc'd symbols to corresponding conditional address ranges.
void track_static_locals(goto_programt &dest)
Search the call graph reachable from the instrumented function to identify local static variables use...
const namespacet ns
Program namespace.
const irep_idt & function_id
Name of the instrumented function.
Boolean negation.
Definition std_expr.h:2181
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:1928
Havoc function assigns clauses.
Specify write set in function contracts.
API to expression classes for Pointers.
Pointer Logic.
Various predicates over pointers in programs.
void add_pragma_disable_pointer_checks(source_locationt &location)
Adds a pragma on a source location disable all pointer checks.
Definition utils.cpp:79
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.
Definition utils.cpp:269