File tree 8 files changed +35
-28
lines changed
8 files changed +35
-28
lines changed Original file line number Diff line number Diff line change 12
12
#ifndef CPROVER_JAVA_BYTECODE_GATHER_METHODS_LAZILY_H
13
13
#define CPROVER_JAVA_BYTECODE_GATHER_METHODS_LAZILY_H
14
14
15
+ #include " ci_lazy_methods_needed.h"
16
+ #include " java_bytecode_parse_tree.h"
17
+ #include " java_class_loader.h"
18
+ #include " select_pointer_type.h"
19
+ #include " synthetic_methods_map.h"
20
+
15
21
#include < map>
16
22
#include < functional>
17
23
18
24
#include < util/irep.h>
19
25
#include < util/symbol_table.h>
20
26
#include < util/message.h>
27
+
21
28
#include < goto-programs/class_hierarchy.h>
22
- #include < java_bytecode/java_bytecode_parse_tree.h>
23
- #include < java_bytecode/java_class_loader.h>
24
- #include < java_bytecode/ci_lazy_methods_needed.h>
25
- #include < java_bytecode/select_pointer_type.h>
26
- #include < java_bytecode/synthetic_methods_map.h>
27
29
28
30
class java_string_library_preprocesst ;
29
31
Original file line number Diff line number Diff line change 12
12
#ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_H
13
13
#define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_H
14
14
15
- #include < util/symbol_table.h >
16
- #include < util/message.h >
15
+ #include " ci_lazy_methods_needed.h "
16
+ #include " java_bytecode_parse_tree.h "
17
17
#include " java_string_library_preprocess.h"
18
18
19
- #include " java_bytecode_parse_tree.h "
20
- #include < java_bytecode/ci_lazy_methods_needed .h>
19
+ #include < util/message.h >
20
+ #include < util/symbol_table .h>
21
21
22
22
class class_hierarchyt ;
23
23
Original file line number Diff line number Diff line change 12
12
#ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_CLASS_H
13
13
#define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_CLASS_H
14
14
15
+ #include " ci_lazy_methods_needed.h"
16
+ #include " java_bytecode_parse_tree.h"
17
+ #include " java_bytecode_convert_class.h"
18
+
15
19
#include < util/expanding_vector.h>
16
20
#include < util/message.h>
17
21
#include < util/std_types.h>
18
22
#include < util/std_expr.h>
23
+
19
24
#include < analyses/cfg_dominators.h>
20
- #include " java_bytecode_parse_tree.h"
21
- #include " java_bytecode_convert_class.h"
22
- #include < java_bytecode/ci_lazy_methods_needed.h>
23
25
24
26
#include < vector>
25
27
#include < list>
Original file line number Diff line number Diff line change 10
10
#ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H
11
11
#define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H
12
12
13
- #include < memory>
14
-
15
- #include < util/cmdline.h>
16
- #include < util/make_unique.h>
17
-
18
- #include < langapi/language.h>
19
-
20
13
#include " ci_lazy_methods.h"
21
14
#include " ci_lazy_methods_needed.h"
22
15
#include " java_class_loader.h"
23
16
#include " java_static_initializers.h"
24
17
#include " java_string_library_preprocess.h"
25
18
#include " object_factory_parameters.h"
19
+ #include " select_pointer_type.h"
26
20
#include " synthetic_methods_map.h"
27
21
28
- #include < java_bytecode/select_pointer_type.h>
22
+ #include < memory>
23
+
24
+ #include < util/cmdline.h>
25
+ #include < util/make_unique.h>
26
+
27
+ #include < langapi/language.h>
29
28
30
29
#define JAVA_BYTECODE_LANGUAGE_OPTIONS /* NOLINT*/ \
31
30
" (no-core-models)" \
Original file line number Diff line number Diff line change 10
10
#ifndef CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H
11
11
#define CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H
12
12
13
+ #include " java_bytecode_language.h"
14
+ #include " select_pointer_type.h"
15
+
13
16
#include < util/irep.h>
14
17
#include < util/symbol.h>
15
- #include < java_bytecode/select_pointer_type.h>
16
- #include < java_bytecode/java_bytecode_language.h>
17
18
18
19
#define JAVA_ENTRY_POINT_RETURN_SYMBOL " return'"
19
20
#define JAVA_ENTRY_POINT_EXCEPTION_SYMBOL " uncaught_exception'"
Original file line number Diff line number Diff line change 68
68
#ifndef CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H
69
69
#define CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H
70
70
71
+ #include " java_bytecode_language.h"
72
+ #include " select_pointer_type.h"
73
+
71
74
#include < util/message.h>
72
75
#include < util/std_code.h>
73
76
#include < util/symbol_table.h>
74
77
75
- #include < java_bytecode/select_pointer_type.h>
76
- #include < java_bytecode/java_bytecode_language.h>
77
-
78
78
// / Selects the kind of allocation used by java_object_factory et al.
79
79
enum class allocation_typet
80
80
{
Original file line number Diff line number Diff line change 9
9
#ifndef CPROVER_JAVA_BYTECODE_JAVA_STATIC_INITIALIZERS_H
10
10
#define CPROVER_JAVA_BYTECODE_JAVA_STATIC_INITIALIZERS_H
11
11
12
+ #include " object_factory_parameters.h"
13
+ #include " select_pointer_type.h"
14
+ #include " synthetic_methods_map.h"
15
+
12
16
#include < unordered_set>
13
17
14
18
#include < util/symbol_table.h>
15
19
#include < util/std_code.h>
16
- #include < java_bytecode/object_factory_parameters.h>
17
- #include < java_bytecode/select_pointer_type.h>
18
- #include < java_bytecode/synthetic_methods_map.h>
19
20
20
21
irep_idt clinit_wrapper_name (const irep_idt &class_name);
21
22
Original file line number Diff line number Diff line change 12
12
#include < cstdint>
13
13
#include < limits>
14
14
15
+ #include < util/irep.h>
16
+
15
17
#define MAX_NONDET_ARRAY_LENGTH_DEFAULT 5
16
18
#define MAX_NONDET_STRING_LENGTH std::numeric_limits<std::int32_t >::max()
17
19
#define MAX_NONDET_TREE_DEPTH 5
You can’t perform that action at this time.
0 commit comments