diff --git a/regression/cbmc-java/enum1/enum1.class b/regression/cbmc-java/enum1/enum1.class new file mode 100644 index 00000000000..25433918f32 Binary files /dev/null and b/regression/cbmc-java/enum1/enum1.class differ diff --git a/regression/cbmc-java/enum1/enum1.java b/regression/cbmc-java/enum1/enum1.java new file mode 100644 index 00000000000..40838ccdc0d --- /dev/null +++ b/regression/cbmc-java/enum1/enum1.java @@ -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); + } +} diff --git a/regression/cbmc-java/enum1/test.desc b/regression/cbmc-java/enum1/test.desc new file mode 100644 index 00000000000..8a395386017 --- /dev/null +++ b/regression/cbmc-java/enum1/test.desc @@ -0,0 +1,8 @@ +CORE +enum1.class +--java-unwind-enum-static --unwind 3 +^EXIT=10$ +^SIGNAL=0$ +^Unwinding loop java::enum1.:()V.0 iteration 5 (6 max) file enum1.java line 6 function java::enum1.:()V bytecode_index 78 thread 0$ +-- +^warning: ignoring diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index d09b544c678..4d839835824 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -550,6 +550,8 @@ int cbmc_parse_optionst::doit() if(set_properties(goto_functions)) return 7; // should contemplate EX_USAGE from sysexits.h + // unwinds 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); diff --git a/src/goto-programs/remove_static_init_loops.cpp b/src/goto-programs/remove_static_init_loops.cpp index 25d48ccf654..f1084d6ca53 100644 --- a/src/goto-programs/remove_static_init_loops.cpp +++ b/src/goto-programs/remove_static_init_loops.cpp @@ -7,6 +7,7 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ #include +#include #include #include "remove_static_init_loops.h" @@ -56,6 +57,10 @@ void remove_static_init_loopst::unwind_enum_static( const std::string java_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 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); } } }