Skip to content

Commit 093a216

Browse files
kroeningkroening
committed
move goto_instruction_code.h to goto-programs/
The classes in goto_instruction_code.h are the representation of the instructions of goto programs, and thus belong into the goto-programs subdirectory.
1 parent 6b88028 commit 093a216

31 files changed

+128
-87
lines changed

‎jbmc/src/java_bytecode/character_refine_preprocess.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,8 @@ Date: March 2017
2020
#ifndef CPROVER_JAVA_BYTECODE_CHARACTER_REFINE_PREPROCESS_H
2121
#define CPROVER_JAVA_BYTECODE_CHARACTER_REFINE_PREPROCESS_H
2222

23-
#include <util/goto_instruction_code.h>
23+
#include <goto-programs/goto_instruction_code.h>
24+
2425
#include <util/mp_arith.h>
2526
#include <util/std_code.h>
2627

‎jbmc/src/java_bytecode/code_with_references.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,9 @@ Author: Romain Brenguier, [email protected]
99
#include "code_with_references.h"
1010
#include "java_types.h"
1111

12+
#include <goto-programs/goto_instruction_code.h>
13+
1214
#include <util/arith_tools.h>
13-
#include <util/goto_instruction_code.h>
1415

1516
codet allocate_array(
1617
const exprt &expr,

‎jbmc/src/java_bytecode/java_bytecode_instrument.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,9 +10,10 @@ Date: June 2017
1010

1111
#include "java_bytecode_instrument.h"
1212

13+
#include <goto-programs/goto_instruction_code.h>
14+
1315
#include <util/arith_tools.h>
1416
#include <util/c_types.h>
15-
#include <util/goto_instruction_code.h>
1617
#include <util/std_code.h>
1718
#include <util/symbol_table.h>
1819

‎jbmc/src/java_bytecode/java_bytecode_typecheck_code.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,8 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include "java_bytecode_typecheck.h"
1313

14-
#include <util/goto_instruction_code.h>
14+
#include <goto-programs/goto_instruction_code.h>
15+
1516
#include <util/std_code.h>
1617

1718
void java_bytecode_typecheckt::typecheck_code(codet &code)

‎jbmc/src/java_bytecode/lift_clinit_calls.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,9 @@ Author: Diffblue Ltd.
1212

1313
#include <java_bytecode/java_static_initializers.h>
1414

15+
#include <goto-programs/goto_instruction_code.h>
16+
1517
#include <util/expr_iterator.h>
16-
#include <util/goto_instruction_code.h>
1718

1819
#include <algorithm>
1920

‎jbmc/unit/java-testing-utils/require_goto_statements.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,8 @@ Author: Diffblue Ltd.
99
/// \file
1010
/// Utilties for inspecting goto functions
1111

12-
#include <util/goto_instruction_code.h>
12+
#include <goto-programs/goto_instruction_code.h>
13+
1314
#include <util/optional.h>
1415

1516
#include <regex>

‎jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,9 @@ Author: Romain Brenguier, [email protected]
1515
#include <testing-utils/expr_query.h>
1616
#include <testing-utils/use_catch.h>
1717

18+
#include <goto-programs/goto_instruction_code.h>
19+
1820
#include <util/arith_tools.h>
19-
#include <util/goto_instruction_code.h>
2021
#include <util/json.h>
2122
#include <util/symbol_table.h>
2223

‎jbmc/unit/java_bytecode/java_static_initializers/java_static_initializers.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,9 @@ Author: Diffblue Ltd.
1515
#include <testing-utils/expr_query.h>
1616
#include <testing-utils/use_catch.h>
1717

18+
#include <goto-programs/goto_instruction_code.h>
19+
1820
#include <util/arith_tools.h>
19-
#include <util/goto_instruction_code.h>
2021
#include <util/json.h>
2122
#include <util/symbol_table.h>
2223

‎jbmc/unit/java_bytecode/java_static_initializers/module_dependencies.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
goto-programs
12
java_bytecode
23
testing-utils
34
util

‎src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,11 +14,12 @@ Author: Daniel Kroening, [email protected]
1414
#include <util/arith_tools.h>
1515
#include <util/c_types.h>
1616
#include <util/cprover_prefix.h>
17-
#include <util/goto_instruction_code.h>
1817
#include <util/pointer_expr.h>
1918
#include <util/std_types.h>
2019
#include <util/string_constant.h>
2120

21+
#include <goto-programs/goto_instruction_code.h>
22+
2223
#include <atomic>
2324

2425
#include "c_expr.h"

‎src/ansi-c/c_typecheck_type.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,11 +13,12 @@ Author: Daniel Kroening, [email protected]
1313

1414
#include <unordered_set>
1515

16+
#include <goto-programs/goto_instruction_code.h>
17+
1618
#include <util/arith_tools.h>
1719
#include <util/c_types.h>
1820
#include <util/config.h>
1921
#include <util/fresh_symbol.h>
20-
#include <util/goto_instruction_code.h>
2122
#include <util/mathematical_types.h>
2223
#include <util/pointer_expr.h>
2324
#include <util/pointer_offset_size.h>

‎src/ansi-c/expr2c_class.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,9 +16,10 @@ Author: Daniel Kroening, [email protected]
1616
#include <unordered_map>
1717
#include <unordered_set>
1818

19+
#include <goto-programs/goto_instruction_code.h>
20+
1921
#include <util/bitvector_expr.h>
2022
#include <util/byte_operators.h>
21-
#include <util/goto_instruction_code.h>
2223
#include <util/mathematical_expr.h>
2324
#include <util/std_code.h>
2425

‎src/cpp/cpp_typecheck_constructor.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,9 +11,10 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include "cpp_typecheck.h"
1313

14+
#include <goto-programs/goto_instruction_code.h>
15+
1416
#include <util/arith_tools.h>
1517
#include <util/c_types.h>
16-
#include <util/goto_instruction_code.h>
1718
#include <util/pointer_expr.h>
1819
#include <util/std_code.h>
1920

‎src/cpp/cpp_typecheck_destructor.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,8 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include "cpp_typecheck.h"
1313

14-
#include <util/goto_instruction_code.h>
14+
#include <goto-programs/goto_instruction_code.h>
15+
1516
#include <util/pointer_expr.h>
1617

1718
bool cpp_typecheckt::find_dtor(const symbolt &symbol) const

‎src/cpp/cpp_typecheck_initializer.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,10 +11,11 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include "cpp_typecheck.h"
1313

14+
#include <goto-programs/goto_instruction_code.h>
15+
1416
#include <util/arith_tools.h>
1517
#include <util/c_types.h>
1618
#include <util/expr_initializer.h>
17-
#include <util/goto_instruction_code.h>
1819
#include <util/pointer_expr.h>
1920
#include <util/pointer_offset_size.h>
2021

‎src/goto-instrument/object_id.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,8 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include "object_id.h"
1313

14-
#include <util/goto_instruction_code.h>
14+
#include <goto-programs/goto_instruction_code.h>
15+
1516
#include <util/pointer_expr.h>
1617

1718
enum class get_modet { LHS_R, LHS_W, READ };

‎src/goto-programs/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ SRC = allocate_objects.cpp \
2121
goto_functions.cpp \
2222
goto_inline_class.cpp \
2323
goto_inline.cpp \
24+
goto_instruction_code.cpp \
2425
goto_program.cpp \
2526
goto_trace.cpp \
2627
graphml_witness.cpp \

‎src/goto-programs/allocate_objects.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,8 @@ Author: Daniel Kroening, [email protected]
99
#ifndef CPROVER_UTIL_ALLOCATE_OBJECTS_H
1010
#define CPROVER_UTIL_ALLOCATE_OBJECTS_H
1111

12-
#include <util/goto_instruction_code.h>
12+
#include "goto_instruction_code.h"
13+
1314
#include <util/namespace.h>
1415
#include <util/source_location.h>
1516
#include <util/std_code.h>

‎src/goto-programs/destructor.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,8 +10,8 @@ Author: Daniel Kroening, [email protected]
1010
/// Destructor Calls
1111

1212
#include "destructor.h"
13+
#include "goto_instruction_code.h"
1314

14-
#include <util/goto_instruction_code.h>
1515
#include <util/namespace.h>
1616

1717
code_function_callt get_destructor(

‎src/goto-programs/goto_instruction_code.cpp

Lines changed: 72 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,72 @@
1+
/*******************************************************************\
2+
3+
Module: Data structures representing instructions in a GOTO program
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Data structures representing instructions in a GOTO program
11+
12+
#include "goto_instruction_code.h"
13+
14+
#include <util/arith_tools.h>
15+
#include <util/c_types.h>
16+
#include <util/string_constant.h>
17+
18+
code_inputt::code_inputt(
19+
std::vector<exprt> arguments,
20+
optionalt<source_locationt> location)
21+
: codet{ID_input, std::move(arguments)}
22+
{
23+
if(location)
24+
add_source_location() = std::move(*location);
25+
check(*this, validation_modet::INVARIANT);
26+
}
27+
28+
code_inputt::code_inputt(
29+
const irep_idt &description,
30+
exprt expression,
31+
optionalt<source_locationt> location)
32+
: code_inputt{{address_of_exprt(index_exprt(
33+
string_constantt(description),
34+
from_integer(0, index_type()))),
35+
std::move(expression)},
36+
std::move(location)}
37+
{
38+
}
39+
40+
void code_inputt::check(const codet &code, const validation_modet vm)
41+
{
42+
DATA_CHECK(
43+
vm, code.operands().size() >= 2, "input must have at least two operands");
44+
}
45+
46+
code_outputt::code_outputt(
47+
std::vector<exprt> arguments,
48+
optionalt<source_locationt> location)
49+
: codet{ID_output, std::move(arguments)}
50+
{
51+
if(location)
52+
add_source_location() = std::move(*location);
53+
check(*this, validation_modet::INVARIANT);
54+
}
55+
56+
code_outputt::code_outputt(
57+
const irep_idt &description,
58+
exprt expression,
59+
optionalt<source_locationt> location)
60+
: code_outputt{{address_of_exprt(index_exprt(
61+
string_constantt(description),
62+
from_integer(0, index_type()))),
63+
std::move(expression)},
64+
std::move(location)}
65+
{
66+
}
67+
68+
void code_outputt::check(const codet &code, const validation_modet vm)
69+
{
70+
DATA_CHECK(
71+
vm, code.operands().size() >= 2, "output must have at least two operands");
72+
}

‎src/util/goto_instruction_code.h renamed to ‎src/goto-programs/goto_instruction_code.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@ Author: Daniel Kroening, [email protected]
99
#ifndef CPROVER_UTIL_GOTO_INSTRUCTION_CODE_H
1010
#define CPROVER_UTIL_GOTO_INSTRUCTION_CODE_H
1111

12-
#include "std_code_base.h"
13-
#include "std_expr.h"
12+
#include <util/std_code_base.h>
13+
#include <util/std_expr.h>
1414

1515
/// A \ref codet representing an assignment in the program.
1616
/// For example, if an expression `e1` is represented as an \ref exprt `expr1`

‎src/goto-programs/goto_program.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,13 +12,14 @@ Author: Daniel Kroening, [email protected]
1212
#ifndef CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
1313
#define CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
1414

15+
#include "goto_instruction_code.h"
16+
1517
#include <iosfwd>
1618
#include <set>
1719
#include <limits>
1820
#include <string>
1921

2022
#include <util/deprecate.h>
21-
#include <util/goto_instruction_code.h>
2223
#include <util/invariant.h>
2324
#include <util/namespace.h>
2425
#include <util/source_location.h>

‎src/goto-programs/validate_code.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,8 @@ Author: Daniel Poetzl
1212
# include <iostream>
1313
#endif
1414

15-
#include <util/goto_instruction_code.h>
15+
#include "goto_instruction_code.h"
16+
1617
#include <util/std_code.h>
1718
#include <util/validate_helpers.h>
1819

‎src/goto-programs/wp.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -13,11 +13,11 @@ Author: Daniel Kroening, [email protected]
1313

1414
// #include <langapi/language_util.h>
1515

16-
#include <util/goto_instruction_code.h>
17-
#include <util/pointer_expr.h>
18-
#include <util/std_code.h>
16+
#include "goto_instruction_code.h"
1917

2018
#include <util/invariant.h>
19+
#include <util/pointer_expr.h>
20+
#include <util/std_code.h>
2121

2222
bool has_nondet(const exprt &dest)
2323
{

‎src/jsil/jsil_convert.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,8 @@ Author: Michael Tautschnig, [email protected]
1111

1212
#include "jsil_convert.h"
1313

14-
#include <util/goto_instruction_code.h>
14+
#include <goto-programs/goto_instruction_code.h>
15+
1516
#include <util/message.h>
1617
#include <util/symbol_table.h>
1718

‎src/jsil/jsil_typecheck.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,8 +11,9 @@ Author: Michael Tautschnig, [email protected]
1111

1212
#include "jsil_typecheck.h"
1313

14+
#include <goto-programs/goto_instruction_code.h>
15+
1416
#include <util/bitvector_types.h>
15-
#include <util/goto_instruction_code.h>
1617
#include <util/prefix.h>
1718
#include <util/std_code.h>
1819
#include <util/symbol_table.h>

‎src/jsil/parser.y

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,8 @@ extern char *yyjsiltext;
1111
#define YYSTYPE unsigned
1212
#define YYSTYPE_IS_TRIVIAL 1
1313

14-
#include <util/goto_instruction_code.h>
14+
#include <goto-programs/goto_instruction_code.h>
15+
1516
#include <util/string_constant.h>
1617

1718
#include "jsil_y.tab.h"

‎src/linking/static_lifetime_init.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,10 +8,11 @@ Author: Daniel Kroening, [email protected]
88

99
#include "static_lifetime_init.h"
1010

11+
#include <goto-programs/goto_instruction_code.h>
12+
1113
#include <util/arith_tools.h>
1214
#include <util/c_types.h>
1315
#include <util/expr_initializer.h>
14-
#include <util/goto_instruction_code.h>
1516
#include <util/namespace.h>
1617
#include <util/prefix.h>
1718
#include <util/std_code.h>

‎src/pointer-analysis/value_set_fi.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,10 +13,11 @@ Author: Daniel Kroening, [email protected]
1313

1414
#include <ostream>
1515

16+
#include <goto-programs/goto_instruction_code.h>
17+
1618
#include <util/arith_tools.h>
1719
#include <util/byte_operators.h>
1820
#include <util/c_types.h>
19-
#include <util/goto_instruction_code.h>
2021
#include <util/namespace.h>
2122
#include <util/pointer_expr.h>
2223
#include <util/prefix.h>

‎src/statement-list/statement_list_typecheck.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,9 @@ Author: Matthias Weiss, [email protected]
1212
#include "statement_list_typecheck.h"
1313
#include "converters/statement_list_types.h"
1414

15+
#include <goto-programs/goto_instruction_code.h>
16+
1517
#include <util/cprover_prefix.h>
16-
#include <util/goto_instruction_code.h>
1718
#include <util/message.h>
1819
#include <util/namespace.h>
1920
#include <util/pointer_expr.h>

0 commit comments

Comments
 (0)