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
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
assigns_clauset::function_id
const irep_idt function_id
Definition: assigns.h:76
assigns_clause_targett::pointer_for
static exprt pointer_for(const exprt &object)
Definition: assigns.h:38
assigns_clauset::targets
std::vector< assigns_clause_targett * > targets
Definition: assigns.h:72
assigns_clause_targett::log
messaget & log
Definition: assigns.h:47
assigns_clause_targett::get_init_block
goto_programt & get_init_block()
Definition: assigns.cpp:114
assigns_clause_targett::alias_expression
exprt alias_expression(const exprt &lhs)
Definition: assigns.cpp:64
assigns_clauset::init_block
goto_programt init_block()
Definition: assigns.cpp:156
assigns_clauset::alias_expression
exprt alias_expression(const exprt &lhs)
Definition: assigns.cpp:195
exprt
Base class for all expressions.
Definition: expr.h:54
assigns_clause_targett::contract
const code_contractst & contract
Definition: assigns.h:45
assigns_clauset::add_target
assigns_clause_targett * add_target(exprt target)
Definition: assigns.cpp:143
assigns_clauset::assigns_clauset
assigns_clauset(const exprt &assigns, code_contractst &contract, const irep_idt function_id, messaget log_parameter)
Definition: assigns.cpp:119
assigns_clause_targett::pointer_object
const exprt pointer_object
Definition: assigns.h:44
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
assigns_clauset::log
messaget log
Definition: assigns.h:77
assigns_clause_targett::target
symbol_exprt target
Definition: assigns.h:48
assigns_clause_targett::temporary_declarations
std::vector< symbol_exprt > temporary_declarations() const
Definition: assigns.cpp:57
assigns_clauset::parent
code_contractst & parent
Definition: assigns.h:75
code_contractst
Definition: contracts.h:62
assigns_clause_targett::assigns_clause_targett
assigns_clause_targett(const exprt &object, code_contractst &contract, messaget &log_parameter, const irep_idt &function_id)
Definition: assigns.cpp:22
assigns_clause_targett::target_id
const irep_idt & target_id
Definition: assigns.h:49
assigns_clauset
Definition: assigns.h:53
assigns_clauset::compatible_expression
exprt compatible_expression(const assigns_clauset &called_assigns)
Definition: assigns.cpp:211
assigns_clauset::assigns
const exprt & assigns
Definition: assigns.h:70
contracts.h
Verify and use annotated invariants and pre/post-conditions.
assigns_clause_targett::~assigns_clause_targett
~assigns_clause_targett()
Definition: assigns.cpp:53
assigns_clauset::havoc_code
goto_programt havoc_code()
Definition: assigns.cpp:184
assigns_clause_targett::get_direct_pointer
const exprt & get_direct_pointer() const
Definition: assigns.cpp:109
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
assigns_clauset::dead_stmts
goto_programt dead_stmts()
Definition: assigns.cpp:170
assigns_clauset::standin_declarations
goto_programt standin_declarations
Definition: assigns.h:73
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:341
assigns_clause_targett::init_block
goto_programt init_block
Definition: assigns.h:46
assigns_clauset::~assigns_clauset
~assigns_clauset()
Definition: assigns.cpp:135
assigns_clause_targett::compatible_expression
exprt compatible_expression(const assigns_clause_targett &called_target)
Definition: assigns.cpp:103
assigns_clause_targett
A base class for assigns clause targets.
Definition: assigns.h:23