#include <java_bytecode_language.h>
Collaboration diagram for java_bytecode_language_optionst:Public Member Functions | |
| java_bytecode_language_optionst (const optionst &options, message_handlert &) | |
| 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 |
| std::optional< 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 |
| std::optional< 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... | |
| std::optional< std::string > | main_jar |
| If set then a JAR file has been given via the -jar option. More... | |
Detailed Description
Definition at line 201 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, |
| message_handlert & | message_handler | ||
| ) |
Definition at line 140 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 219 of file java_bytecode_language.h.
◆ assert_uncaught_exceptions
| bool java_bytecode_language_optionst::assert_uncaught_exceptions = false |
Definition at line 211 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 208 of file java_bytecode_language.h.
◆ extra_methods
| std::vector<load_extra_methodst> java_bytecode_language_optionst::extra_methods |
Definition at line 237 of file java_bytecode_language.h.
◆ ignore_manifest_main_class
| bool java_bytecode_language_optionst::ignore_manifest_main_class = false |
Definition at line 215 of file java_bytecode_language.h.
◆ java_cp_include_files
| std::string java_bytecode_language_optionst::java_cp_include_files |
Definition at line 228 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 227 of file java_bytecode_language.h.
◆ lazy_methods_mode
| lazy_methods_modet java_bytecode_language_optionst::lazy_methods_mode |
Definition at line 223 of file java_bytecode_language.h.
◆ main_jar
| std::optional<std::string> java_bytecode_language_optionst::main_jar |
If set then a JAR file has been given via the -jar option.
Definition at line 254 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 222 of file java_bytecode_language.h.
◆ method_context
| std::optional<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 246 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 235 of file java_bytecode_language.h.
◆ nondet_static
| bool java_bytecode_language_optionst::nondet_static = false |
Definition at line 214 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 251 of file java_bytecode_language.h.
◆ static_values_json
| std::optional<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 232 of file java_bytecode_language.h.
◆ string_refinement_enabled
| bool java_bytecode_language_optionst::string_refinement_enabled = false |
Definition at line 209 of file java_bytecode_language.h.
◆ threading_support
| bool java_bytecode_language_optionst::threading_support = false |
Definition at line 213 of file java_bytecode_language.h.
◆ throw_assertion_error
| bool java_bytecode_language_optionst::throw_assertion_error = false |
Definition at line 212 of file java_bytecode_language.h.
◆ throw_runtime_exceptions
| bool java_bytecode_language_optionst::throw_runtime_exceptions = false |
Definition at line 210 of file java_bytecode_language.h.
The documentation for this struct was generated from the following files:
- /home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/java_bytecode_language.h
- /home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/java_bytecode_language.cpp
