diffblue / cprover-sv-comp Goto Github PK

View Code? Open in Web Editor NEW

2.0 8.0 11.0 110 KB

CPROVER wrappers and configuration for the Software Verification Competition (SV-COMP)

Makefile 16.54% Shell 11.88% C++ 71.58%

cprover-sv-comp's Introduction

CPROVER SV-COMP Wrappers and Configuration

Build package

make

Build wrapper script

If you you want to build the wrapper script only, use

make tool-wrapper

where tool is cbmc, jbmc or 2ls.

Benchexec tool script

Benchexec benchmark definition

License

https://github.com/diffblue/cbmc/blob/master/LICENSE

Running experiments in SV-COMP style

git clone --depth=1 https://github.com/sosy-lab/sv-benchmarks
git clone https://github.com/sosy-lab/benchexec
cd benchexec
tar xzf ../2ls-sv-comp-2017.tar.gz
wget https://raw.githubusercontent.com/sosy-lab/sv-comp/master/benchmark-defs/2ls.xml
sed -i 's/witness.graphml/${logfile_path_abs}${inputfile_name}-witness.graphml/' 2ls.xml
bin/benchexec 2ls.xml --tasks <those categories that you want to run>
wget https://raw.githubusercontent.com/sosy-lab/sv-comp/master/benchmark-defs/cpa-seq-validate-correctness-witnesses.xml
wget https://raw.githubusercontent.com/sosy-lab/sv-comp/master/benchmark-defs/cpa-seq-validate-violation-witnesses.xml
git clone --depth=1 https://github.com/sosy-lab/cpachecker.git
cd cpachecker
ant
cd ..
ln -s cpachecker/scripts/cpa.sh cpa.sh
ln -s cpachecker/config/ config
# manually tweak the requiredfiles and option name=-witness lines in cpa-seq-validate*.xml
bin/benchexec cpa-seq-validate-correctness-witnesses.xml
PYTHONPATH=. python3 contrib/mergeBenchmarkSets.py #needs more parameters
bin/table-generator results/*xml.bz2

Replace 2ls by cbmc to use the above with CBMC.

Collecting profiling data

bin/benchexec cbmc.xml --tasks <those categories that you want to run> -T 120s
gprof --sum ./cbmc-binary *.gmon.out.*
gprof ./cbmc-profiling gmon.sum > sum.profile
rm gmon.out *.gmon.out.*

cprover-sv-comp's People

Contributors

Stargazers

Watchers

Forkers

tautschnig peterschrammel steffan711 marek-trtik lucasccordeiro zhixing-xu viktormalik clayne frnecas

cprover-sv-comp's Issues

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 Introduction

CPROVER SV-COMP Wrappers and Configuration

Build package

Build wrapper script

Benchexec tool script

Benchexec benchmark definition

License

Running experiments in SV-COMP style

Collecting profiling data

cprover-sv-comp's People

Contributors

Stargazers

Watchers

Forkers

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