Skip to content

Commit 3d1e3fb

Browse files
committed
move validate_code to goto-programs/
This code operates on goto program instructions exclusively, and thus belongs into the goto-programs/ subdirectory.
1 parent d873a55 commit 3d1e3fb

File tree

6 files changed

+7
-18
lines changed

6 files changed

+7
-18
lines changed

src/goto-programs/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -69,6 +69,7 @@ SRC = allocate_objects.cpp \
6969
string_instrumentation.cpp \
7070
structured_trace_util.cpp \
7171
system_library_symbols.cpp \
72+
validate_code.cpp \
7273
validate_goto_model.cpp \
7374
vcd_goto_trace.cpp \
7475
wp.cpp \

src/goto-programs/goto_program.cpp

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

1212
#include "goto_program.h"
1313

14+
#include "validate_code.h"
15+
1416
#include <iomanip>
1517

1618
#include <util/base_type.h>

src/util/validate_code.cpp renamed to src/goto-programs/validate_code.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -9,12 +9,12 @@ Author: Daniel Poetzl
99
#include "validate_code.h"
1010

1111
#ifdef REPORT_UNIMPLEMENTED_CODE_CHECKS
12-
#include <iostream>
12+
# include <iostream>
1313
#endif
1414

15-
#include "goto_instruction_code.h"
16-
#include "std_code.h"
17-
#include "validate_helpers.h"
15+
#include <util/goto_instruction_code.h>
16+
#include <util/std_code.h>
17+
#include <util/validate_helpers.h>
1818

1919
#define CALL_ON_CODE(code_type) \
2020
C<codet, code_type>()(code, std::forward<Args>(args)...)
File renamed without changes.

src/util/Makefile

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -106,7 +106,6 @@ SRC = arith_tools.cpp \
106106
unicode.cpp \
107107
union_find.cpp \
108108
union_find_replace.cpp \
109-
validate_code.cpp \
110109
validate_expressions.cpp \
111110
validate_types.cpp \
112111
version.cpp \

src/util/std_code.h

Lines changed: 0 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -190,19 +190,6 @@ class code_blockt:public codet
190190
}
191191

192192
codet &find_last_statement();
193-
194-
static void validate_full(
195-
const codet &code,
196-
const namespacet &ns,
197-
const validation_modet vm = validation_modet::INVARIANT)
198-
{
199-
for(const auto &statement : code.operands())
200-
{
201-
DATA_CHECK(
202-
vm, code.id() == ID_code, "code block must be made up of codet");
203-
validate_full_code(to_code(statement), ns, vm);
204-
}
205-
}
206193
};
207194

208195
template<> inline bool can_cast_expr<code_blockt>(const exprt &base)

0 commit comments

Comments
 (0)