Skip to content

Commit

Permalink
fix test compilation issues
Browse files Browse the repository at this point in the history
  • Loading branch information
jcp19 committed Feb 26, 2025
1 parent 0b1e2cc commit 7049839
Show file tree
Hide file tree
Showing 2 changed files with 9 additions and 15 deletions.
4 changes: 1 addition & 3 deletions src/test/scala/RewriteWithCycles.scala
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,6 @@
import org.scalatest.funsuite.AnyFunSuite
import viper.silver.ast.utility.rewriter.{Rewritable, StrategyBuilder}

import scala.reflect.runtime.{universe => reflection}

class RewriteWithCycles extends AnyFunSuite {


Expand Down Expand Up @@ -44,7 +42,7 @@ class RewriteWithCycles extends AnyFunSuite {
}

// Visit all reachable nodes in the graph and call func on them.
def visitAll[I : reflection.TypeTag](s:SlimGraph[I], func:I=>I) = {
def visitAll[I](s:SlimGraph[I], func:I=>I) = {
val strat = StrategyBuilder.Ancestor[SlimGraph[I]]({
case (sG, c) => {
if(c.ancestorList.dropRight(1).contains(sG))
Expand Down
20 changes: 8 additions & 12 deletions src/test/scala/UtilityTests.scala
Original file line number Diff line number Diff line change
Expand Up @@ -6,24 +6,20 @@

import org.scalatest.funsuite.AnyFunSuite
import org.scalatest.matchers.should.Matchers
import viper.silver.ast._
import viper.silver.ast.utility.ImpureAssumeRewriter


class UtilityTests extends AnyFunSuite with Matchers {

/* These tests exercise utility methods on the AST (transformers, visitors, rewriters etc.) */

test("Assume rewriter (direct)"){ // assume acc(x.f) -> rewritten to -> assume perm(x.f) >= write
val assumeBody = FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(),Field("f",Int)(NoPosition))(NoPosition), Some(FullPerm()(NoPosition)))(NoPosition)
val testMethod : Method = Method("m1", Seq(), Seq(), Seq(), Seq(),
Some(Seqn(Seq(
Assume(assumeBody)(NoPosition)
), Seq())(NoPosition, NoInfo, NoTrafos))
)(NoPosition)

val testProgram : Program = Program(Seq(), Seq(Field("f",Int)(NoPosition)), Seq(), Seq(), Seq(testMethod), Seq())(NoPosition)

// val assumeBody = FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(),Field("f",Int)(NoPosition))(NoPosition), Some(FullPerm()(NoPosition)))(NoPosition)
// val testMethod : Method = Method("m1", Seq(), Seq(), Seq(), Seq(),
// Some(Seqn(Seq(
// Assume(assumeBody)(NoPosition)
// ), Seq())(NoPosition, NoInfo, NoTrafos))
// )(NoPosition)

// val testProgram : Program = Program(Seq(), Seq(Field("f",Int)(NoPosition)), Seq(), Seq(), Seq(testMethod), Seq())(NoPosition)
// val rewritten = AssumeRewriter.rewrite(assumeBody,testProgram)

// rewritten should be (TrueLit()(NoPosition)) // this (spurious) test seems to cause an infinite recursion bug..
Expand Down

0 comments on commit 7049839

Please sign in to comment.