diff --git a/src/main/scala/leon/genc/CAST.scala b/src/main/scala/leon/genc/CAST.scala index 07f4b558d097920c20fd2d0943973fcd60fbd0be..e98d9c1ab0c3ae0dfcc873030ea5f5e8b7df8296 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 10408436e133a4339e55d0c021e6babbda8f640b..4b572f3afd2e9ee2e71e8da7f5737d7092b8e50e 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