Merge pull request #441 from viperproject/fix-termination-encoding-pr…

…oblem Fix encoding problem with termination checking
viperproject · Apr 28, 2022 · 530fb25 · 530fb25
2 parents c14dabd + bb8f21d
commit 530fb25
Showing 1 changed file with 11 additions and 4 deletions.
diff --git a/src/main/scala/viper/gobra/ast/internal/transform/CGEdgesTerminationTransform.scala b/src/main/scala/viper/gobra/ast/internal/transform/CGEdgesTerminationTransform.scala
@@ -38,14 +38,14 @@ object CGEdgesTerminationTransform extends InternalTransform {
                   *   {
                   *     assume false
                   *     if typeOf(recv) == impl1 {
-                  *       call implementation method from impl1 on recv
+                  *       call implementation method from impl1 on recv.(impl1)
                   *     }
                   *     if typeOf(recv) == impl2 {
-                  *       call implementation method from impl2 on recv
+                  *       call implementation method from impl2 on recv.(impl2)
                   *     }
                   *     ...
                   *     if typeOf(recv) == implN {
-                  *       call implementation method from implN on recv
+                  *       call implementation method from implN on recv.(implN)
                   *     }
                   *   }
                   */
@@ -61,7 +61,14 @@ object CGEdgesTerminationTransform extends InternalTransform {
                           case implProxy: in.MethodProxy =>
                             in.If(
                               in.EqCmp(in.TypeOf(m.receiver)(src), typeAsExpr(t)(src))(src),
-                              in.Seqn(Vector(in.MethodCall(m.results map parameterAsLocalValVar, in.Parameter.In(m.receiver.id, t)(src), implProxy, m.args)(src), in.Return()(src)))(src),
+                              in.Seqn(Vector(
+                                in.MethodCall(
+                                  m.results map parameterAsLocalValVar,
+                                  in.TypeAssertion(m.receiver, t)(src),
+                                  implProxy, m.args
+                                )(src),
+                                in.Return()(src)
+                              ))(src),
                               in.Seqn(Vector())(src)
                             )(src)
                           case v => Violation.violation(s"Expected a MethodProxy but got $v instead.")