cprover
Loading...
Searching...
No Matches
dfcc_contract_clauses_codegen.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
6Date: 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/optional.h>
22#include <util/std_expr.h>
23
24#include "dfcc_contract_mode.h"
25
26#include <set>
27
28class goto_modelt;
30class dfcc_libraryt;
33
37{
38public:
46
58 const irep_idt &language_mode,
60 goto_programt &dest);
61
73 const irep_idt &language_mode,
75 goto_programt &dest);
76
77protected:
83
87 const irep_idt &language_mode,
89 goto_programt &dest);
90
94 const irep_idt &language_mode,
95 const exprt &target,
96 goto_programt &dest);
97
101 const irep_idt &language_mode,
103 goto_programt &dest);
104
108 const irep_idt &language_mode,
109 const exprt &target,
110 goto_programt &dest);
111
115 void inline_and_check_warnings(goto_programt &goto_program);
116};
117
118#endif
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
A class for an expression that represents a conditional target or a list of targets sharing a common ...
Definition c_expr.h:232
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.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
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.
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Enum type representing the contract checking and replacement modes.
Program Transformation.
API to expression classes.