cprover
Loading...
Searching...
No Matches
goto_instruction_code.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Data structures representing instructions in a GOTO program
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
13
14#include <util/arith_tools.h>
15#include <util/c_types.h>
16#include <util/namespace.h>
17#include <util/std_expr.h>
20
22 std::vector<exprt> arguments,
24 : codet{ID_input, std::move(arguments)}
25{
26 if(location)
27 add_source_location() = std::move(*location);
29}
30
32 const irep_idt &description,
33 exprt expression,
36 string_constantt(description),
38 std::move(expression)},
39 std::move(location)}
40{
41}
42
43void code_inputt::check(const codet &code, const validation_modet vm)
44{
46 vm, code.operands().size() >= 2, "input must have at least two operands");
47}
48
50 std::vector<exprt> arguments,
52 : codet{ID_output, std::move(arguments)}
53{
54 if(location)
55 add_source_location() = std::move(*location);
57}
58
60 const irep_idt &description,
61 exprt expression,
64 string_constantt(description),
66 std::move(expression)},
67 std::move(location)}
68{
69}
70
71void code_outputt::check(const codet &code, const validation_modet vm)
72{
74 vm, code.operands().size() >= 2, "output must have at least two operands");
75}
76
78havoc_slice_call(const exprt &p, const exprt &size, const namespacet &ns)
79{
80 irep_idt identifier = CPROVER_PREFIX "havoc_slice";
81 symbol_exprt havoc_slice_function = ns.lookup(identifier).symbol_expr();
82 code_function_callt::argumentst arguments = {p, size};
84 std::move(arguments)};
85}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bitvector_typet c_index_type()
Definition c_types.cpp:16
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
codet representation of a function call statement.
A codet representing the declaration that an input of a particular description has a value which corr...
code_inputt(std::vector< exprt > arguments, optionalt< source_locationt > location={})
This constructor is for support of calls to __CPROVER_input in user code.
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
A codet representing the declaration that an output of a particular description has a value which cor...
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
code_outputt(std::vector< exprt > arguments, optionalt< source_locationt > location={})
This constructor is for support of calls to __CPROVER_output in user code.
Data structure for representing an arbitrary statement in a program.
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
operandst & operands()
Definition expr.h:92
source_locationt & add_source_location()
Definition expr.h:235
Array index operator.
Definition std_expr.h:1328
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Expression to hold a symbol (variable)
Definition std_expr.h:80
#define CPROVER_PREFIX
code_function_callt havoc_slice_call(const exprt &p, const exprt &size, const namespacet &ns)
Builds a code_function_callt to __CPROVER_havoc_slice(p, size).
STL namespace.
API to expression classes.
Author: Diffblue Ltd.
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition validate.h:22
validation_modet