From 727b1065e6298a23162caa6b533b95c3dc2a2129 Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <vkuncak@gmail.com>
Date: Tue, 13 Jul 2010 08:18:30 +0000
Subject: [PATCH] expr
---
testcases/ExprComp.scala | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/testcases/ExprComp.scala b/testcases/ExprComp.scala
index 1346f1abb..81829179c 100644
--- a/testcases/ExprComp.scala
+++ b/testcases/ExprComp.scala
@@ -67,12 +67,12 @@ object ExprComp {
def run0(p : Program) = run(p, EStack())
// Compiling expressions to programs
- def compile(e : Expr, acc : Program) : Program = e match {
+ def compile(e : Expr, acc : Program, vs : /* ghost */ ValueStack) : Program = { e match {
case Constant(v) => NProgram(PushVal(v), acc)
case Binary(e1,op,e2) => NProgram(ApplyBinOp(op),compile(e2,compile(e1,acc)))
- }
+ } } // ensuring (res => run(res, vs) = NStack(eval(e), vs))
- def compile0(e : Expr) : Program = compile(e, EProgram())
+ def compile0(e : Expr) : Program = compile(e, EProgram(), EStack())
// Correctness statement
// val anyS : ValueStack = EStack() // not really, but arbitrary
--
GitLab