File tree 4 files changed +8
-9
lines changed
4 files changed +8
-9
lines changed Original file line number Diff line number Diff line change @@ -78,7 +78,8 @@ goto-harness.dir: util.dir goto-programs.dir langapi.dir linking.dir \
78
78
goto-instrument.dir
79
79
80
80
goto-instrument.dir : languages goto-programs.dir pointer-analysis.dir \
81
- goto-symex.dir linking.dir analyses.dir solvers.dir
81
+ goto-symex.dir linking.dir analyses.dir solvers.dir \
82
+ goto-checker.dir
82
83
83
84
goto-checker.dir : solvers.dir goto-symex.dir goto-programs.dir
84
85
Original file line number Diff line number Diff line change @@ -107,6 +107,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
107
107
../cpp/cpp$(LIBEXT ) \
108
108
../linking/linking$(LIBEXT ) \
109
109
../big-int/big-int$(LIBEXT ) \
110
+ ../goto-checker/goto-checker$(LIBEXT ) \
110
111
../goto-programs/goto-programs$(LIBEXT ) \
111
112
../goto-symex/goto-symex$(LIBEXT ) \
112
113
../assembler/assembler$(LIBEXT ) \
Original file line number Diff line number Diff line change @@ -25,17 +25,16 @@ Author: Qinheping Hu
25
25
#include < analyses/dependence_graph.h>
26
26
#include < ansi-c/cprover_library.h>
27
27
#include < assembler/remove_asm.h>
28
- #include < contracts/contracts.h>
29
- #include < contracts/utils.h>
30
28
#include < cpp/cprover_library.h>
31
29
#include < goto-checker/all_properties_verifier_with_trace_storage.h>
32
30
#include < goto-checker/multi_path_symex_checker.h>
31
+ #include < goto-instrument/contracts/contracts.h>
32
+ #include < goto-instrument/contracts/utils.h>
33
+ #include < goto-instrument/havoc_utils.h>
33
34
#include < langapi/language_util.h>
34
35
#include < pointer-analysis/add_failed_symbols.h>
35
36
#include < solvers/prop/prop.h>
36
37
37
- #include " havoc_utils.h"
38
-
39
38
static bool contains_symbol_prefix (const exprt &expr, const std::string &prefix)
40
39
{
41
40
if (
Original file line number Diff line number Diff line change @@ -9,13 +9,11 @@ Author: Qinheping Hu
9
9
#include " synthesizer_utils.h"
10
10
11
11
#include < analyses/natural_loops.h>
12
-
13
- #include " havoc_utils.h"
12
+ # include < goto-instrument/contracts/utils.h >
13
+ #include < goto-instrument/ havoc_utils.h>
14
14
15
15
#include < sstream>
16
16
17
- #include " contracts/utils.h"
18
-
19
17
goto_programt::const_targett get_loop_end_from_loop_head_and_content (
20
18
const goto_programt::const_targett &loop_head,
21
19
const loop_templatet<goto_programt::const_targett> &loop)
You can’t perform that action at this time.
0 commit comments