From 2485477f4e91cba7fe6e0c137817d62f513a3c42 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Tue, 26 May 2015 14:42:16 +0200
Subject: [PATCH] xlang correctly handles short circuit with side effects
---
.../xlang/ImperativeCodeElimination.scala | 10 ++++++++++
.../xlang/valid/ShortCircuit.scala | 19 +++++++++++++++++++
2 files changed, 29 insertions(+)
create mode 100644 src/test/resources/regression/verification/xlang/valid/ShortCircuit.scala
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 9d000489f..8f26df8f4 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -252,6 +252,16 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
}
(i, scope, Map())
+ case And(args) => {
+ val ifExpr = args.reduceRight((el, acc) => IfExpr(el, acc, BooleanLiteral(false)))
+ toFunction(ifExpr)
+ }
+
+ case Or(args) => {
+ val ifExpr = args.reduceRight((el, acc) => IfExpr(el, BooleanLiteral(true), acc))
+ toFunction(ifExpr)
+ }
+
case n @ NAryOperator(Seq(), recons) => (n, (body: Expr) => body, Map())
case n @ NAryOperator(args, recons) => {
val (recArgs, scope, fun) = args.foldRight((Seq[Expr](), (body: Expr) => body, Map[Identifier, Identifier]()))((arg, acc) => {
diff --git a/src/test/resources/regression/verification/xlang/valid/ShortCircuit.scala b/src/test/resources/regression/verification/xlang/valid/ShortCircuit.scala
new file mode 100644
index 000000000..a35daf11a
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ShortCircuit.scala
@@ -0,0 +1,19 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+object ShortCircuit {
+
+ def negate(a: Boolean) = {
+ var b = true
+ a && { b = false; true }
+ b
+ } ensuring { res => res != a }
+
+ def negateOr(a: Boolean) = {
+ var b = false
+ a || { b = true; true }
+ b
+ } ensuring { res => res != a }
+
+}
--
GitLab