#include <java_bytecode_language.h>
Collaboration diagram for java_bytecode_language_optionst: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... | |
Detailed Description
Definition at line 216 of file java_bytecode_language.h.
Constructor & Destructor Documentation
◆ java_bytecode_language_optionst() [1/2]
| java_bytecode_language_optionst::java_bytecode_language_optionst | ( | const optionst & | options, |
| messaget & | log | ||
| ) |
Definition at line 144 of file java_bytecode_language.cpp.
◆ java_bytecode_language_optionst() [2/2]
|
default |
Member Data Documentation
◆ assert_no_exceptions_thrown
| bool java_bytecode_language_optionst::assert_no_exceptions_thrown = false |
Transform athrow bytecode instructions into assert FALSE followed by assume FALSE.
Definition at line 234 of file java_bytecode_language.h.
◆ assert_uncaught_exceptions
| bool java_bytecode_language_optionst::assert_uncaught_exceptions = false |
Definition at line 226 of file java_bytecode_language.h.
◆ assume_inputs_non_null
| bool java_bytecode_language_optionst::assume_inputs_non_null = false |
assume inputs variables to be non-null
Definition at line 223 of file java_bytecode_language.h.
◆ extra_methods
| std::vector<load_extra_methodst> java_bytecode_language_optionst::extra_methods |
Definition at line 252 of file java_bytecode_language.h.
◆ ignore_manifest_main_class
| bool java_bytecode_language_optionst::ignore_manifest_main_class = false |
Definition at line 230 of file java_bytecode_language.h.
◆ java_cp_include_files
| std::string java_bytecode_language_optionst::java_cp_include_files |
Definition at line 243 of file java_bytecode_language.h.
◆ java_load_classes
| 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 242 of file java_bytecode_language.h.
◆ lazy_methods_mode
| lazy_methods_modet java_bytecode_language_optionst::lazy_methods_mode |
Definition at line 238 of file java_bytecode_language.h.
◆ main_jar
| 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 269 of file java_bytecode_language.h.
◆ max_user_array_length
| size_t java_bytecode_language_optionst::max_user_array_length = 0 |
max size for user code created arrays
Definition at line 237 of file java_bytecode_language.h.
◆ method_context
| 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 261 of file java_bytecode_language.h.
◆ no_load_classes
| std::unordered_set<std::string> java_bytecode_language_optionst::no_load_classes |
List of classes to never load.
Definition at line 250 of file java_bytecode_language.h.
◆ nondet_static
| bool java_bytecode_language_optionst::nondet_static = false |
Definition at line 229 of file java_bytecode_language.h.
◆ should_lift_clinit_calls
| 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 266 of file java_bytecode_language.h.
◆ static_values_json
| 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 247 of file java_bytecode_language.h.
◆ string_refinement_enabled
| bool java_bytecode_language_optionst::string_refinement_enabled = false |
Definition at line 224 of file java_bytecode_language.h.
◆ threading_support
| bool java_bytecode_language_optionst::threading_support = false |
Definition at line 228 of file java_bytecode_language.h.
◆ throw_assertion_error
| bool java_bytecode_language_optionst::throw_assertion_error = false |
Definition at line 227 of file java_bytecode_language.h.
◆ throw_runtime_exceptions
| bool java_bytecode_language_optionst::throw_runtime_exceptions = false |
Definition at line 225 of file java_bytecode_language.h.
The documentation for this struct was generated from the following files:
- /home/runner/work/cbmc-documentation/cbmc-documentation/jbmc/src/java_bytecode/java_bytecode_language.h
- /home/runner/work/cbmc-documentation/cbmc-documentation/jbmc/src/java_bytecode/java_bytecode_language.cpp
