The cprover-sv-comp's discuss from diffblue

Value mismatch between CBMC's console log and GraphML witness

CBMC prints the values for __VERIFIER_nondet in both its console logs and GraphML witnesses when an error path is found.
However, sometimes these values do not match.

Here is an example.

Program: cambridge.2.prop1-back-serstep.c
Property: unreach-call.prp
CBMC version: 5.70.0-121-g4f69955d00 (binaries and wrapper script downloaded from tool archive of SV-COMP 2023)

Command line:

./cbmc --graphml-witness witness.graphml --propertyfile unreach-call.prp --64 cambridge.2.prop1-back-serstep.c > exe.log

The input and output files are also available here: example.zip

The values for input_149 = __VERIFIER_nondet_ushort() at line 181 of the program in exe.log and witness.graphml mismatch, as shown by

$ grep "input_149=" exe.log 
  input_149=0 (00000000 00000000)
  input_149=0 (00000000 00000000)
  input_149=0 (00000000 00000000)
  input_149=0 (00000000 00000000)
  input_149=0 (00000000 00000000)
  input_149=0 (00000000 00000000)
  input_149=0 (00000000 00000000)
  input_149=0 (00000000 00000000)
  input_149=65535 (11111111 11111111)
  input_149=65535 (11111111 11111111)
  input_149=65535 (11111111 11111111)

$ grep -A 2 '<data key="startline">181</data>' witness.graphml 
      <data key="startline">181</data>
      <data key="threadId">0</data>
      <data key="assumption">\result = 0;</data>
--
      <data key="startline">181</data>
      <data key="threadId">0</data>
      <data key="assumption">\result = 0;</data>
--
      <data key="startline">181</data>
      <data key="threadId">0</data>
      <data key="assumption">\result = 0;</data>
--
      <data key="startline">181</data>
      <data key="threadId">0</data>
      <data key="assumption">\result = 0;</data>
--
      <data key="startline">181</data>
      <data key="threadId">0</data>
      <data key="assumption">\result = 0;</data>
--
      <data key="startline">181</data>
      <data key="threadId">0</data>
      <data key="assumption">\result = 0;</data>
--
      <data key="startline">181</data>
      <data key="threadId">0</data>
      <data key="assumption">\result = 0;</data>
--
      <data key="startline">181</data>
      <data key="threadId">0</data>
      <data key="assumption">\result = 0;</data>
--
      <data key="startline">181</data>
      <data key="threadId">0</data>
      <data key="assumption">\result = 0;</data>
--
      <data key="startline">181</data>
      <data key="threadId">0</data>
      <data key="assumption">\result = 0;</data>
--
      <data key="startline">181</data>
      <data key="threadId">0</data>
      <data key="assumption">\result = 0;</data>

Both files contain 11 occurrences of input_149.
However, the values are different in the last 3 loop iterations (65535 vs. 0).

diffblue / cprover-sv-comp Goto Github PK

cprover-sv-comp's Issues

Value mismatch between CBMC's console log and GraphML witness

Recommend Projects

React

Vue.js

Typescript

TensorFlow

Django

Laravel

D3

Recommend Topics

javascript

web

server

Machine learning

Visualization

Game

Recommend Org

Facebook

Microsoft

Google

Alibaba

D3

Tencent