CBMC
dfcc_spec_functions.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Dynamic frame condition checking for function contracts
4 
5 Author: 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 
30 class goto_modelt;
31 class message_handlert;
32 class symbolt;
34 
44 {
45 public:
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 
201 protected:
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.
Definition: dfcc_library.h:154
This class rewrites GOTO functions that use the built-ins:
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.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
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.