cprover
Loading...
Searching...
No Matches
dfcc_is_fresh.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
6Date: August 2022
7
8\*******************************************************************/
9
10#include "dfcc_is_fresh.h"
11
12#include <util/cprover_prefix.h>
13#include <util/pointer_expr.h>
14#include <util/symbol.h>
15
16#include "dfcc_cfg_info.h"
17#include "dfcc_library.h"
18
20 dfcc_libraryt &library,
21 message_handlert &message_handler)
22 : library(library), message_handler(message_handler), log(message_handler)
23{
24}
25
27 goto_programt &program,
28 dfcc_cfg_infot &cfg_info)
29{
31 program,
32 program.instructions.begin(),
33 program.instructions.end(),
34 cfg_info);
35}
36
38 goto_programt &program,
41 dfcc_cfg_infot &cfg_info)
42{
43 auto &target = first_instruction;
44 while(target != last_instruction)
45 {
46 if(target->is_function_call())
47 {
48 const auto &function = target->call_function();
49
50 if(function.id() == ID_symbol)
51 {
52 const irep_idt &fun_name = to_symbol_expr(function).get_identifier();
53
54 if(fun_name == CPROVER_PREFIX "is_fresh")
55 {
56 // add address on first operand
57 target->call_arguments()[0] =
58 address_of_exprt(target->call_arguments()[0]);
59
60 // fix the function name.
61 to_symbol_expr(target->call_function())
62 .set_identifier(library.dfcc_fun_symbol[dfcc_funt::IS_FRESH].name);
63
64 // pass the write_set
65 target->call_arguments().push_back(cfg_info.get_write_set(target));
66 }
67 }
68 }
69 target++;
70 }
71}
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
Computes natural loops, enforces normal form conditions, computes the nesting graph,...
const exprt & get_write_set(goto_programt::const_targett target) const
Returns the write set variable for that instruction.
dfcc_libraryt & library
void rewrite_calls(goto_programt &program, dfcc_cfg_infot &cfg_info)
Rewrites calls to is_fresh predicates into calls to the library implementation in the given program,...
dfcc_is_fresht(dfcc_libraryt &library, message_handlert &message_handler)
Class interface to library types and functions defined in cprover_contracts.c.
std::map< dfcc_funt, symbolt > dfcc_fun_symbol
Maps enum values to the actual function symbols (dynamically loaded)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
instructionst::iterator targett
#define CPROVER_PREFIX
Class that computes CFG information about the loop structure of a GOTO function for the purpose of dy...
Instruments occurrences of is_fresh predicates in programs encoding requires and ensures clauses of c...
Dynamic frame condition checking library loading.
API to expression classes for Pointers.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
Symbol table entry.