cprover
goto_instruction_code.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Data structures representing instructions in a GOTO program
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "goto_instruction_code.h"
13 
14 #include <util/arith_tools.h>
15 #include <util/c_types.h>
16 #include <util/namespace.h>
17 #include <util/std_expr.h>
18 #include <util/string_constant.h>
19 #include <util/symbol_table_base.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),
37  from_integer(0, c_index_type()))),
38  std::move(expression)},
39  std::move(location)}
40 {
41 }
42 
43 void code_inputt::check(const codet &code, const validation_modet vm)
44 {
45  DATA_CHECK(
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),
65  from_integer(0, c_index_type()))),
66  std::move(expression)},
67  std::move(location)}
68 {
69 }
70 
71 void code_outputt::check(const codet &code, const validation_modet vm)
72 {
73  DATA_CHECK(
74  vm, code.operands().size() >= 2, "output must have at least two operands");
75 }
76 
78 havoc_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};
83  return code_function_callt{std::move(havoc_slice_function),
84  std::move(arguments)};
85 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
bitvector_typet c_index_type()
Definition: c_types.cpp:16
Operator to return the address of an object.
Definition: pointer_expr.h:361
codet representation of a function call statement.
exprt::operandst argumentst
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.
Definition: std_code_base.h:29
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
source_locationt & add_source_location()
Definition: expr.h:235
operandst & operands()
Definition: expr.h:92
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().
Definition: namespace.cpp:138
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).
nonstd::optional< T > optionalt
Definition: optional.h:35
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