Merge pull request #503 from mgudemann/fix_remove_static_init_non_java_functions

ignore non-Java files in enum static init unwind

Author: kroening

regression/cbmc-java/enum1/enum1.class

@@ -0,0 +1,16 @@
+public enum enum1
+{
+  VAL1, VAL2, VAL3, VAL4, VAL5;
+  static
+  {
+    for(enum1 e : enum1.values())
+    {
+      System.out.println(e);
+    }
+  }
+  public static void main(String[] args)
+  {
+    enum1 e=VAL5;
+    assert(e==VAL5);
+  }
+}

regression/cbmc-java/enum1/enum1.java

@@ -0,0 +1,8 @@
+CORE
+enum1.class
+--java-unwind-enum-static --unwind 3
+^EXIT=10$
+^SIGNAL=0$
+^Unwinding loop java::enum1.<clinit>:()V.0 iteration 5 (6 max) file enum1.java line 6 function java::enum1.<clinit>:()V bytecode_index 78 thread 0$
+--
+^warning: ignoring

regression/cbmc-java/enum1/test.desc

@@ -550,6 +550,8 @@ int cbmc_parse_optionst::doit()
   if(set_properties(goto_functions))
     return 7; // should contemplate EX_USAGE from sysexits.h
 
+  // unwinds <clinit> loops to number of enum elements
+  // side effect: add this as explicit unwind to unwind set
   if(options.get_bool_option("java-unwind-enum-static"))
     remove_static_init_loops(symbol_table, goto_functions, options);
 

src/cbmc/cbmc_parse_options.cpp

@@ -7,6 +7,7 @@ Author: Daniel Kroening, kroening@kroening.com
 \*******************************************************************/
 
 #include <util/message.h>
+#include <util/suffix.h>
 #include <util/string2int.h>
 
 #include "remove_static_init_loops.h"
@@ -56,6 +57,10 @@ void remove_static_init_loopst::unwind_enum_static(
         const std::string java_clinit="<clinit>:()V";
         const std::string &fname=id2string(ins.function);
         size_t class_prefix_length=fname.find_last_of('.');
+        // is Java function and static init?
+        const symbolt &function_name=symbol_table.lookup(ins.function);
+        if(!(function_name.mode==ID_java && has_suffix(fname, java_clinit)))
+          continue;
         assert(
           class_prefix_length!=std::string::npos &&
           "could not identify class name");
@@ -65,23 +70,16 @@ void remove_static_init_loopst::unwind_enum_static(
         size_t unwinds=class_type.get_size_t(ID_java_enum_static_unwind);
 
         unwind_max=std::max(unwind_max, unwinds);
-        if(fname.length()>java_clinit.length())
+        if(unwinds>0)
         {
-          // extend unwindset with unwinds for <clinit> of enum
-          if(fname.compare(
-            fname.length()-java_clinit.length(),
-            java_clinit.length(),
-            java_clinit)==0 && unwinds>0)
-          {
-            const std::string &set=options.get_option("unwindset");
-            std::string newset;
-            if(set!="")
-              newset=",";
-            newset+=
-              id2string(ins.function)+"."+std::to_string(loop_id)+":"+
-              std::to_string(unwinds);
-            options.set_option("unwindset", set+newset);
-          }
+          const std::string &set=options.get_option("unwindset");
+          std::string newset;
+          if(set!="")
+            newset=",";
+          newset+=
+            id2string(ins.function)+"."+std::to_string(loop_id)+":"+
+            std::to_string(unwinds);
+          options.set_option("unwindset", set+newset);
         }
       }
     }