Multi-path checker for Java requires preprocessing

Author: peterschrammel

jbmc/src/java_bytecode/Makefile

@@ -25,6 +25,7 @@ SRC = bytecode_info.cpp \
       java_enum_static_init_unwind_handler.cpp \
       java_entry_point.cpp \
       java_local_variable_table.cpp \
+      java_multi_path_symex_checker.cpp \
       java_multi_path_symex_only_checker.cpp \
       java_object_factory.cpp \
       java_object_factory_parameters.cpp \

jbmc/src/java_bytecode/java_multi_path_symex_checker.cpp

@@ -0,0 +1,40 @@
+/*******************************************************************\
+
+Module: Goto Checker using Bounded Model Checking for Java
+
+Author: Daniel Kroening, Peter Schrammel
+
+ \*******************************************************************/
+
+/// \file
+/// Goto Checker using Bounded Model Checking for Java
+
+#include "java_multi_path_symex_checker.h"
+
+#include <java_bytecode/java_enum_static_init_unwind_handler.h>
+
+java_multi_path_symex_checkert::java_multi_path_symex_checkert(
+  const optionst &options,
+  ui_message_handlert &ui_message_handler,
+  abstract_goto_modelt &goto_model)
+  : multi_path_symex_checkert(options, ui_message_handler, goto_model)
+{
+  // unwinds <clinit> loops to number of enum elements
+  if(options.get_bool_option("java-unwind-enum-static"))
+  {
+    // clang-format off
+    // (it asks for the body to be at the same indent level as the parameters
+    //  for some reason)
+    symex.add_loop_unwind_handler(
+      [&goto_model](
+        const goto_symex_statet::call_stackt &context,
+        unsigned loop_num,
+        unsigned unwind,
+        unsigned &max_unwind)
+      { // NOLINT (*)
+        return java_enum_static_init_unwind_handler(
+          context, loop_num, unwind, max_unwind, goto_model.get_symbol_table());
+      });
+    // clang-format on
+  }
+}

jbmc/src/java_bytecode/java_multi_path_symex_checker.h

@@ -0,0 +1,26 @@
+/*******************************************************************\
+
+Module: Goto Checker using Bounded Model Checking for Java
+
+Author: Daniel Kroening, Peter Schrammel
+
+ \*******************************************************************/
+
+/// \file
+/// Goto Checker using Bounded Model Checking for Java
+
+#ifndef CPROVER_JAVA_BYTECODE_JAVA_MULTI_PATH_SYMEX_CHECKER_H
+#define CPROVER_JAVA_BYTECODE_JAVA_MULTI_PATH_SYMEX_CHECKER_H
+
+#include <goto-checker/multi_path_symex_checker.h>
+
+class java_multi_path_symex_checkert : public multi_path_symex_checkert
+{
+public:
+  java_multi_path_symex_checkert(
+    const optionst &options,
+    ui_message_handlert &ui_message_handler,
+    abstract_goto_modelt &goto_model);
+};
+
+#endif // CPROVER_JAVA_BYTECODE_JAVA_MULTI_PATH_SYMEX_CHECKER_H