From a1bcfa903500c46de7d7458be3baceb3e2f6c939 Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Tue, 18 Jun 2024 08:42:26 +0200 Subject: [PATCH] Applies CR suggestions MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: João Pereira --- src/main/scala/viper/gobra/Gobra.scala | 2 +- src/main/scala/viper/gobra/frontend/Config.scala | 6 ++++-- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/main/scala/viper/gobra/Gobra.scala b/src/main/scala/viper/gobra/Gobra.scala index 1fd2e55cf..6561abfeb 100644 --- a/src/main/scala/viper/gobra/Gobra.scala +++ b/src/main/scala/viper/gobra/Gobra.scala @@ -31,7 +31,7 @@ import scala.concurrent.{Await, Future, TimeoutException} object GoVerifier { - val copyright = "(c) Copyright ETH Zurich 2012 - 2023" + val copyright = "(c) Copyright ETH Zurich 2012 - 2024" val name = "Gobra" diff --git a/src/main/scala/viper/gobra/frontend/Config.scala b/src/main/scala/viper/gobra/frontend/Config.scala index 5ba73246d..0cdeff3c9 100644 --- a/src/main/scala/viper/gobra/frontend/Config.scala +++ b/src/main/scala/viper/gobra/frontend/Config.scala @@ -365,12 +365,14 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals | ${GoVerifier.name} -r [OPTIONS] | | Mode 1 (-i): - | The first way interprets the list of files as one package that should be verified. + | The first mode takes a list of files that must belong to the same package. + | Files belonging to the same package but missing in the list are not considered for type-checking and verification. | Optionally, positional information can be provided for each file, e.g. @42,111, such that only | members at these positions will be verified. | | Mode 2 (-p): - | Interprets each provided directory as a directory storing files belonging to a single package. + | ${GoVerifier.name} verifies all `.${PackageResolver.gobraExtension}` and `.${PackageResolver.goExtension}` files in the provided directories, + | while treating files in the same directory as belonging to the same package. | Verifies these packages. The project root (by default the current working directory) is used to derive a | unique package identifier, since package names might not be unique. |