basic blocks are covered even when later assumes in that block are unsatisfiable

[mgudemann]

in the following goto program, the block 2 is considered covered, although the supplied array might contain nothing but null, which contradicts the later assume.

inner_class_array.f() /* java::inner_class_array.f:([Linner_class_array$A;)I */
        // 9 file inner_class_array.java line 6 function java::inner_class_array.f:([Linner_class_array$A;)I bytecode_index 2
        // Labels: pc0
        ASSERT false // function java::inner_class_array.f:([Linner_class_array$A;)I block 1
        // 10 file inner_class_array.java line 6 function java::inner_class_array.f:([Linner_class_array$A;)I
        ASSUME !(arg1a == null) // reference is null in *arg1a
        // 11 file inner_class_array.java line 6 function java::inner_class_array.f:([Linner_class_array$A;)I bytecode_index 2
        IF arg1a->length <= 0 THEN GOTO 1
        // 12 file inner_class_array.java line 7 function java::inner_class_array.f:([Linner_class_array$A;)I bytecode_index 5
        ASSERT false // function java::inner_class_array.f:([Linner_class_array$A;)I block 2
        // 13 no location
        // Labels: pc5
        int anonlocal::2i;
        // 14 file inner_class_array.java line 7 function java::inner_class_array.f:([Linner_class_array$A;)I bytecode_index 5
        ASSUME 0 >= 0 // Array index < 0
        // 15 file inner_class_array.java line 7 function java::inner_class_array.f:([Linner_class_array$A;)I bytecode_index 5
        ASSUME 0 < ((struct java::array[reference] *)(void *)arg1a)->length // Array index >= length
        // 16 file inner_class_array.java line 7 function java::inner_class_array.f:([Linner_class_array$A;)I
        ASSUME !(arg1a->data == null) // reference is null in arg1a->data[0]
        // 17 file inner_class_array.java line 7 function java::inner_class_array.f:([Linner_class_array$A;)I
        ASSUME !(*arg1a->data == null) // reference is null in *((struct inner_class_array$A *)arg1a->data[0])
        // 18 file inner_class_array.java line 7 function java::inner_class_array.f:([Linner_class_array$A;)I bytecode_index 7
        anonlocal::2i = ((struct inner_class_array$A *)arg1a->data[0])->x;
        // 19 file inner_class_array.java line 8 function java::inner_class_array.f:([Linner_class_array$A;)I bytecode_index 9
        inner_class_array.f:([Linner_class_array$A;)I#return_value = anonlocal::2i;
        // 20 file inner_class_array.java line 8 function java::inner_class_array.f:([Linner_class_array$A;)I bytecode_index 9
        dead anonlocal::2i;
        // 21 file inner_class_array.java line 8 function java::inner_class_array.f:([Linner_class_array$A;)I bytecode_index 9
        GOTO 2
        // 22 file inner_class_array.java line 10 function java::inner_class_array.f:([Linner_class_array$A;)I bytecode_index 11
        // Labels: pc14
     1: ASSERT false // function java::inner_class_array.f:([Linner_class_array$A;)I block 3
        // 23 file inner_class_array.java line 10 function java::inner_class_array.f:([Linner_class_array$A;)I bytecode_index 11
        inner_class_array.f:([Linner_class_array$A;)I#return_value = 0;
        // 24 no location
     2: END_FUNCTION
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

There are at least two possibilites to fix this

1. revert 5c30907 which removed ASSUME from the coverage targets
2. add the ASSERT false at the end of the basic block instead of the beginning; as the understanding of basic block means that if any instruction is executed, then all others are, too, this does not necessarily hold for ASSUME

[peterschrammel]

3. consider all assumes for coverage goals, not only those that occur 'before' the goal

[peterschrammel]

Summary of discussion with @mgudemann:

1. would be a partial quick fix to make some cases work
2. would be better because it reduces the number of goals being instrumented, but is still partial
3. is required for cases such as:

   IF a GOTO 1:
   ASSUME b
   ...
   ASSERT FALSE // 1
   GOTO 2
1: ASSERT FALSE // 2
2: ASSUME c
   ASSERT FALSE // 3

where we could get tests covering (1) and (2, 3) respectively. However, (1) need not satisfy c and would therefore be an invalid test

[tautschnig]

Was fixed in #7810.