Add unit test for non-instrumentation of Java virtual calls

Author: Matthias Güdemann

src/goto-instrument/Makefile

@@ -94,12 +94,12 @@ INCLUDES= -I ..
 
 LIBS =
 
-CLEANFILES = goto-instrument$(EXEEXT)
+CLEANFILES = goto-instrument$(EXEEXT) goto-instrument$(LIBEXT)
 
 include ../config.inc
 include ../common
 
-all: goto-instrument$(EXEEXT)
+all: goto-instrument$(EXEEXT) goto-instrument$(LIBEXT)
 
 ifneq ($(LIB_GLPK),)
   LIBS += $(LIB_GLPK)
@@ -111,6 +111,9 @@ endif
 goto-instrument$(EXEEXT): $(OBJ)
 	$(LINKBIN)
 
+goto-instrument$(LIBEXT): $(OBJ)
+	$(LINKLIB)
+
 .PHONY: goto-instrument-mac-signed
 
 goto-instrument-mac-signed: goto-instrument$(EXEEXT)

unit/CMakeLists.txt

@@ -36,7 +36,15 @@ target_include_directories(unit
     ${CBMC_SOURCE_DIR}
     ${CMAKE_CURRENT_SOURCE_DIR}
 )
-target_link_libraries(unit testing-utils ansi-c solvers java_bytecode)
+target_link_libraries(
+ unit
+ testing-utils
+ ansi-c
+ solvers
+ java_bytecode
+ goto-programs
+ goto-instrument-lib)
+
 add_test(
     NAME unit
     COMMAND $<TARGET_FILE:unit>

unit/Makefile

@@ -66,6 +66,7 @@ CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \
               ../src/util/util$(LIBEXT) \
               ../src/big-int/big-int$(LIBEXT) \
               ../src/goto-programs/goto-programs$(LIBEXT) \
+              ../src/goto-instrument/goto-instrument$(LIBEXT) \
               ../src/pointer-analysis/pointer-analysis$(LIBEXT) \
               ../src/langapi/langapi$(LIBEXT) \
               ../src/assembler/assembler$(LIBEXT) \

unit/java_bytecode/java_virtual_functions/virtual_functions.cpp

@@ -13,7 +13,8 @@
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/remove_virtual_functions.h>
 #include <util/config.h>
-
+#include <goto-instrument/cover.h>
+#include <util/options.h>
 #include <util/std_expr.h>
 
 void check_function_call(
@@ -113,8 +114,54 @@ SCENARIO(
           }
         }
       }
-
       REQUIRE(found_function);
+
+      WHEN("basic blocks are instrumented")
+      {
+        optionst options;
+        options.set_option("cover", "location");
+        THEN("instrumentation assertions are inserted")
+        {
+          REQUIRE_FALSE(
+            instrument_cover_goals(
+              options, new_table, new_goto_functions, null_output));
+        }
+        THEN(
+          "instructions are marked as originating from virtual function call "
+          "removal")
+        {
+          auto function = new_goto_functions.function_map.find(function_name);
+          REQUIRE(function != new_goto_functions.function_map.end());
+
+          const goto_programt &goto_program = function->second.body;
+          auto it = std::find_if(
+            goto_program.instructions.begin(),
+            goto_program.instructions.end(),
+            [](const goto_programt::instructiont &instruction) {
+              return instruction.type == goto_program_instruction_typet::GOTO &&
+                     instruction.guard.id() == ID_equal;
+            });
+          REQUIRE(it != goto_program.instructions.end());
+          THEN(
+            "all instructions that share the same bytecode index "
+            "are marked as originating from a removed virtual function "
+            "call and there is no GOTO ASSERT")
+          {
+            const source_locationt &loc = it->source_location;
+            REQUIRE(loc != source_locationt::nil());
+            REQUIRE(!loc.get_java_bytecode_index().empty());
+
+            while(it->source_location != source_locationt::nil() &&
+                  it->source_location.get_java_bytecode_index() ==
+                    loc.get_java_bytecode_index())
+            {
+              REQUIRE(it->source_location.get_java_removed_virtual_call());
+              REQUIRE(it->type != goto_program_instruction_typet::ASSERT);
+              ++it;
+            }
+          }
+        }
+      }
     }
   }
 }