cprover
assigns.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Specify write set in function contracts.
4 
5 Author: Felipe R. Monteiro
6 
7 Date: July 2021
8 
9 \*******************************************************************/
10 
13 
14 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_ASSIGNS_H
15 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_ASSIGNS_H
16 
17 #include "contracts.h"
18 
20 
23 {
24 public:
26  const exprt &object,
28  messaget &log_parameter,
29  const irep_idt &function_id);
31 
32  std::vector<symbol_exprt> temporary_declarations() const;
33  exprt alias_expression(const exprt &lhs);
35  const exprt &get_direct_pointer() const;
37 
38  static exprt pointer_for(const exprt &object)
39  {
40  return address_of_exprt(object);
41  }
42 
43 protected:
50 };
51 
53 {
54 public:
56  const exprt &assigns,
57  code_contractst &contract,
58  const irep_idt function_id,
59  messaget log_parameter);
61 
66  exprt alias_expression(const exprt &lhs);
67  exprt compatible_expression(const assigns_clauset &called_assigns);
68 
69 protected:
70  const exprt &assigns;
71 
72  std::vector<assigns_clause_targett *> targets;
74 
78 };
79 
80 #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_ASSIGNS_H
Operator to return the address of an object.
Definition: pointer_expr.h:341
A base class for assigns clause targets.
Definition: assigns.h:23
assigns_clause_targett(const exprt &object, code_contractst &contract, messaget &log_parameter, const irep_idt &function_id)
Definition: assigns.cpp:22
symbol_exprt target
Definition: assigns.h:48
exprt alias_expression(const exprt &lhs)
Definition: assigns.cpp:64
const exprt & get_direct_pointer() const
Definition: assigns.cpp:109
std::vector< symbol_exprt > temporary_declarations() const
Definition: assigns.cpp:57
const exprt pointer_object
Definition: assigns.h:44
goto_programt init_block
Definition: assigns.h:46
exprt compatible_expression(const assigns_clause_targett &called_target)
Definition: assigns.cpp:103
const irep_idt & target_id
Definition: assigns.h:49
goto_programt & get_init_block()
Definition: assigns.cpp:114
messaget & log
Definition: assigns.h:47
const code_contractst & contract
Definition: assigns.h:45
static exprt pointer_for(const exprt &object)
Definition: assigns.h:38
goto_programt havoc_code()
Definition: assigns.cpp:184
exprt alias_expression(const exprt &lhs)
Definition: assigns.cpp:195
code_contractst & parent
Definition: assigns.h:75
goto_programt init_block()
Definition: assigns.cpp:156
const exprt & assigns
Definition: assigns.h:70
const irep_idt function_id
Definition: assigns.h:76
assigns_clause_targett * add_target(exprt target)
Definition: assigns.cpp:143
goto_programt standin_declarations
Definition: assigns.h:73
exprt compatible_expression(const assigns_clauset &called_assigns)
Definition: assigns.cpp:211
messaget log
Definition: assigns.h:77
std::vector< assigns_clause_targett * > targets
Definition: assigns.h:72
goto_programt dead_stmts()
Definition: assigns.cpp:170
assigns_clauset(const exprt &assigns, code_contractst &contract, const irep_idt function_id, messaget log_parameter)
Definition: assigns.cpp:119
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
Expression to hold a symbol (variable)
Definition: std_expr.h:80
Verify and use annotated invariants and pre/post-conditions.
Pointer Logic.