Skip to content
Snippets Groups Projects
Commit fcaa876f authored by Nicolas Voirol's avatar Nicolas Voirol
Browse files

All TIP parser tests run

parent 6adf983f
No related branches found
No related tags found
No related merge requests found
......@@ -4,12 +4,11 @@ package inox
package tip
import org.scalatest._
import org.scalatest.concurrent._
import solvers._
import utils._
class TIPTestSuite extends InoxTestSuite with ResourceUtils {
class TIPTestSuite extends FunSuite with ResourceUtils {
val tipDir = "tip-benchmarks/benchmarks"
......@@ -17,14 +16,14 @@ class TIPTestSuite extends InoxTestSuite with ResourceUtils {
val files = resourceFiles(s"$tipDir/$base")
if (files.isEmpty) {
ignore(s"tip-benchmarks: $base directory not found (missing git submodule?") {_ => ()}
ignore(s"tip-benchmarks: $base directory not found (missing git submodule?") {}
} else {
val baseFile = new java.io.File(getClass.getResource(s"/$tipDir").getPath)
for (file <- files) {
test(s"Verifying tip-benchmarks/$base") { ctx =>
val (syms, clause) = parsers.TIPParser.parse(file)
val program = InoxProgram(ctx, syms)
val path = baseFile.toURI.relativize(file.toURI).getPath
assert(SimpleSolverAPI(SolverFactory.default(program)).solveSAT(clause).isSAT)
test(s"Parsing tip-benchmarks/$path") {
parsers.TIPParser.parse(file)
}
}
}
......
......@@ -261,10 +261,11 @@ trait Printers {
p"$id: $tpe"
case (tfd: TypedFunDef) => p"typed def ${tfd.id}[${tfd.tps}]"
case (afd: TypedADTDefinition) => p"typed class ${afd.id}[${afd.tps}]"
case TypeParameterDef(tp) => p"$tp"
case TypeParameter(id) => p"$id"
case IfExpr(c, t, ie: IfExpr) =>
optP {
p"""|if ($c) {
......
This diff is collapsed.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment