Changes between Initial Version and Version 1 of Ticket #7, comment 5


Ignore:
Timestamp:
10/27/2018 06:23:48 PM (6 years ago)
Author:
Vladimír Štill
Comment:

Legend:

Unmodified
Added
Removed
Modified

  • Ticket #7, comment 5

    initial v1  
    119. `divine check --svcomp --symbolic ~/repo/sv-benchmarks/c/array-memsafety/bubblesort-alloca_true-valid-memsafety_true-termination.c`
    22
    3 There is a spurious memory error, probably due to the fact that SYM transformation fails to detect that it is sending symbolic value to `alloca`, which results in alloca allocating based on the current explicit value in the variable (which is 0, resulting in allocation size 1). I suggest this problem is for now resolved by an `UNREACHABLE` in SYM transformation
     3There is a spurious memory error, probably due to the fact that SYM transformation fails to detect that it is sending symbolic value to `alloca`, which results in alloca allocating based on the current explicit value in the variable (which is 0, resulting in allocation size 1). I suggest this problem is for now resolved by an `UNREACHABLE` in SYM transformation.