From 398968983cceef88f018f5e3edaed0af8775c174 Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Tue, 8 Oct 2019 12:56:40 +0100
Subject: [PATCH] Add unit tests of lazy `cprover_initialize` generation

This tests that an empty bodied initialize function is generated by
`typecheck` and that the body is then populated by `convert_lazy_method`
---
 .../java_bytecode_language/language.cpp       | 48 +++++++++++++++++++
 .../module_dependencies.txt                   |  2 +
 2 files changed, 50 insertions(+)

diff --git a/jbmc/unit/java_bytecode/java_bytecode_language/language.cpp b/jbmc/unit/java_bytecode/java_bytecode_language/language.cpp
index ada4c44010..4a49a81186 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_language/language.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_language/language.cpp
@@ -12,6 +12,9 @@ Author: Diffblue Limited.
 
 #include <java-testing-utils/load_java_class.h>
 #include <java-testing-utils/require_type.h>
+#include <java_bytecode/java_bytecode_language.h>
+#include <linking/static_lifetime_init.h>
+#include <util/options.h>
 
 SCENARIO(
   "java_bytecode_language_opaque_field",
@@ -45,3 +48,48 @@ SCENARIO(
     }
   }
 }
+
+static void use_external_driver(java_bytecode_languaget &language)
+{
+  optionst options;
+  options.set_option("symex-driven-lazy-loading", true);
+  language.set_language_options(options);
+}
+
+TEST_CASE(
+  "LAZY_METHODS_MODE_EXTERNAL_DRIVER based generation of cprover_initialise",
+  "[core][java_bytecode_language]")
+{
+  java_bytecode_languaget language;
+  null_message_handlert null_message_handler;
+  language.set_message_handler(null_message_handler);
+  use_external_driver(language);
+  symbol_tablet symbol_table;
+  language.typecheck(symbol_table, "");
+  {
+    const symbolt *const initialise = symbol_table.lookup(INITIALIZE_FUNCTION);
+    REQUIRE(initialise);
+    REQUIRE(initialise->value.is_nil());
+  }
+  language.convert_lazy_method(INITIALIZE_FUNCTION, symbol_table);
+  {
+    const symbolt *const initialise = symbol_table.lookup(INITIALIZE_FUNCTION);
+    REQUIRE(initialise);
+    REQUIRE(can_cast_expr<codet>(initialise->value));
+  }
+}
+
+TEST_CASE(
+  "Standard generation of cprover_initialise",
+  "[core][java_bytecode_language]")
+{
+  java_bytecode_languaget language;
+  null_message_handlert null_message_handler;
+  language.set_message_handler(null_message_handler);
+  language.set_language_options(optionst{});
+  symbol_tablet symbol_table;
+  language.typecheck(symbol_table, "");
+  const symbolt *const initialise = symbol_table.lookup(INITIALIZE_FUNCTION);
+  REQUIRE(initialise);
+  REQUIRE(can_cast_expr<codet>(initialise->value));
+}
diff --git a/jbmc/unit/java_bytecode/java_bytecode_language/module_dependencies.txt b/jbmc/unit/java_bytecode/java_bytecode_language/module_dependencies.txt
index 0b24c99c48..2275c6ca78 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_language/module_dependencies.txt
+++ b/jbmc/unit/java_bytecode/java_bytecode_language/module_dependencies.txt
@@ -1,3 +1,5 @@
+java_bytecode
 java-testing-utils
+linking
 testing-utils
 util