cprover
Loading...
Searching...
No Matches
dfcc_wrapper_program.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dynamic frame condition checking for function contracts
4
5Author: Remi Delmas, delmasrd@amazon.com
6
7\*******************************************************************/
9
10#include <util/arith_tools.h>
11#include <util/c_types.h>
12#include <util/expr_util.h>
13#include <util/format_expr.h>
14#include <util/invariant.h>
16#include <util/namespace.h>
18#include <util/std_expr.h>
19
21
22#include <ansi-c/c_expr.h>
25
27#include "dfcc_instrument.h"
28#include "dfcc_library.h"
30#include "dfcc_utils.h"
31
34 symbol_table_baset &symbol_table,
35 dfcc_libraryt &library,
36 const symbolt &wrapper_symbol)
37{
39 symbol_table,
41 wrapper_symbol.name,
42 "__contract_write_set",
43 wrapper_symbol.location);
44}
45
48 symbol_table_baset &symbol_table,
49 dfcc_libraryt &library,
50 const symbolt &wrapper_symbol)
51{
53 symbol_table,
55 wrapper_symbol.name,
56 "__address_of_contract_write_set",
57 wrapper_symbol.location);
58}
59
60// Generate the write set to check for side effects in requires clauses
62 symbol_table_baset &symbol_table,
63 dfcc_libraryt &library,
64 const symbolt &wrapper_symbol)
65{
67 symbol_table,
69 wrapper_symbol.name,
70 "__requires_write_set",
71 wrapper_symbol.location);
72}
73
76 symbol_table_baset &symbol_table,
77 dfcc_libraryt &library,
78 const symbolt &wrapper_symbol)
79{
81 symbol_table,
83 wrapper_symbol.name,
84 "__address_of_requires_write_set",
85 wrapper_symbol.location);
86}
87
90 symbol_table_baset &symbol_table,
91 dfcc_libraryt &library,
92 const symbolt &wrapper_symbol)
93{
95 symbol_table,
97 wrapper_symbol.name,
98 "__ensures_write_set",
99 wrapper_symbol.location);
100}
101
104 symbol_table_baset &symbol_table,
105 dfcc_libraryt &library,
106 const symbolt &wrapper_symbol)
107{
109 symbol_table,
111 wrapper_symbol.name,
112 "__address_of_ensures_write_set",
113 wrapper_symbol.location);
114}
115
118 symbol_table_baset &symbol_table,
119 dfcc_libraryt &library,
120 const symbolt &wrapper_symbol)
121{
123 symbol_table,
125 wrapper_symbol.name,
126 "__is_fresh_set",
127 wrapper_symbol.location);
128}
129
132 symbol_table_baset &symbol_table,
133 dfcc_libraryt &library,
134 const symbolt &wrapper_symbol)
135{
137 symbol_table,
139 wrapper_symbol.name,
140 "__address_of_is_fresh_set",
141 wrapper_symbol.location);
142}
143
145 const dfcc_contract_modet contract_mode,
146 const symbolt &wrapper_symbol,
147 const symbolt &wrapped_symbol,
148 const dfcc_contract_functionst &contract_functions,
150 goto_modelt &goto_model,
151 message_handlert &message_handler,
152 dfcc_libraryt &library,
153 dfcc_instrumentt &instrument,
154 dfcc_lift_memory_predicatest &memory_predicates)
155 : contract_mode(contract_mode),
156 wrapper_symbol(wrapper_symbol),
157 wrapped_symbol(wrapped_symbol),
158 contract_functions(contract_functions),
159 contract_symbol(contract_functions.pure_contract_symbol),
160 contract_code_type(to_code_with_contract_type(contract_symbol.type)),
161 caller_write_set(caller_write_set_symbol.symbol_expr()),
162 wrapper_sl(wrapper_symbol.location),
163 return_value_opt(),
164 contract_write_set(create_contract_write_set(
165 goto_model.symbol_table,
166 library,
167 wrapper_symbol)),
168 addr_of_contract_write_set(create_addr_of_contract_write_set(
169 goto_model.symbol_table,
170 library,
171 wrapper_symbol)),
172 requires_write_set(create_requires_write_set(
173 goto_model.symbol_table,
174 library,
175 wrapper_symbol)),
176 addr_of_requires_write_set(create_addr_of_requires_write_set(
177 goto_model.symbol_table,
178 library,
179 wrapper_symbol)),
180 ensures_write_set(create_ensures_write_set(
181 goto_model.symbol_table,
182 library,
183 wrapper_symbol)),
184 addr_of_ensures_write_set(create_addr_of_ensures_write_set(
185 goto_model.symbol_table,
186 library,
187 wrapper_symbol)),
188 is_fresh_set(
189 create_is_fresh_set(goto_model.symbol_table, library, wrapper_symbol)),
190 addr_of_is_fresh_set(create_addr_of_is_fresh_set(
191 goto_model.symbol_table,
192 library,
193 wrapper_symbol)),
194 function_pointer_contracts(),
195 goto_model(goto_model),
196 message_handler(message_handler),
197 log(message_handler),
198 library(library),
199 instrument(instrument),
200 memory_predicates(memory_predicates),
201 ns(goto_model.symbol_table),
202 converter(goto_model.symbol_table, log.get_message_handler())
203{
204 // generate a return value symbol (needed to instantiate all contract lambdas)
205 if(contract_code_type.return_type().id() != ID_empty)
206 {
209 contract_code_type.return_type(),
210 wrapper_symbol.name,
211 "__contract_return_value",
212 wrapper_symbol.location);
213
214 // build contract_lambda_parameters
216 }
217
218 // build contract_lambda_parameters
219 for(const auto &param_id :
220 to_code_type(wrapper_symbol.type).parameter_identifiers())
221 {
222 contract_lambda_parameters.push_back(ns.lookup(param_id).symbol_expr());
223 }
224
225 // encode all contract clauses
233}
234
236 goto_programt &dest,
237 std::set<irep_idt> &dest_fp_contracts)
238{
239 add_to_dest(dest);
240 dest_fp_contracts.insert(
242}
243
258
260{
261 // call write_set_create(
262 // requires_write_set,
263 // assigns_size = 0,
264 // frees_size = 0,
265 // replacement_mode = false,
266 // assume_requires_ctx = contract_mode == check,
267 // assert_requires_ctx = contract_mode != check,
268 // assume_ensures_ctx = false,
269 // assert_ensures_ctx = false,
270 // )
272
278 wrapper_sl));
279
287 false_exprt(),
288 false_exprt(),
289 true_exprt(),
290 true_exprt(),
291 wrapper_sl);
292
294
295 // check for absence of allocation/deallocation in requires clauses
296 // ```c
297 // DECL __check_no_alloc: bool;
298 // CALL __check_no_alloc = check_empty_alloc_dealloc(requilres_write_set);
299 // ASSERT __check_no_alloc;
300 // DEAD __check_no_alloc: bool;
301 // ```
304 bool_typet(),
305 wrapper_symbol.name,
306 "__no_alloc_dealloc_in_requires",
307 wrapper_sl);
308
310
314 wrapper_sl));
315
317 check_sl.set_function(wrapper_symbol.name);
318 check_sl.set_property_class("no_alloc_dealloc_in_requires");
319 check_sl.set_comment(
320 "Check that requires do not allocate or deallocate memory");
323
324 // generate write set release and DEAD instructions
327 wrapper_sl));
329}
330
332{
333 // call write_set_create(
334 // ensures_write_set,
335 // assigns_size = 0,
336 // frees_size = 0,
337 // assume_requires_ctx = false,
338 // assert_requires_ctx = false,
339 // assume_ensures_ctx = contract_mode != check,
340 // assert_ensures_ctx = contract_mode == check,
341 // )
343
348 wrapper_sl));
349
351
356 false_exprt(),
357 false_exprt(),
360 true_exprt(),
361 true_exprt(),
362 wrapper_sl);
363
365
366 // call link_allocated(pre_post, caller) if in REPLACE MODE
368 {
372 wrapper_sl));
373 }
374
375 // check for absence of allocation/deallocation in contract clauses
376 // ```c
377 // DECL __check_no_alloc: bool;
378 // CALL __check_no_alloc = check_empty_alloc_dealloc(ensures_write_set);
379 // ASSERT __check_no_alloc;
380 // DEAD __check_no_alloc: bool;
381 // ```
384 bool_typet(),
385 wrapper_symbol.name,
386 "__no_alloc_dealloc_in_ensures_clauses",
387 wrapper_sl);
388
390
394 wrapper_sl));
395
397 check_sl.set_function(wrapper_symbol.name);
398 check_sl.set_property_class("no_alloc_dealloc_in_ensures");
399 check_sl.set_comment(
400 "Check that ensures do not allocate or deallocate memory");
401
404
405 // generate write set release
408 wrapper_sl));
409
410 // declare write set DEAD
412}
413
415{
417
423 wrapper_sl));
424
425 // We use the empty write set used to check ensures for side effects
426 // to check for side effects in the assigns and frees functions as well
427 // TODO: I don't know what the above comment means, why was there an empty
428 // write set here?
429
430 // call write_set_create
431 {
434 from_integer(contract_functions.get_nof_assigns_targets(), size_type()),
435 from_integer(contract_functions.get_nof_frees_targets(), size_type()),
436 false_exprt(),
437 false_exprt(),
438 false_exprt(),
439 false_exprt(),
440 true_exprt(),
441 true_exprt(),
442 wrapper_sl);
444 }
445
446 // build arguments for assigns and frees clauses functions
449 for(const auto &parameter : wrapper_code_type.parameter_identifiers())
450 {
452 wrapper_arguments.push_back(parameter_symbol.symbol_expr());
453 }
454
455 // call spec_assigns to build the contract write set
456 {
458 contract_functions.get_spec_assigns_function_symbol().symbol_expr());
459
460 auto &arguments = call.arguments();
461
462 // forward wrapper arguments
463 for(const auto &arg : wrapper_arguments)
464 arguments.push_back(arg);
465
466 // pass write set to populate
467 arguments.emplace_back(addr_of_contract_write_set);
468
469 // pass the empty write set to check side effects against
470 arguments.emplace_back(addr_of_requires_write_set);
471
473 }
474
475 // call spec_frees to build the contract write set
476 {
478 contract_functions.get_spec_frees_function_symbol().symbol_expr());
479 auto &arguments = call.arguments();
480
481 // forward wrapper arguments
482 for(const auto &arg : wrapper_arguments)
483 arguments.push_back(arg);
484
485 // pass write set to populate
486 arguments.emplace_back(addr_of_contract_write_set);
487
488 // pass the empty write set to check side effects against
489 arguments.emplace_back(addr_of_requires_write_set);
490
492 }
493
494 // generate write set release and DEAD instructions
497 wrapper_sl));
500}
501
536
538{
539 // we use this empty requires write set to check for the absence of side
540 // effects in the requires clauses
541 const auto &wrapper_id = wrapper_symbol.name;
542 const auto &language_mode =
544
545 // if in replacement mode, check that assertions hold in the current context,
546 // otherwise assume
547 const auto &statement_type =
549
550 // goto program where all requires are added
552
553 // translate each requires clause
554 for(const auto &r : contract_code_type.c_requires())
555 {
558 requires_lmbd.add_source_location() = r.source_location();
559 if(
563 goto_model.symbol_table, requires_lmbd, language_mode);
564
565 source_locationt sl(r.source_location());
567 {
568 sl.set_property_class(ID_precondition);
569 sl.set_comment(
570 "Check requires clause of contract " + id2string(contract_symbol.name) +
571 " for function " + id2string(wrapper_id));
572 }
575 }
576
577 // fix calls to user-defined memory predicates
579
580 // instrument for side effects
586
587 // append resulting program to preconditions section
589}
590
592{
593 const auto &language_mode = wrapper_symbol.mode;
594 const auto &wrapper_id = wrapper_symbol.name;
595 const auto &statement_type =
597
598 // goto program where all requires are added
600
601 // translate each ensures clause
602 for(const auto &e : contract_code_type.c_ensures())
603 {
605 .application(contract_lambda_parameters)
606 .with_source_location<exprt>(e);
607
610
611 // this also rewrites ID_old expressions to fresh variables
613 goto_model.symbol_table, ensures, language_mode, history);
614
615 source_locationt sl(e.source_location());
617 {
618 sl.set_property_class(ID_postcondition);
619 sl.set_comment(
620 "Check ensures clause of contract " + id2string(contract_symbol.name) +
621 " for function " + id2string(wrapper_id));
622 }
623
626 }
627
628 // When checking an ensures clause we link the contract write set to the
629 // ensures write set to know what was deallocated by the function so that
630 // the was_freed predicate can perform its checks
634 wrapper_sl));
635
636 // fix calls to user-defined user-defined memory predicates
638
639 // instrument for side effects
645
646 // add the ensures program to the postconditions section
648}
649
657
659{
660 // build call to the wrapped function
662
664 {
665 symbol_exprt return_value = return_value_opt.value();
666 // DECL
668 call.lhs() = return_value;
669
670 // SET_RETURN_VALUE
673
674 // DEAD
676 }
677
678 // forward wrapper arguments
680
681 for(const auto &parameter : wrapper_code_type.parameter_identifiers())
682 {
683 PRECONDITION(!parameter.empty());
685 call.arguments().push_back(parameter_symbol.symbol_expr());
686 }
687
688 // pass write set to check against
689 call.arguments().push_back(addr_of_contract_write_set);
690
692}
693
695{
696 // generate local write set and add as parameter to the call
698 for(const auto &parameter :
699 to_code_type(wrapper_symbol.type).parameter_identifiers())
700 {
701 PRECONDITION(!parameter.empty());
703 write_set_arguments.push_back(parameter_symbol.symbol_expr());
704 }
705
706 // check assigns clause inclusion
707 // IF __caller_write_set==NULL GOTO skip_target;
708 // DECL check: bool;
709 // CALL check = __CPROVER_contracts_write_set_check_assigns_clause_inclusion(
710 // __caller_write_set, &__local_write_set);
711 // ASSERT check;
712 // CALL check = __CPROVER_contracts_write_set_check_frees_clause_inclusion(
713 // __caller_write_set, &__local_write_set);
714 // ASSERT check;
715 // DEAD check;
716 // skip_target: skip;
717
718 auto goto_instruction =
721
722 {
723 // assigns clause inclusion
726 bool_typet(),
727 wrapper_symbol.name,
728 "__check_assigns_clause_incl",
729 wrapper_sl);
730
732
736 wrapper_sl));
737
739 check_sl.set_function(wrapper_symbol.name);
740 check_sl.set_property_class("assigns");
741 check_sl.set_comment(
742 "Check that the assigns clause of " + id2string(contract_symbol.name) +
743 " is included in the caller's assigns clause");
746 }
747
748 {
749 // frees clause inclusion
752 bool_typet(),
753 wrapper_symbol.name,
754 "__check_frees_clause_incl",
755 wrapper_sl);
756
758
762 wrapper_sl));
763
765 check_sl.set_function(wrapper_symbol.name);
766 check_sl.set_property_class("frees");
767 check_sl.set_comment(
768 "Check that the frees clause of " + id2string(contract_symbol.name) +
769 " is included in the caller's frees clause");
772 }
773
774 auto label_instruction =
776 goto_instruction->complete_goto(label_instruction);
777
779 contract_functions.get_spec_assigns_havoc_function_symbol().symbol_expr(),
780 {addr_of_contract_write_set});
781
783
784 // assign nondet to the return value
785 if(return_value_opt.has_value())
786 {
787 symbol_exprt return_value = return_value_opt.value();
788
789 // DECL
791
792 // ASSIGN NONDET
794 return_value,
796 wrapper_sl));
797
798 // SET RETURN VALUE
801
802 // DEAD
804 }
805
806 // nondet free the freeable set, record effects in both the contract write
807 // set and the caller write set
811 wrapper_sl));
812}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
API to expression classes that are internal to the C frontend.
unsignedbv_typet size_type()
Definition c_types.cpp:55
const code_with_contract_typet & to_code_with_contract_type(const typet &type)
Cast a typet to a code_with_contract_typet.
Definition c_types.h:467
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
The Boolean type.
Definition std_types.h:36
goto_instruction_codet representation of a function call statement.
Data structure for representing an arbitrary statement in a program.
Generates GOTO functions modelling a contract assigns and frees clauses.
This class instruments GOTO functions or instruction sequences for frame condition checking and loop ...
void instrument_goto_program(const irep_idt &function_id, goto_programt &goto_program, const exprt &write_set, std::set< irep_idt > &function_pointer_contracts)
Instruments a GOTO program against a given write set variable.
Class interface to library types and functions defined in cprover_contracts.c.
const code_function_callt write_set_check_allocated_deallocated_is_empty_call(const exprt &check_var, const exprt &write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_allocated_deallocated_is_empty.
const code_function_callt obj_set_create_indexed_by_object_id_call(const exprt &obj_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_obj_set_create_indexed_by_object_id.
const code_function_callt link_allocated_call(const exprt &write_set_postconditions_ptr, const exprt &write_set_to_link_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_link_allocated.
const code_function_callt write_set_release_call(const exprt &write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_release.
const code_function_callt obj_set_release_call(const exprt &obj_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_obj_set_release.
const code_function_callt link_deallocated_call(const exprt &write_set_postconditions_ptr, const exprt &write_set_to_link_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_link_deallocated.
const code_function_callt write_set_check_assigns_clause_inclusion_call(const exprt &check_var, const exprt &reference_write_set_ptr, const exprt &candidate_write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_assigns_clause_inclusion.
const code_function_callt link_is_fresh_call(const exprt &write_set_ptr, const exprt &is_fresh_obj_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_link_is_fresh.
std::map< dfcc_typet, typet > dfcc_type
Maps enum values to the actual types (dynamically loaded)
const code_function_callt write_set_create_call(const exprt &write_set_ptr, const exprt &contract_assigns_size, const exprt &contract_frees_size, const exprt &assume_requires_ctx, const exprt &assert_requires_ctx, const exprt &assume_ensures_ctx, const exprt &assert_ensures_ctx, const exprt &allow_allocate, const exprt &allow_deallocate, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_create.
const code_function_callt write_set_check_frees_clause_inclusion_call(const exprt &check_var, const exprt &reference_write_set_ptr, const exprt &candidate_write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_frees_clause_inclusion.
const code_function_callt write_set_deallocate_freeable_call(const exprt &write_set_ptr, const exprt &target_write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_deallocate_freeable.
void fix_calls(goto_programt &program)
Fixes calls to user-defined memory predicates in the given program, by adding an address-of to argume...
const source_locationt wrapper_sl
Source location with wrapper function name as function name.
void encode_ensures_clauses()
Encodes postconditions, instruments them to check for side effects.
const symbol_exprt contract_write_set
Symbol for the write set object derived from the contract.
void encode_havoced_function_call()
Creates instructions that havoc the contract write set, create a nondet return value,...
const symbol_exprt caller_write_set
void encode_requires_write_set()
Encodes the empty write set used to check for side effects in requires.
void encode_requires_clauses()
Encodes preconditions, instruments them to check for side effects.
void encode_is_fresh_set()
Encodes the object set used to evaluate is fresh predicates,.
const symbol_exprt addr_of_requires_write_set
Symbol for the pointer to the write set used to check requires clauses.
void encode_contract_write_set()
Encodes the write set of the contract being checked/replaced (populated by calling functions provided...
const dfcc_contract_functionst & contract_functions
const code_with_contract_typet & contract_code_type
const symbol_exprt requires_write_set
Symbol for the write set used to check requires clauses for side effects.
exprt::operandst contract_lambda_parameters
Vector of arguments to use to instantiate the lambdas wrapping the contract clauses.
const symbol_exprt addr_of_ensures_write_set
Symbol for the pointer to the write set used to check ensures clauses.
const dfcc_contract_modet contract_mode
void encode_checked_function_call()
Creates a checked function call to the wrapped function, passing it the contract-derived write set as...
std::set< irep_idt > function_pointer_contracts
Set of required or ensured contracts for function pointers discovered when processing the contract of...
const symbol_exprt addr_of_is_fresh_set
Symbol for the pointer to the is_fresh object set.
dfcc_lift_memory_predicatest & memory_predicates
void add_to_dest(goto_programt &dest, std::set< irep_idt > &dest_fp_contracts)
Adds the whole program to dest and the discovered function pointer contracts dest_fp_contracts.
void encode_function_call()
Encodes the function call section of the wrapper program.
dfcc_wrapper_programt(const dfcc_contract_modet contract_mode, const symbolt &wrapper_symbol, const symbolt &wrapped_symbol, const dfcc_contract_functionst &contract_functions, const symbolt &caller_write_set_symbol, goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library, dfcc_instrumentt &instrument, dfcc_lift_memory_predicatest &memory_predicates)
const symbol_exprt addr_of_contract_write_set
Symbol for the pointer to the write set object derived from the contract.
const symbol_exprt ensures_write_set
Symbol for the write set used to check ensures clauses for side effects.
dfcc_instrumentt & instrument
void encode_ensures_write_set()
Encodes the empty write set used to check for side effects in ensures.
optionalt< symbol_exprt > return_value_opt
Symbol for the return value of the wrapped function.
goto_programt link_deallocated_contract
const symbol_exprt is_fresh_set
Symbol for the object set used to evaluate is_fresh predicates.
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
typet & type()
Return the type of the expression.
Definition expr.h:84
The Boolean constant false.
Definition std_expr.h:3017
void goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode)
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_set_return_value(exprt return_value, const source_locationt &l=source_locationt::nil())
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
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_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
Expression to hold a symbol (variable)
Definition std_expr.h:113
The symbol table base class interface.
Symbol table entry.
Definition symbol.h:28
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
irep_idt name
The unique identifier.
Definition symbol.h:40
The Boolean constant true.
Definition std_expr.h:3008
Translates assigns and frees clauses of a function contract into goto functions that allow to build a...
dfcc_contract_modet
Enum type representing the contract checking and replacement modes.
Add instrumentation to a goto program to perform frame condition checks.
Dynamic frame condition checking library loading.
@ WRITE_SET
type of descriptors of assignable/freeable sets of locations
@ OBJ_SET_PTR
type of pointers to sets of object identifiers
@ OBJ_SET
type of sets of object identifiers
@ WRITE_SET_PTR
type of pointers to descriptors of assignable/freeable sets of locations
Collects all user-defined predicates that call functions is_fresh, pointer_in_range,...
Dynamic frame condition checking utility functions.
static symbol_exprt create_requires_write_set(symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol)
static symbol_exprt create_addr_of_contract_write_set(symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol)
Generate the contract write set pointer.
static symbol_exprt create_addr_of_ensures_write_set(symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol)
Generate the write set pointer to check side effects in ensures clauses.
static symbol_exprt create_addr_of_is_fresh_set(symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol)
Generate object set pointer used to support is_fresh predicates.
static symbol_exprt create_addr_of_requires_write_set(symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol)
Generate the write set pointer to check side effects in requires clauses.
static symbol_exprt create_ensures_write_set(symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol)
Generate the write set to check side effects in ensures clauses.
static symbol_exprt create_contract_write_set(symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol)
Generate the contract write set.
static symbol_exprt create_is_fresh_set(symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol)
Generate object set used to support is_fresh predicates.
Generates the body of a wrapper function from a contract for contract checking or contract replacemen...
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Deprecated expression utility functions.
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
static int8_t r
Definition irep_hash.h:60
API to expression classes for 'mathematical' expressions.
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
Pointer Logic.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
API to expression classes.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
static symbolt & get_function_symbol(symbol_table_baset &, const irep_idt &function_id)
Returns the symbolt for function_id.
static const exprt make_null_check_expr(const exprt &ptr)
Returns the expression expr == NULL.
static symbol_exprt create_symbol(symbol_table_baset &, const typet &type, const irep_idt &function_id, const std::string &base_name, const source_locationt &source_location)
Adds a new symbol named function_id::base_name of type type with given attributes in the symbol table...
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.
Definition utils.cpp:549
void add_quantified_variable(symbol_table_baset &symbol_table, exprt &expression, const irep_idt &mode)
This function recursively searches expression to find nested or non-nested quantified expressions.
Definition utils.cpp:367