From 3173308c6276ee6a5ae6d387fe6953fcdc72f43e Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Fri, 10 Nov 2017 10:28:25 +0100 Subject: [PATCH] adding minimal example witness for a concurrent task. Task: sv-benchmarks/c/pthread/lazy01_false-unreach-call.i Produced by: CPAchecker r26486 with BDD-based analysis (svcomp18). --- lazy01_false-unreach-call.i.graphml | 159 ++++++++++++++++++++++++++++ 1 file changed, 159 insertions(+) create mode 100644 lazy01_false-unreach-call.i.graphml diff --git a/lazy01_false-unreach-call.i.graphml b/lazy01_false-unreach-call.i.graphml new file mode 100644 index 0000000..4a9aa3a --- /dev/null +++ b/lazy01_false-unreach-call.i.graphml @@ -0,0 +1,159 @@ + + + + false + + + false + + + false + + + + + + + + + + + + + + + + + ../sv-benchmarks/c/pthread/lazy01_false-unreach-call.i + + + + + + + + violation_witness + C + CPAchecker 1.6.1-svn + CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) + ../sv-benchmarks/c/pthread/lazy01_false-unreach-call.i + 9f2b31ce9d2cde0ecebdfe4ab1034371aded2ee9 + 32bit + 2017-11-10T11:00:11+01:00 + + true + + + + 0 + 1247 + 1247 + 28393 + 28403 + main + + + + 0 + 1 + 1253 + 1253 + 28467 + 28500 + + + + 1 + 1253 + 1253 + 28467 + 28500 + thread1 + + + true + + + 0 + 2 + 1254 + 1254 + 28505 + 28538 + + + + 1 + thread1 + + + + 0 + 2 + 1254 + 1254 + 28505 + 28538 + + + + 2 + 1254 + 1254 + 28505 + 28538 + thread2 + + + 0 + 3 + 1255 + 1255 + 28543 + 28576 + + + + 2 + thread2 + + + + 0 + 3 + 1255 + 1255 + 28543 + 28576 + + + + 3 + 1255 + 1255 + 28543 + 28576 + thread3 + + + true + __VERIFIER_error(); called in line 1240 + + + 3 + 1239 + 1239 + 28304 + 28312 + condition-true + + + 3 + 1239 + 1239 + 28304 + 28312 + condition-false + + +