From d22361664f12d137bba3f7ce68d12e6ab1993c6b Mon Sep 17 00:00:00 2001
From: Marco Antognini <antognini.marco@gmail.com>
Date: Wed, 6 Jan 2016 17:14:24 +0100
Subject: [PATCH] Improve tuple constness
---
src/main/scala/leon/genc/CAST.scala | 7 ++++++-
src/main/scala/leon/genc/CConverter.scala | 2 +-
2 files changed, 7 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/genc/CAST.scala b/src/main/scala/leon/genc/CAST.scala
index 07f4b558d..e98d9c1ab 100644
--- a/src/main/scala/leon/genc/CAST.scala
+++ b/src/main/scala/leon/genc/CAST.scala
@@ -18,6 +18,11 @@ object CAST { // C Abstract Syntax Tree
/* ------------------------------------------------------------ Types ----- */
abstract class Type(val rep: String) extends Tree {
override def toString = rep
+
+ def mutable: Type = this match {
+ case Const(typ) => typ.mutable
+ case _ => this
+ }
}
/* Type Modifiers */
@@ -149,7 +154,7 @@ object CAST { // C Abstract Syntax Tree
val name = Id("__leon_tuple_" + bases.mkString("_") + "_t")
val fields = bases.zipWithIndex map {
- case (typ, idx) => Var(getNthId(idx + 1), typ)
+ case (typ, idx) => Val(getNthId(idx + 1), typ)
}
Struct(name, fields)
diff --git a/src/main/scala/leon/genc/CConverter.scala b/src/main/scala/leon/genc/CConverter.scala
index 10408436e..4b572f3af 100644
--- a/src/main/scala/leon/genc/CConverter.scala
+++ b/src/main/scala/leon/genc/CConverter.scala
@@ -666,7 +666,7 @@ class CConverter(val ctx: LeonContext, val prog: Program) {
// Similarly to buildDeclInitVar:
val (tmp, body) = f.value match {
case CAST.IfElse(cond, thn, elze) =>
- val tmp = CAST.FreshVar(typ, "normexec")
+ val tmp = CAST.FreshVar(typ.mutable, "normexec")
val decl = CAST.DeclVar(tmp)
val ifelse = buildIfElse(cond, injectAssign(tmp, thn), injectAssign(tmp, elze))
val body = f.body ~~ decl ~ ifelse
--
GitLab