From 4d4a3ff193ba6fbf527e99a83a9b5bc76710f3cd Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Mon, 11 Apr 2016 16:12:42 +0200
Subject: [PATCH] leon finds data racing counter-example
---
src/main/scala/leon/xlang/IntroduceGlobalStatePhase.scala | 2 +-
testcases/verification/xlang/DataRacing.scala | 8 +++++---
2 files changed, 6 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/xlang/IntroduceGlobalStatePhase.scala b/src/main/scala/leon/xlang/IntroduceGlobalStatePhase.scala
index bf91ff246..28e385a9a 100644
--- a/src/main/scala/leon/xlang/IntroduceGlobalStatePhase.scala
+++ b/src/main/scala/leon/xlang/IntroduceGlobalStatePhase.scala
@@ -54,7 +54,7 @@ object IntroduceGlobalStatePhase extends TransformationPhase {
}
private def extendFunDefWithState(fd: FunDef, stateCCD: CaseClassDef)(ctx: LeonContext): FunDef = {
- val newParams = fd.params :+ ValDef(FreshIdentifier("state", stateCCD.typed))
+ val newParams = fd.params :+ ValDef(FreshIdentifier("globalState", stateCCD.typed))
val newFunDef = new FunDef(fd.id.freshen, fd.tparams, newParams, fd.returnType)
newFunDef.addFlags(fd.flags)
newFunDef.setPos(fd)
diff --git a/testcases/verification/xlang/DataRacing.scala b/testcases/verification/xlang/DataRacing.scala
index 2d094a1d5..f57640061 100644
--- a/testcases/verification/xlang/DataRacing.scala
+++ b/testcases/verification/xlang/DataRacing.scala
@@ -34,12 +34,14 @@ object DataRacing {
case (RunnableNil(), RunnableNil()) => ()
}
- def main(): Unit = {
+ //z3 finds counterexample in 0.5
+ //cvc4 needs 130 seconds
+ def main(): Int = {
val state = SharedState(0)
val t1 = RunnableCons((s: SharedState) => s.i = s.i + 1, RunnableNil())
val t2 = RunnableCons((s: SharedState) => s.i = s.i * 2, RunnableNil())
execute(t1, t2, state)
- assert(state.i == 2)
- }
+ state.i
+ } ensuring(_ == 2)
}
--
GitLab