Bumped compiler version to 3.5.2 and removed a patmat warning (#1599)

* Bumped compiler version to 3.5.2 and removed a patmat warning * Depend on Inox module compiled with 3.5.2 * bump sbt plugin --------- Co-authored-by: Samuel Chassot <[email protected]>
epfl-lara · Nov 5, 2024 · e22e91a · e22e91a
1 parent 89534df
commit e22e91a
Show file tree

Hide file tree

Showing 6 changed files with 8 additions and 7 deletions.
diff --git a/bin/package-sbt-plugin.sh b/bin/package-sbt-plugin.sh
@@ -6,8 +6,8 @@ if [[ $(git diff --stat) != '' ]]; then
   STAINLESS_VERSION="$STAINLESS_VERSION-SNAPSHOT"
 fi
 
-SCALA_VERSION="3.5.0"
-SCALA_LIB_VERSION="3.5.0"
+SCALA_VERSION="3.5.2"
+SCALA_LIB_VERSION="3.5.2"
 PUBLISHED_SBT_PLUGIN_DIR="$HOME/.ivy2/local/ch.epfl.lara/sbt-stainless/scala_2.12/sbt_1.0/$STAINLESS_VERSION"
 LIB_SCALA_VERSION_JAR_NAME_PART=$(echo $SCALA_LIB_VERSION | cut -d '.' -f 1)
 PUBLISHED_LIB_DIR="$HOME/.ivy2/local/ch.epfl.lara/stainless-library_$LIB_SCALA_VERSION_JAR_NAME_PART/$STAINLESS_VERSION"

diff --git a/build.sbt b/build.sbt
@@ -40,9 +40,9 @@ lazy val nTestSuiteParallelism = {
 
 // The Scala version with which Stainless is compiled.
 // Note: in case of version bump, do not forget to update the `test` files in `sbt-plugin` (for `sbt scripted`)!
-val stainlessScalaVersion = "3.5.0"
+val stainlessScalaVersion = "3.5.2"
 val frontendDottyVersion = stainlessScalaVersion
-// The Stainless libraries use Scala 2.13 and Scala 3.3, and is compatible only with Scala 3.3.
+// The Stainless libraries use Scala 2.13 and Scala 3.5, and is compatible only with Scala 3.5.
 val stainlessLibScalaVersion = stainlessScalaVersion
 
 scalaVersion := stainlessScalaVersion

diff --git a/core/src/main/scala/stainless/extraction/inlining/FunctionInlining.scala b/core/src/main/scala/stainless/extraction/inlining/FunctionInlining.scala
@@ -88,6 +88,7 @@ class FunctionInlining(override val s: Trees, override val t: trace.Trees)
                   Assert(annotated(cond.setPos(fi), DropVCs), Some(s"Inlined precondition$num of " + tfd.id.asString), acc).setPos(fi),
                   i-1
                 )
+              case (spec, (acc,i)) => context.reporter.fatalError(f"In addPreconditionAssertions, I did not expect spec that is not LetInSpec or Precondition; I got the following spec: ${spec.toString}")
             }._1
           }
 

diff --git a/inox b/inox
diff --git a/sbt-plugin/src/sbt-test/sbt-plugin/ghost/test b/sbt-plugin/src/sbt-test/sbt-plugin/ghost/test
@@ -1,5 +1,5 @@
 > + tailrec/run
 > + basic/run
-$ exists basic/target/scala-3.5.0/classes/test/Main.class
+$ exists basic/target/scala-3.5.2/classes/test/Main.class
 $ absent basic/target/sneakyGhostCalled basic/target/insideGhostCalled
 > + actor-tests/compile
diff --git a/sbt-plugin/src/sbt-test/sbt-plugin/simple/test b/sbt-plugin/src/sbt-test/sbt-plugin/simple/test
@@ -1,5 +1,5 @@
 > assertLogMessage
 > + success/compile
 # check that a module on which stainless verification passes compiles fine (i.e., binaries are produced)
-$ exists success/target/scala-3.5.0/classes/Extern1.class
+$ exists success/target/scala-3.5.2/classes/Extern1.class
 # > failure/checkScalaFailures
-Original file line number
+Diff line change
@@ Expand Up @@
                       Assert(annotated(cond.setPos(fi), DropVCs), Some(s"Inlined precondition$num of " + tfd.id.asString), acc).setPos(fi),
                       i-1
                     )
+                  case (spec, (acc,i)) => context.reporter.fatalError(f"In addPreconditionAssertions, I did not expect spec that is not LetInSpec or Precondition; I got the following spec: ${spec.toString}")
                 }._1
               }
@@ Expand Down @@