CBMC
dfcc_obeys_contract.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: August 2022
7 
8 \*******************************************************************/
9 
13 
14 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_OBEYS_CONTRACT_H
15 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_OBEYS_CONTRACT_H
16 
17 #include <util/message.h>
18 
20 
21 class goto_modelt;
22 class message_handlert;
23 class dfcc_libraryt;
24 class dfcc_cfg_infot;
25 class exprt;
26 
30 {
31 public:
37 
41  void rewrite_calls(
42  goto_programt &program,
43  dfcc_cfg_infot &cfg_info,
44  std::set<irep_idt> &function_pointer_contracts);
45 
50  void rewrite_calls(
51  goto_programt &program,
52  goto_programt::targett first_instruction,
53  const goto_programt::targett &last_instruction,
54  dfcc_cfg_infot &cfg_info,
55  std::set<irep_idt> &function_pointer_contracts);
56 
57 protected:
61 
65  void get_contract_name(
66  const exprt &expr,
67  std::set<irep_idt> &function_pointer_contracts);
68 };
69 
70 #endif
Computes natural loops, enforces normal form conditions, computes the nesting graph,...
Class interface to library types and functions defined in cprover_contracts.c.
Definition: dfcc_library.h:154
Rewrites calls to obeys_contract predicates into calls to the library implementation.
dfcc_obeys_contractt(dfcc_libraryt &library, message_handlert &message_handler)
message_handlert & message_handler
void rewrite_calls(goto_programt &program, dfcc_cfg_infot &cfg_info, std::set< irep_idt > &function_pointer_contracts)
Rewrites calls to obeys_contract predicates into calls to the library implementation in the given pro...
void get_contract_name(const exprt &expr, std::set< irep_idt > &function_pointer_contracts)
Extracts the name from the second argument of a call to obeys_contract (modulo any intermediate typec...
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
instructionst::iterator targett
Definition: goto_program.h:614
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:154
Concrete Goto Program.