add test, fix positioning & block placement

viperproject · Jul 15, 2024 · 8f2fa05 · 8f2fa05
1 parent 1e41b5e
commit 8f2fa05
Show file tree

Hide file tree

Showing 4 changed files with 17 additions and 6 deletions.
diff --git a/src/main/scala/viper/silver/parser/ParseAst.scala b/src/main/scala/viper/silver/parser/ParseAst.scala
@@ -1467,7 +1467,7 @@ case class PNewExp(keyword: PKw.New, fields: PGrouped.Paren[Either[PSym.Star, PD
   def forceSubstitution(ts: PTypeSubstitution) = {}
 }
 
-sealed trait PScope extends PNode {
+trait PScope extends PNode {
   val scopeId = PScope.uniqueId()
 }
 

diff --git a/src/main/scala/viper/silver/plugin/standard/reasoning/ReasoningPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/reasoning/ReasoningPASTExtension.scala
@@ -9,7 +9,7 @@ package viper.silver.plugin.standard.reasoning
 import viper.silver.FastMessaging
 import viper.silver.ast.{Exp, ExtensionExp, LocalVar, LocalVarDecl, Position, Seqn, Stmt, Trigger}
 import viper.silver.parser.TypeHelper.Bool
-import viper.silver.parser.{NameAnalyser, PAssignTarget, PCall, PCallable, PDelimited, PExp, PExtender, PGrouped, PIdnRef, PIdnUseExp, PKeywordLang, PKeywordStmt, PKw, PLabel, PLocalVarDecl, PReserved, PSeqn, PStmt, PSym, PSymOp, PTrigger, PType, PTypeSubstitution, Translator, TypeChecker}
+import viper.silver.parser.{NameAnalyser, PAssignTarget, PCall, PCallable, PDelimited, PExp, PExtender, PGrouped, PIdnRef, PIdnUseExp, PKeywordLang, PKeywordStmt, PKw, PLabel, PLocalVarDecl, PReserved, PScope, PSeqn, PStmt, PSym, PSymOp, PTrigger, PType, PTypeSubstitution, Translator, TypeChecker}
 
 case object PObtainKeyword extends PKw("obtain") with PKeywordLang with PKeywordStmt
 case object PWhereKeyword extends PKw("where") with PKeywordLang
@@ -42,7 +42,7 @@ case class PExistentialElim(obtainKw: PReserved[PObtainKeyword.type], delimitedV
   }
 }
 
-case class PUniversalIntro(proveKw: PReserved[PProveKeyword.type], forallKw: PKw.Forall, delimitedVarDecls: PDelimited[PLocalVarDecl, PSym.Comma], triggers: Seq[PTrigger], assumingKw: PReserved[PAssumingKeyword.type], e1: PExp, impliesKw: PReserved[PImpliesKeyword.type], e2: PExp, block: PSeqn)(val pos: (Position, Position)) extends PExtender with PStmt {
+case class PUniversalIntro(proveKw: PReserved[PProveKeyword.type], forallKw: PKw.Forall, delimitedVarDecls: PDelimited[PLocalVarDecl, PSym.Comma], triggers: Seq[PTrigger], assumingKw: PReserved[PAssumingKeyword.type], e1: PExp, impliesKw: PReserved[PImpliesKeyword.type], e2: PExp, block: PSeqn)(val pos: (Position, Position)) extends PExtender with PStmt with PScope {
   lazy val varDecls: Seq[PLocalVarDecl] = delimitedVarDecls.toSeq
 
   override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = {
@@ -60,7 +60,7 @@ case class PUniversalIntro(proveKw: PReserved[PProveKeyword.type], forallKw: PKw
       triggers.map { t1 => Trigger(t1.exp.inner.toSeq.map { t2 => t.exp(t2) })(t.liftPos(t1)) },
       t.exp(e1),
       t.exp(e2),
-      t.stmt(block).asInstanceOf[Seqn])(t.liftPos(e1))
+      t.stmt(block).asInstanceOf[Seqn])(t.liftPos(block))
   }
 }
 

diff --git a/src/main/scala/viper/silver/plugin/standard/reasoning/ReasoningPlugin.scala b/src/main/scala/viper/silver/plugin/standard/reasoning/ReasoningPlugin.scala
@@ -237,15 +237,15 @@ class ReasoningPlugin(@unused reporter: viper.silver.reporter.Reporter,
             Seq(Inhale(u.assumingExp)(u.assumingExp.pos)),
             Seq.empty)(u.assumingExp.pos),
           Seqn(Seq.empty, Seq.empty)(u.assumingExp.pos)
-        )(u.assumingExp.pos),
+        )(u.pos),
         // execute block
         u.block,
         // conditionally assert imply expression
         Assert(Implies(boolvar.localVar, u.implyingExp)(u.implyingExp.pos))(u.implyingExp.pos, errT = errTransformer),
         Inhale(Forall(quantifiedVars, newTrigs, Implies(LabelledOld(newExp1, lbl)(u.implyingExp.pos), newExp2)(u.implyingExp.pos))(u.implyingExp.pos))(u.implyingExp.pos)
       ),
       Seq(boolvar) ++ u.varList
-    )(u.assumingExp.pos)
+    )(u.pos)
   }
 
   override def beforeVerify(input: Program): Program = {

diff --git a/src/test/resources/reasoning/universal_introduction/ui_func.vpr b/src/test/resources/reasoning/universal_introduction/ui_func.vpr
@@ -32,3 +32,14 @@ method mFunctionNOK()
         y := func1(x)
     }
 }
+
+function func2(e: Ref): Ref {
+    e
+}
+
+method mFunction2NOK() {
+    var x: Ref
+    prove forall i:Ref assuming true implies i == x {
+        x := test(i)
+    }
+}