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/cprover_prefix.h>
17#include <util/namespace.h>
18#include <util/std_expr.h>
20#include <util/symbol.h>
21
23 std::vector<exprt> arguments,
25 : codet{ID_input, std::move(arguments)}
26{
27 if(location)
28 add_source_location() = std::move(*location);
30}
31
33 const irep_idt &description,
34 exprt expression,
37 string_constantt(description),
39 std::move(expression)},
40 std::move(location)}
41{
42}
43
44void code_inputt::check(const codet &code, const validation_modet vm)
45{
47 vm, code.operands().size() >= 2, "input must have at least two operands");
48}
49
51 std::vector<exprt> arguments,
53 : codet{ID_output, std::move(arguments)}
54{
55 if(location)
56 add_source_location() = std::move(*location);
58}
59
61 const irep_idt &description,
62 exprt expression,
65 string_constantt(description),
67 std::move(expression)},
68 std::move(location)}
69{
70}
71
72void code_outputt::check(const codet &code, const validation_modet vm)
73{
75 vm, code.operands().size() >= 2, "output must have at least two operands");
76}
77
79havoc_slice_call(const exprt &p, const exprt &size, const namespacet &ns)
80{
81 irep_idt identifier = CPROVER_PREFIX "havoc_slice";
82 symbol_exprt havoc_slice_function = ns.lookup(identifier).symbol_expr();
83 code_function_callt::argumentst arguments = {p, size};
85 std::move(arguments)};
86}
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:563
goto_instruction_codet representation of a function call statement.
A goto_instruction_codet representing the declaration that an input of a particular description has a...
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 goto_instruction_codet &code, const validation_modet vm=validation_modet::INVARIANT)
A goto_instruction_codet representing the declaration that an output of a particular description has ...
static void check(const goto_instruction_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:39
Base class for all expressions.
Definition expr.h:56
operandst & operands()
Definition expr.h:94
source_locationt & add_source_location()
Definition expr.h:228
Array index operator.
Definition std_expr.h:1410
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:113
#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.
Symbol table entry.
#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