From 7a72e998d7e5bae9a3fb1e8bfa9b8c97ff9af4c8 Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Mon, 6 Dec 2021 17:15:17 +0100 Subject: [PATCH 1/2] sets scope for functions, predicates, and methods (of ASTs) --- .../scala/verifier/DefaultMasterVerifier.scala | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/src/main/scala/verifier/DefaultMasterVerifier.scala b/src/main/scala/verifier/DefaultMasterVerifier.scala index a4cc6b41b..31778cc8b 100644 --- a/src/main/scala/verifier/DefaultMasterVerifier.scala +++ b/src/main/scala/verifier/DefaultMasterVerifier.scala @@ -27,7 +27,7 @@ import viper.silicon.supporters._ import viper.silicon.supporters.functions.DefaultFunctionVerificationUnitProvider import viper.silicon.supporters.qps._ import viper.silicon.utils.Counter -import viper.silver.ast.BackendType +import viper.silver.ast.{BackendType, Member} import viper.silver.ast.utility.rewriter.Traverse import viper.silver.cfg.silver.SilverCfg import viper.silver.reporter.{ConfigurationConfirmation, ExecutionTraceReport, Reporter, VerificationResultMessage} @@ -194,7 +194,7 @@ class DefaultMasterVerifier(config: Config, override val reporter: Reporter) val elapsed = System.currentTimeMillis() - startTime reporter report VerificationResultMessage(s"silicon", function, elapsed, condenseToViperResult(results)) logger debug s"Silicon finished verification of function `${function.name}` in ${viper.silver.reporter.format.formatMillisReadably(elapsed)} seconds with the following result: ${condenseToViperResult(results).toString}" - results + setErrorScope(results, function) }) val predicateVerificationResults = predicateSupporter.units.toList flatMap (predicate => { @@ -203,7 +203,7 @@ class DefaultMasterVerifier(config: Config, override val reporter: Reporter) val elapsed = System.currentTimeMillis() - startTime reporter report VerificationResultMessage(s"silicon", predicate, elapsed, condenseToViperResult(results)) logger debug s"Silicon finished verification of predicate `${predicate.name}` in ${viper.silver.reporter.format.formatMillisReadably(elapsed)} seconds with the following result: ${condenseToViperResult(results).toString}" - results + setErrorScope(results, predicate) }) decider.prover.stop() @@ -231,7 +231,7 @@ class DefaultMasterVerifier(config: Config, override val reporter: Reporter) reporter report VerificationResultMessage(s"silicon", method, elapsed, condenseToViperResult(results)) logger debug s"Silicon finished verification of method `${method.name}` in ${viper.silver.reporter.format.formatMillisReadably(elapsed)} seconds with the following result: ${condenseToViperResult(results).toString}" - results + setErrorScope(results, method) }) }) ++ cfgs.map(cfg => { val s = createInitialState(cfg, program)/*.copy(parallelizeBranches = true)*/ /* [BRANCH-PARALLELISATION] */ @@ -468,4 +468,12 @@ class DefaultMasterVerifier(config: Config, override val reporter: Reporter) }) } } + + private def setErrorScope(results: Seq[VerificationResult], scope: Member): Seq[VerificationResult] = { + results.foreach { + case Failure(err) => err.scope = Some(scope) + case _ => + } + results + } } From 32be5f412d80cc81406f217ecdf87dab05bf2a97 Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Mon, 6 Dec 2021 17:25:42 +0100 Subject: [PATCH 2/2] fixes CI compilation issues while being backwards compatible --- src/main/scala/verifier/DefaultMasterVerifier.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/verifier/DefaultMasterVerifier.scala b/src/main/scala/verifier/DefaultMasterVerifier.scala index 31778cc8b..cea86c4c1 100644 --- a/src/main/scala/verifier/DefaultMasterVerifier.scala +++ b/src/main/scala/verifier/DefaultMasterVerifier.scala @@ -471,7 +471,7 @@ class DefaultMasterVerifier(config: Config, override val reporter: Reporter) private def setErrorScope(results: Seq[VerificationResult], scope: Member): Seq[VerificationResult] = { results.foreach { - case Failure(err) => err.scope = Some(scope) + case f: Failure => f.message.scope = Some(scope) case _ => } results