cprover
|
#include <java_bytecode_language.h>
Public Member Functions | |
java_bytecode_language_optionst (const optionst &options, messaget &log) | |
java_bytecode_language_optionst ()=default | |
Public Attributes | |
bool | assume_inputs_non_null = false |
assume inputs variables to be non-null More... | |
bool | string_refinement_enabled = false |
bool | throw_runtime_exceptions = false |
bool | assert_uncaught_exceptions = false |
bool | throw_assertion_error = false |
bool | threading_support = false |
bool | nondet_static = false |
bool | ignore_manifest_main_class = false |
bool | assert_no_exceptions_thrown = false |
Transform athrow bytecode instructions into assert FALSE followed by assume FALSE . More... | |
size_t | max_user_array_length = 0 |
max size for user code created arrays More... | |
lazy_methods_modet | lazy_methods_mode |
std::vector< irep_idt > | java_load_classes |
list of classes to force load even without reference from the entry point More... | |
std::string | java_cp_include_files |
optionalt< json_objectt > | static_values_json |
JSON which contains initial values of static fields (right after the static initializer of the class was run). More... | |
std::unordered_set< std::string > | no_load_classes |
List of classes to never load. More... | |
std::vector< load_extra_methodst > | extra_methods |
optionalt< prefix_filtert > | method_context |
If set, method bodies are only elaborated if they pass the filter. More... | |
bool | should_lift_clinit_calls |
Should we lift clinit calls in function bodies to the top? For example, turning if(x) A.clinit() else B.clinit() into A.clinit(); B.clinit(); if(x) ... More... | |
optionalt< std::string > | main_jar |
If set then a JAR file has been given via the -jar option. More... | |
Definition at line 214 of file java_bytecode_language.h.
java_bytecode_language_optionst::java_bytecode_language_optionst | ( | const optionst & | options, |
messaget & | log | ||
) |
Definition at line 142 of file java_bytecode_language.cpp.
|
default |
bool java_bytecode_language_optionst::assert_no_exceptions_thrown = false |
Transform athrow
bytecode instructions into assert FALSE
followed by assume FALSE
.
Definition at line 232 of file java_bytecode_language.h.
bool java_bytecode_language_optionst::assert_uncaught_exceptions = false |
Definition at line 224 of file java_bytecode_language.h.
bool java_bytecode_language_optionst::assume_inputs_non_null = false |
assume inputs variables to be non-null
Definition at line 221 of file java_bytecode_language.h.
std::vector<load_extra_methodst> java_bytecode_language_optionst::extra_methods |
Definition at line 250 of file java_bytecode_language.h.
bool java_bytecode_language_optionst::ignore_manifest_main_class = false |
Definition at line 228 of file java_bytecode_language.h.
std::string java_bytecode_language_optionst::java_cp_include_files |
Definition at line 241 of file java_bytecode_language.h.
std::vector<irep_idt> java_bytecode_language_optionst::java_load_classes |
list of classes to force load even without reference from the entry point
Definition at line 240 of file java_bytecode_language.h.
lazy_methods_modet java_bytecode_language_optionst::lazy_methods_mode |
Definition at line 236 of file java_bytecode_language.h.
optionalt<std::string> java_bytecode_language_optionst::main_jar |
If set then a JAR file has been given via the -jar option.
Definition at line 267 of file java_bytecode_language.h.
size_t java_bytecode_language_optionst::max_user_array_length = 0 |
max size for user code created arrays
Definition at line 235 of file java_bytecode_language.h.
optionalt<prefix_filtert> java_bytecode_language_optionst::method_context |
If set, method bodies are only elaborated if they pass the filter.
Methods that do not pass the filter are "excluded": their symbols will include all the meta-information that is available from the bytecode (parameter types, return type, accessibility etc.) but the value of the symbol (corresponding to the body of the method) will be replaced with the same kind of "return nondet null or instance of return type" body that we use for stubbed methods. The original method body will never be loaded.
Definition at line 259 of file java_bytecode_language.h.
std::unordered_set<std::string> java_bytecode_language_optionst::no_load_classes |
List of classes to never load.
Definition at line 248 of file java_bytecode_language.h.
bool java_bytecode_language_optionst::nondet_static = false |
Definition at line 227 of file java_bytecode_language.h.
bool java_bytecode_language_optionst::should_lift_clinit_calls |
Should we lift clinit calls in function bodies to the top? For example, turning if(x) A.clinit() else B.clinit()
into A.clinit(); B.clinit(); if(x) ...
Definition at line 264 of file java_bytecode_language.h.
optionalt<json_objectt> java_bytecode_language_optionst::static_values_json |
JSON which contains initial values of static fields (right after the static initializer of the class was run).
This is read from the file specified by the –static-values command-line option.
Definition at line 245 of file java_bytecode_language.h.
bool java_bytecode_language_optionst::string_refinement_enabled = false |
Definition at line 222 of file java_bytecode_language.h.
bool java_bytecode_language_optionst::threading_support = false |
Definition at line 226 of file java_bytecode_language.h.
bool java_bytecode_language_optionst::throw_assertion_error = false |
Definition at line 225 of file java_bytecode_language.h.
bool java_bytecode_language_optionst::throw_runtime_exceptions = false |
Definition at line 223 of file java_bytecode_language.h.