From a6ab44ad2bd69c8e1e4b9cff7b0bb45f5aeaed48 Mon Sep 17 00:00:00 2001
From: Marco Antognini <antognini.marco@gmail.com>
Date: Wed, 16 Dec 2015 19:16:08 +0100
Subject: [PATCH] Add support for case class
---
src/main/scala/leon/genc/CConverter.scala | 9 +++++++++
.../regression/genc/valid/CaseClass.scala | 19 +++++++++++++++++++
2 files changed, 28 insertions(+)
create mode 100644 src/test/resources/regression/genc/valid/CaseClass.scala
diff --git a/src/main/scala/leon/genc/CConverter.scala b/src/main/scala/leon/genc/CConverter.scala
index a29943083..596bef698 100644
--- a/src/main/scala/leon/genc/CConverter.scala
+++ b/src/main/scala/leon/genc/CConverter.scala
@@ -367,6 +367,15 @@ class CConverter(val ctx: LeonContext, val prog: Program) {
argsFs.bodies ~~ CAST.StructInit(args, struct)
+ case CaseClassSelector(_, x1, fieldId) =>
+ val struct = convertToStruct(x1.getType)
+ val x2 = convertToStmt(x1)
+
+ val fs = normaliseExecution((x2, struct) :: Nil)
+ val x = fs.values.head
+
+ fs.bodies ~~ CAST.AccessField(x, convertToId(fieldId))
+
case LessThan(lhs, rhs) => buildBinOp(lhs, "<", rhs)
case GreaterThan(lhs, rhs) => buildBinOp(lhs, ">", rhs)
case LessEquals(lhs, rhs) => buildBinOp(lhs, "<=", rhs)
diff --git a/src/test/resources/regression/genc/valid/CaseClass.scala b/src/test/resources/regression/genc/valid/CaseClass.scala
new file mode 100644
index 000000000..bf104e378
--- /dev/null
+++ b/src/test/resources/regression/genc/valid/CaseClass.scala
@@ -0,0 +1,19 @@
+import leon.lang._
+
+object CaseClass {
+
+ case class Color(r: Int, g: Int, b: Int)
+
+ def red = Color(0, 255, 0)
+ def cyan = Color(0, 255, 255)
+
+ def sub(c: Color, d: Color) = Color(c.r - d.r, c.g - d.g, c.b - d.b)
+
+ def main = {
+ val c = red
+ val d = cyan
+ val z = sub(c, d).g
+ z
+ }
+
+}
--
GitLab