-
Notifications
You must be signed in to change notification settings - Fork 273
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
cleanup the includes in src/java_bytecode
- Loading branch information
Daniel Kroening
committed
May 1, 2018
1 parent
1050637
commit 392c765
Showing
8 changed files
with
35 additions
and
28 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -12,12 +12,12 @@ Author: Daniel Kroening, [email protected] | |
#ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_H | ||
#define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_H | ||
|
||
#include <util/symbol_table.h> | ||
#include <util/message.h> | ||
#include "ci_lazy_methods_needed.h" | ||
#include "java_bytecode_parse_tree.h" | ||
#include "java_string_library_preprocess.h" | ||
|
||
#include "java_bytecode_parse_tree.h" | ||
#include <java_bytecode/ci_lazy_methods_needed.h> | ||
#include <util/message.h> | ||
#include <util/symbol_table.h> | ||
|
||
class class_hierarchyt; | ||
|
||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -12,14 +12,16 @@ Author: Daniel Kroening, [email protected] | |
#ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_CLASS_H | ||
#define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_CLASS_H | ||
|
||
#include "ci_lazy_methods_needed.h" | ||
#include "java_bytecode_parse_tree.h" | ||
#include "java_bytecode_convert_class.h" | ||
|
||
#include <util/expanding_vector.h> | ||
#include <util/message.h> | ||
#include <util/std_types.h> | ||
#include <util/std_expr.h> | ||
|
||
#include <analyses/cfg_dominators.h> | ||
#include "java_bytecode_parse_tree.h" | ||
#include "java_bytecode_convert_class.h" | ||
#include <java_bytecode/ci_lazy_methods_needed.h> | ||
|
||
#include <vector> | ||
#include <list> | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -10,22 +10,21 @@ Author: Daniel Kroening, [email protected] | |
#ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H | ||
#define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H | ||
|
||
#include <memory> | ||
|
||
#include <util/cmdline.h> | ||
#include <util/make_unique.h> | ||
|
||
#include <langapi/language.h> | ||
|
||
#include "ci_lazy_methods.h" | ||
#include "ci_lazy_methods_needed.h" | ||
#include "java_class_loader.h" | ||
#include "java_static_initializers.h" | ||
#include "java_string_library_preprocess.h" | ||
#include "object_factory_parameters.h" | ||
#include "select_pointer_type.h" | ||
#include "synthetic_methods_map.h" | ||
|
||
#include <java_bytecode/select_pointer_type.h> | ||
#include <memory> | ||
|
||
#include <util/cmdline.h> | ||
#include <util/make_unique.h> | ||
|
||
#include <langapi/language.h> | ||
|
||
#define JAVA_BYTECODE_LANGUAGE_OPTIONS /*NOLINT*/ \ | ||
"(no-core-models)" \ | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -10,10 +10,11 @@ Author: Daniel Kroening, [email protected] | |
#ifndef CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H | ||
#define CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H | ||
|
||
#include "java_bytecode_language.h" | ||
#include "select_pointer_type.h" | ||
|
||
#include <util/irep.h> | ||
#include <util/symbol.h> | ||
#include <java_bytecode/select_pointer_type.h> | ||
#include <java_bytecode/java_bytecode_language.h> | ||
|
||
#define JAVA_ENTRY_POINT_RETURN_SYMBOL "return'" | ||
#define JAVA_ENTRY_POINT_EXCEPTION_SYMBOL "uncaught_exception'" | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -68,13 +68,13 @@ Author: Daniel Kroening, [email protected] | |
#ifndef CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H | ||
#define CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H | ||
|
||
#include "java_bytecode_language.h" | ||
#include "select_pointer_type.h" | ||
|
||
#include <util/message.h> | ||
#include <util/std_code.h> | ||
#include <util/symbol_table.h> | ||
|
||
#include <java_bytecode/select_pointer_type.h> | ||
#include <java_bytecode/java_bytecode_language.h> | ||
|
||
/// Selects the kind of allocation used by java_object_factory et al. | ||
enum class allocation_typet | ||
{ | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -9,13 +9,14 @@ Author: Chris Smowton, [email protected] | |
#ifndef CPROVER_JAVA_BYTECODE_JAVA_STATIC_INITIALIZERS_H | ||
#define CPROVER_JAVA_BYTECODE_JAVA_STATIC_INITIALIZERS_H | ||
|
||
#include "object_factory_parameters.h" | ||
#include "select_pointer_type.h" | ||
#include "synthetic_methods_map.h" | ||
|
||
#include <unordered_set> | ||
|
||
#include <util/symbol_table.h> | ||
#include <util/std_code.h> | ||
#include <java_bytecode/object_factory_parameters.h> | ||
#include <java_bytecode/select_pointer_type.h> | ||
#include <java_bytecode/synthetic_methods_map.h> | ||
|
||
irep_idt clinit_wrapper_name(const irep_idt &class_name); | ||
|
||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -12,6 +12,8 @@ Author: Daniel Kroening, [email protected] | |
#include <cstdint> | ||
#include <limits> | ||
|
||
#include <util/irep.h> | ||
|
||
#define MAX_NONDET_ARRAY_LENGTH_DEFAULT 5 | ||
#define MAX_NONDET_STRING_LENGTH std::numeric_limits<std::int32_t>::max() | ||
#define MAX_NONDET_TREE_DEPTH 5 | ||
|