diff --git a/src/main/scala/leon/genc/CConverter.scala b/src/main/scala/leon/genc/CConverter.scala index a29943083c774f88acbee39ff71490d8104089de..596bef6987c1c345b14b98416cef251b06595dd9 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 0000000000000000000000000000000000000000..bf104e378f0c06ed01dc1e61ae5649684a48684f --- /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 + } + +}