cprover
Loading...
Searching...
No Matches
dfcc_pointer_equals.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: Jan 2025
7
8\*******************************************************************/
9
13
14#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_POINTER_EQUALS_H
15#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_POINTER_EQUALS_H
16
17#include <util/message.h>
18
20
21class goto_modelt;
23class dfcc_libraryt;
24class dfcc_cfg_infot;
25class exprt;
26
32
36{
37public:
43
47 void rewrite_calls(goto_programt &program, dfcc_cfg_infot cfg_info);
48
53 void rewrite_calls(
54 goto_programt &program,
55 goto_programt::targett first_instruction,
56 const goto_programt::targett &last_instruction,
57 dfcc_cfg_infot cfg_info);
58
59protected:
63};
64
65#endif
Computes natural loops, enforces normal form conditions, computes the nesting graph,...
Class interface to library types and functions defined in cprover_contracts.c.
dfcc_pointer_equalst(dfcc_libraryt &library, message_handlert &message_handler)
void rewrite_calls(goto_programt &program, dfcc_cfg_infot cfg_info)
Rewrites calls to pointer_equals predicates into calls to the library implementation in the given pro...
message_handlert & message_handler
Base class for all expressions.
Definition expr.h:56
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
void rewrite_equal_exprt_to_pointer_equals(exprt &expr)
Rewrites equal_exprt over pointers into calls to the front-end function __CPROVER_pointer_equals,...
Concrete Goto Program.