Overflow witness contains no assignment

[fbrausse]

For the SV-COMP task c/Juliet_Test/CWE190_Integer_Overflow__int64_t_fscanf_add_08_bad.i ESBMC finds an integer overflow but the counter-example and witness file do not contain assignments to the variable data in question. This is the part where the overflow happens in the source file:

void CWE190_Integer_Overflow__int64_t_fscanf_add_08_bad()
{
    int64_t data;
    data = 0LL;
    if(staticReturnsTrue())
    {
        fscanf (stdin, "%" "l" "d", &data);
    }
    if(staticReturnsTrue())
    {
        {
            int64_t result = data + 1; // overflow here
            printLongLongLine(result);
        }
    }
}

The counter-example is

[Counterexample]

State 4 file CWE190_Integer_Overflow__int64_t_fscanf_add_08_bad.i line 1568 column 13 function CWE190_Integer_Overflow__int64_t_fscanf_add_08_bad thread 0
----------------------------------------------------
Violated property:
  file CWE190_Integer_Overflow__int64_t_fscanf_add_08_bad.i line 1568 column 13 function CWE190_Integer_Overflow__int64_t_fscanf_add_08_bad
  arithmetic overflow on add
  !overflow("+", data, 1)

Consequently, the witness file only contains

    <node id="N0">
      <data key="entry">true</data>
    </node>
    <node id="N1"/>
    <edge id="E0" source="N0" target="N1">
      <data key="enterFunction">main</data>
      <data key="createThread">0</data>
    </edge>
    <node id="N2">
      <data key="violation">true</data>
    </node>
    <edge id="E1" source="N1" target="N2">
      <data key="startline">1568</data>
      <data key="threadId">0</data>
    </edge>

Neither UAutomizer nor CPAchecker find the overflow using this witness. With a --no-slice witness at least UAutomizer is able to validate the result.

[lucasccordeiro]

Shall we have a run with the option --no-slice enabled?

[lucasccordeiro]

Or --compact-trace.

[fbrausse]

With a --no-slice witness at least UAutomizer is able to validate the result.

CPAchecker still doesn't want to find the violation.

Or --compact-trace.

Good idea, I'll try.