cprover
Loading...
Searching...
No Matches
dfcc_spec_functions.h
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\*******************************************************************/
8
14
15#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_SPEC_FUNCTIONS_H
16#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_SPEC_FUNCTIONS_H
17
18#include <util/arith_tools.h>
19#include <util/c_types.h>
20#include <util/message.h>
21#include <util/std_expr.h>
22#include <util/std_types.h>
23
24#include "dfcc_library.h"
25#include "dfcc_utils.h"
26
27#include <map>
28#include <set>
29
30class goto_modelt;
32class symbolt;
34
44{
45public:
50
70 const irep_idt &function_id,
71 const irep_idt &havoc_function_id,
72 std::size_t &nof_targets);
73
96 const irep_idt &function_id,
97 const goto_programt &original_program,
98 const exprt &write_set_to_havoc,
99 goto_programt &havoc_program,
100 std::size_t &nof_targets);
101
124 const irep_idt &function_id,
125 std::size_t &nof_targets);
126
147 const exprt &write_set_to_fill,
148 const irep_idt &language_mode,
149 goto_programt &program,
150 std::size_t &nof_targets);
151
175 void
176 to_spec_frees_function(const irep_idt &function_id, std::size_t &nof_targets);
177
196 const exprt &write_set_to_fill,
197 const irep_idt &language_mode,
198 goto_programt &program,
199 std::size_t &nof_targets);
200
201protected:
207
211 const typet &get_target_type(const exprt &expr);
212};
213
214#endif
A class for an expression that represents a conditional target or a list of targets sharing a common ...
Definition c_expr.h:233
Class interface to library types and functions defined in cprover_contracts.c.
void to_spec_assigns_function(const irep_idt &function_id, std::size_t &nof_targets)
Transforms (in place) a function.
void to_spec_frees_instructions(const exprt &write_set_to_fill, const irep_idt &language_mode, goto_programt &program, std::size_t &nof_targets)
Rewrites in place program expressed in terms of built-ins specifying freeable targets declaratively u...
void generate_havoc_function(const irep_idt &function_id, const irep_idt &havoc_function_id, std::size_t &nof_targets)
From a function:
void generate_havoc_instructions(const irep_idt &function_id, const goto_programt &original_program, const exprt &write_set_to_havoc, goto_programt &havoc_program, std::size_t &nof_targets)
Translates original_program that specifies assignable targets into a program that havocs the targets.
message_handlert & message_handler
void to_spec_assigns_instructions(const exprt &write_set_to_fill, const irep_idt &language_mode, goto_programt &program, std::size_t &nof_targets)
Rewrites in place program expressed in terms of built-ins specifying assignable targets declaratively...
const typet & get_target_type(const exprt &expr)
Extracts the type of an assigns clause target expression The expression must be of the form: expr = c...
dfcc_spec_functionst(goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library)
void to_spec_frees_function(const irep_idt &function_id, std::size_t &nof_targets)
Transforms (in place) a function.
Base class for all expressions.
Definition expr.h:56
A generic container class for the GOTO intermediate representation of one function.
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:94
Symbol table entry.
Definition symbol.h:28
The type of an expression, extends irept.
Definition type.h:29
Dynamic frame condition checking library loading.
Dynamic frame condition checking utility functions.
API to expression classes.
Pre-defined types.
dstringt irep_idt