public class My {

public static int s_non_init;

public static int s_init = 1;

public static int s_static_init;

static { s_static_init = 2; }

public static final int sf_init = 1;

public static final int sf_static_init;

static { sf_static_init = 2; }

public int field;

public My(int i) {

String s = "bla";

field = i;

if (s_non_init != 0)

field = 108; // this line can only be covered with nondet-static

if (s_init != 1)

field = 108; // this line can only be covered with nondet-static

if (s_static_init != 2)

field = 108; // this line can only be covered with nondet-static

if (sf_init != 1)

field = 108; // this line cannot be covered even with nondet-static

if (sf_static_init != 2)

field = 108; // this line cannot be covered even with nondet-static

if (s != "bla")

field = 108; // this line cannot be covered even with nondet-static

}

}

CORE symex-driven-lazy-loading-expected-failure

My.class

--function "My.<init>" --cover location --nondet-static

^EXIT=0$

^SIGNAL=0$

file My\.java line 18 function java::My\.\<init\>:\(I\)V.*SATISFIED$

file My\.java line 19 function java::My\.\<init\>:\(I\)V.*SATISFIED$

file My\.java line 20 function java::My\.\<init\>:\(I\)V.*SATISFIED$

file My\.java line 25 function java::My\.\<init\>:\(I\)V.*FAILED$

file My\.java line 27 function java::My\.\<init\>:\(I\)V.*FAILED$

--

file My\.java line 23 function java::My\.\<init\>:\(I\)V.*SATISFIED$

--

This tests nondet-static option, namely that static (non-final) variables are

non-det initialized regardless of whether they are given a (static) initializer

or not but constants such as strings are not non-det initialized

This fails under symex-driven lazy loading because nondet-static cannot be used

with it