Skip to content

Commit

Permalink
Don't try to delete nonexistent preprocessor output
Browse files Browse the repository at this point in the history
Clang can remove the output file on its own if it fails, so only delete the file if it hasn't already.

Adds (integration) tests.

Fixes #1235.
  • Loading branch information
wandernauta committed Sep 15, 2024
1 parent 8fab87a commit 78ad163
Show file tree
Hide file tree
Showing 5 changed files with 18 additions and 17 deletions.
2 changes: 1 addition & 1 deletion src/parsers/vct/parsers/parser/ColCPPParser.scala
Original file line number Diff line number Diff line change
Expand Up @@ -94,6 +94,6 @@ case class ColCPPParser(
val result = ColIPPParser(debugOptions, blameProvider, Some(baseOrigin))
.parse[G](ireadable)
result
} finally { Files.delete(interpreted) }
} finally { Files.deleteIfExists(interpreted) }
}
}
2 changes: 1 addition & 1 deletion src/parsers/vct/parsers/parser/ColCParser.scala
Original file line number Diff line number Diff line change
Expand Up @@ -94,6 +94,6 @@ case class ColCParser(
val result = ColIParser(debugOptions, blameProvider, Some(baseOrigin))
.parse[G](ireadable)
result
} finally { Files.delete(interpreted) }
} finally { Files.deleteIfExists(interpreted) }
}
}
5 changes: 5 additions & 0 deletions test/main/vct/test/integration/examples/CPPSpec.scala
Original file line number Diff line number Diff line change
Expand Up @@ -23,4 +23,9 @@ class CPPSpec extends VercorsSpec {
vercors should verify using silicon example "concepts/cpp/methods/Permissions.cpp"
vercors should verify using silicon example "concepts/cpp/methods/Predicates.cpp"
vercors should verify using silicon example "concepts/cpp/methods/PureGhostMethod.cpp"

vercors should error withCode "preprocessorError" in "Source file with preprocessor error" cpp
"""
#define foo(
"""
}
5 changes: 5 additions & 0 deletions test/main/vct/test/integration/examples/CSpec.scala
Original file line number Diff line number Diff line change
Expand Up @@ -346,6 +346,11 @@ class CSpec extends VercorsSpec {
}
"""

vercors should error withCode "preprocessorError" in "Source file with preprocessor error" c
"""
#define foo(
"""

vercors should verify using silicon in "Parallel omp loop with declarations inside" c
"""
#include <omp.h>
Expand Down
21 changes: 6 additions & 15 deletions test/main/vct/test/integration/helper/VercorsSpec.scala
Original file line number Diff line number Diff line change
Expand Up @@ -212,26 +212,17 @@ abstract class VercorsSpec extends AnyFlatSpec {
}

class DescPhrase(val verdict: Verdict, val backends: Seq[Backend], val desc: String, val flags: Seq[String]) {
def pvl(data: String)(implicit pos: source.Position): Unit = {
val inputs = Seq(LiteralReadable("test.pvl", data))
private def literal(suffix: String, data: String)(implicit pos: source.Position): Unit = {
val inputs = Seq(LiteralReadable(s"test.$suffix", data))
for(backend <- backends) {
registerTest(verdict, desc, Seq(new Tag("literalCase")), backend, inputs, flags)
}
}

def java(data: String)(implicit pos: source.Position): Unit = {
val inputs = Seq(LiteralReadable("test.java", data))
for(backend <- backends) {
registerTest(verdict, desc, Seq(new Tag("literalCase")), backend, inputs, flags)
}
}

def c(data: String)(implicit pos: source.Position): Unit = {
val inputs = Seq(LiteralReadable("test.c", data))
for(backend <- backends) {
registerTest(verdict, desc, Seq(new Tag("literalCase")), backend, inputs, flags)
}
}
def pvl(data: String)(implicit pos: source.Position): Unit = literal("pvl", data)
def java(data: String)(implicit pos: source.Position): Unit = literal("java", data)
def c(data: String)(implicit pos: source.Position): Unit = literal("c", data)
def cpp(data: String)(implicit pos: source.Position): Unit = literal("cpp", data)
}

val vercors: VercorsWord = new VercorsWord
Expand Down

0 comments on commit 78ad163

Please sign in to comment.