cprover
havoc_assigns_clause_targets.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Havoc multiple and possibly dependent targets simultaneously
4
5Author: Remi Delmas, delmasrd@amazon.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_HAVOC_ASSIGNS_CLAUSE_TARGETS_H
13#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_HAVOC_ASSIGNS_CLAUSE_TARGETS_H
14
16#include <util/expr.h>
17
18class namespacet;
19class symbol_tablet;
20class goto_programt;
21class goto_functionst;
23
55{
56public:
58 const irep_idt &_function_id,
59 const std::vector<exprt> &_targets,
60 const goto_functionst &_functions,
61 const source_locationt &_source_location,
62 symbol_tablet &_st,
63 message_handlert &_message_handler)
64 : instrument_spec_assignst(_function_id, _functions, _st, _message_handler),
65 targets(_targets),
66 source_location(_source_location)
67 {
68 }
69
72
73private:
102 void havoc_if_valid(car_exprt car, goto_programt &dest);
103
104 const std::vector<exprt> &targets;
106};
107#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_HAVOC_ASSIGNS_CLAUSE_TARGETS_H
Class that represents a normalized conditional address range, with:
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
Class to generate havocking instructions for target expressions of a function contract's assign claus...
const std::vector< exprt > & targets
void havoc_if_valid(car_exprt car, goto_programt &dest)
Generates instructions to conditionally havoc the given conditional address range expression car,...
void get_instructions(goto_programt &dest)
Generates the assigns clause replacement instructions in dest.
havoc_assigns_clause_targetst(const irep_idt &_function_id, const std::vector< exprt > &_targets, const goto_functionst &_functions, const source_locationt &_source_location, symbol_tablet &_st, message_handlert &_message_handler)
A class that generates instrumentation for assigns clause checking.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The symbol table.
Definition: symbol_table.h:14
Specify write set in function contracts.