Merge pull request #4893 from svorenova/not-null-annotation-check-location

Correct the source location of methods and not null annotation checks [TG-8270]

Author: svorenova

jbmc/regression/jbmc/parameter-annotation-not-null/MainKotlin.class

@@ -0,0 +1,2 @@
+abstract class MainKotlin(val scope: String, val kind: String) {
+}

jbmc/regression/jbmc/parameter-annotation-not-null/MainKotlin.kt

@@ -4,7 +4,7 @@ Main.class
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-\[not-null-annotation-check\.1\] line \d+ Not null annotation check: FAILURE
-\[not-null-annotation-check\.2\] line \d+ Not null annotation check: SUCCESS
+\[java::Main\.bar:\(Ljava/lang/Integer;ZLjava/lang/Object;\[Ljava/lang/String;\)Ljava/lang/Integer;\.not-null-annotation-check\.1\] line \d+ Not null annotation check: FAILURE
+\[java::Main\.bar:\(Ljava/lang/Integer;ZLjava/lang/Object;\[Ljava/lang/String;\)Ljava/lang/Integer;\.not-null-annotation-check\.2\] line \d+ Not null annotation check: SUCCESS
 --
 ^warning: ignoring

jbmc/regression/jbmc/parameter-annotation-not-null/test_array.desc

@@ -0,0 +1,12 @@
+CORE
+MainKotlin.class
+--function "MainKotlin.<init>" --show-properties
+^EXIT=0$
+^SIGNAL=0$
+Property java::MainKotlin.<init>:\(Ljava/lang/String;Ljava/lang/String;\)V.not-null-annotation-check.1:
+Property java::MainKotlin.<init>:\(Ljava/lang/String;Ljava/lang/String;\)V.not-null-annotation-check.2:
+file MainKotlin.kt line 1 function java::MainKotlin.<init>:\(Ljava/lang/String;Ljava/lang/String;\)V$
+--
+--
+Test that the not-null-annotation-check property name is correctly prefixed with
+the method name and has line number assigned

jbmc/regression/jbmc/parameter-annotation-not-null/test_kotlin.desc

@@ -4,7 +4,7 @@ Main.class
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-\[not-null-annotation-check\.1\] line \d+ Not null annotation check: SUCCESS
-\[not-null-annotation-check\.2\] line \d+ Not null annotation check: FAILURE
+\[java::Main\.foo:\(Ljava/lang/Integer;ZLjava/lang/Object;\[Ljava/lang/String;\)Ljava/lang/Integer;\.not-null-annotation-check\.1\] line \d+ Not null annotation check: SUCCESS
+\[java::Main\.foo:\(Ljava/lang/Integer;ZLjava/lang/Object;\[Ljava/lang/String;\)Ljava/lang/Integer;\.not-null-annotation-check\.2\] line \d+ Not null annotation check: FAILURE
 --
 ^warning: ignoring

jbmc/regression/jbmc/parameter-annotation-not-null/test_object.desc

@@ -4,7 +4,7 @@ Main.class
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-\[not-null-annotation-check\.1\] line \d+ Not null annotation check: SUCCESS
-\[not-null-annotation-check\.2\] line \d+ Not null annotation check: SUCCESS
+\[java::Main\.foo:\(Ljava/lang/Integer;ZLjava/lang/Object;\[Ljava/lang/String;\)Ljava/lang/Integer;\.not-null-annotation-check\.1\] line \d+ Not null annotation check: SUCCESS
+\[java::Main\.foo:\(Ljava/lang/Integer;ZLjava/lang/Object;\[Ljava/lang/String;\)Ljava/lang/Integer;\.not-null-annotation-check\.2\] line \d+ Not null annotation check: SUCCESS
 --
 ^warning: ignoring

jbmc/regression/jbmc/parameter-annotation-not-null/test_success.desc

@@ -1238,6 +1238,11 @@ void java_bytecode_parsert::rmethod_attribute(methodt &method)
     for(std::size_t j=0; j<attributes_count; j++)
       rcode_attribute(method);
 
+    // method name
+    method.source_location.set_function(
+      "java::" + id2string(parse_tree.parsed_class.name) + "." +
+      id2string(method.name) + ":" + method.descriptor);
+
     irep_idt line_number;
 
     // add missing line numbers
@@ -1250,16 +1255,18 @@ void java_bytecode_parsert::rmethod_attribute(methodt &method)
         line_number=it->source_location.get_line();
       else if(!line_number.empty())
         it->source_location.set_line(line_number);
-      it->source_location
-        .set_function(
-          "java::"+id2string(parse_tree.parsed_class.name)+"."+
-          id2string(method.name)+":"+method.descriptor);
+      it->source_location.set_function(method.source_location.get_function());
     }
 
-    // line number of method
-    if(!method.instructions.empty())
-      method.source_location.set_line(
-        method.instructions.begin()->source_location.get_line());
+    // line number of method (the first line number available)
+    const auto it = std::find_if(
+      method.instructions.begin(),
+      method.instructions.end(),
+      [&](const instructiont &instruction) {
+        return !instruction.source_location.get_line().empty();
+      });
+    if(it != method.instructions.end())
+      method.source_location.set_line(it->source_location.get_line());
   }
   else if(attribute_name=="Signature")
   {