CBMC
dfcc_contract_clauses_codegen.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 Date: February 2023
7 
8 \*******************************************************************/
9 
13 
14 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_CLAUSES_CODEGEN_H
15 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_CLAUSES_CODEGEN_H
16 
18 
19 #include <util/message.h>
20 #include <util/namespace.h>
21 #include <util/std_expr.h>
22 
23 #include "dfcc_contract_mode.h"
24 
25 #include <set>
26 
27 class goto_modelt;
28 class message_handlert;
29 class dfcc_libraryt;
32 
36 {
37 public:
45 
57  const irep_idt &language_mode,
58  const exprt::operandst &assigns_clause,
59  goto_programt &dest);
60 
72  const irep_idt &language_mode,
73  const exprt::operandst &frees_clause,
74  goto_programt &dest);
75 
76 protected:
82 
86  const irep_idt &language_mode,
87  const conditional_target_group_exprt &group,
88  goto_programt &dest);
89 
93  const irep_idt &language_mode,
94  const exprt &target,
95  goto_programt &dest);
96 
100  const irep_idt &language_mode,
101  const conditional_target_group_exprt &group,
102  goto_programt &dest);
103 
107  const irep_idt &language_mode,
108  const exprt &target,
109  goto_programt &dest);
110 
114  void inline_and_check_warnings(goto_programt &goto_program);
115 };
116 
117 #endif
A class for an expression that represents a conditional target or a list of targets sharing a common ...
Definition: c_expr.h:233
Translates assigns and frees clauses of a function contract or loop contract into GOTO programs that ...
void encode_freeable_target_group(const irep_idt &language_mode, const conditional_target_group_exprt &group, goto_programt &dest)
Generates GOTO instructions to build the representation of the given conditional target group.
void encode_assignable_target(const irep_idt &language_mode, const exprt &target, goto_programt &dest)
Generates GOTO instructions to build the representation of the given assignable target.
void encode_assignable_target_group(const irep_idt &language_mode, const conditional_target_group_exprt &group, goto_programt &dest)
Generates GOTO instructions to build the representation of the given conditional target group.
void gen_spec_assigns_instructions(const irep_idt &language_mode, const exprt::operandst &assigns_clause, goto_programt &dest)
Generates instructions encoding the assigns_clause targets and adds them to dest.
void encode_freeable_target(const irep_idt &language_mode, const exprt &target, goto_programt &dest)
Generates GOTO instructions to build the representation of the given freeable target.
void gen_spec_frees_instructions(const irep_idt &language_mode, const exprt::operandst &frees_clause, goto_programt &dest)
Generates instructions encoding the frees_clause targets and adds them to dest.
void inline_and_check_warnings(goto_programt &goto_program)
Inlines all calls in the given program and checks that the only missing functions or functions withou...
dfcc_contract_clauses_codegent(goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library)
Class interface to library types and functions defined in cprover_contracts.c.
Definition: dfcc_library.h:154
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
std::vector< exprt > operandst
Definition: expr.h:58
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
Enum type representing the contract checking and replacement modes.
Program Transformation.
API to expression classes.