Chalice: Code cleanup.

3 files changed, 5 insertions, 29 deletions

diff --git a/Chalice/src/main/scala/Ast.scala b/Chalice/src/main/scala/Ast.scala
index 943e83b2..78d2ac74 100644
--- a/Chalice/src/main/scala/Ast.scala
+++ b/Chalice/src/main/scala/Ast.scala
@@ -182,9 +182,6 @@ case class Method(id: String, ins: List[Variable], outs: List[Variable], spec: L
   override def Outs = outs

 }

 case class Predicate(id: String, private val rawDefinition: Expression) extends NamedMember(id) {

-  // list of functions that possibly depend on this predicate (that is, functions

-  // that mention this predicate in their precondition)

-  var dependentFunctions: List[Function] = List()

   lazy val definition: Expression = rawDefinition.transform {

     case Epsilon | MethodEpsilon => Some(PredicateEpsilon(None))

     case _ => None

diff --git a/Chalice/src/main/scala/Resolver.scala b/Chalice/src/main/scala/Resolver.scala
index 6bc2e054..17bb668e 100644
--- a/Chalice/src/main/scala/Resolver.scala
+++ b/Chalice/src/main/scala/Resolver.scala
@@ -228,14 +228,7 @@ object Resolver {
            case f@Function(id, ins, out, spec, definition) =>

               // TODO: disallow credit(...) expressions in function specifications

              spec foreach {

-               case Precondition(e) =>

-                 ResolveExpr(e, context, false, true)(false)

-                 // add the function to all predicates it depends on

-                 e visit {_ match {

-                   case pred@MemberAccess(e, p) if pred.isPredicate =>

-                     pred.predicate.dependentFunctions = f :: pred.predicate.dependentFunctions

-                   case _ =>}

-                 }

+               case Precondition(e) => ResolveExpr(e, context, false, true)(false)

                case Postcondition(e) => ResolveExpr(e, context, false, true)(false)

                case lc : LockChange => context.Error(lc.pos, "lockchange not allowed on function") 

              }

diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala
index d370813e..213a361b 100644
--- a/Chalice/src/main/scala/Translator.scala
+++ b/Chalice/src/main/scala/Translator.scala
@@ -264,8 +264,7 @@ class Translator {
             (applyF ==@ limitedApplyF)))) ::

       Nil

     else

-      Nil) :::

-    Boogie.Function(functionName(f) + "#trigger", formalsOnlyReceiver, BVar("$myresult", tbool)) :: Nil

+      Nil)

   }

 

   def framingAxiom(f: Function): List[Decl] = {

@@ -693,7 +692,7 @@ class Translator {
         // pick new k

         val (foldKV, foldK) = Boogie.NewBVar("foldK", tint, true)

         val stmts = Comment("fold") ::

-        functionTrigger(o, pred.predicate) :::

+        functionTrigger(o, pred.predicate) ::

         BLocal(foldKV) :: bassume(0 < foldK && 1000*foldK < percentPermission(1) && 1000*foldK < methodK) ::

         isDefined(e) :::

         isDefined(perm) :::

@@ -2733,21 +2732,8 @@ object TranslationHelper {
   

   // output a dummy function assumption that serves as trigger for the function

   // definition axiom.

-  def functionTrigger(receiver: Expr, predicate: Predicate): List[Stmt] = {

-    bassume(FunctionApp("#" + predicate.FullName+"#trigger", receiver :: Nil)) :: Nil

-  }

-  def defaultValue(t: Type): Expr = {

-    t match {

-      case _ => 0

-      //case Type(MuClass, _) => bLockBottom

-      //case NamedType("ref") => bnull

-      /*case NamedType("bool") => false

-      case NamedType("int") => false

-      case NamedType("seq") => false

-      case NamedType("string") => 0

-      case IndexedType("Seq", arg) => createEmptySeq*/

-      //case _ => throw new InternalErrorException("unexpected type: " +t)

-    }

+  def functionTrigger(receiver: Expr, predicate: Predicate): Stmt = {

+    bassume(FunctionApp("#" + predicate.FullName+"#trigger", receiver :: Nil))

   }

   

   def emptyPartialHeap: Expr = Boogie.VarExpr("emptyPartialHeap")