From a58d5bded57e801d2b7d0ad795a510091cda46b4 Mon Sep 17 00:00:00 2001 From: gauravpartha Date: Mon, 21 Nov 2022 19:37:56 +0100 Subject: [PATCH 1/7] add new Boogie reserved keyword is --- src/main/scala/viper/carbon/boogie/BoogieNameGenerator.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/carbon/boogie/BoogieNameGenerator.scala b/src/main/scala/viper/carbon/boogie/BoogieNameGenerator.scala index 0ac0a96e..6c9bfb88 100644 --- a/src/main/scala/viper/carbon/boogie/BoogieNameGenerator.scala +++ b/src/main/scala/viper/carbon/boogie/BoogieNameGenerator.scala @@ -19,7 +19,7 @@ class BoogieNameGenerator extends DefaultNameGenerator { "invariant", "goto", "break", "return", "call", "forall", "assert", "havoc", "assume", "returns", "var", "implementation", "axiom", "exists", "old", "false", "real", "int", "true", "bool", "finite", "ensures", "requires", "modifies", "where", "par", "lambda", "uses", "RTP", "RTZ", "yield", "async", "roundNearestTiesToAway", "roundNearestTiesToEven", "extends", "roundTowardPositive", - "roundTowardZero", "RNA", "RTN", "roundTowardNegative", "RNE") ++ + "roundTowardZero", "RNA", "RTN", "roundTowardNegative", "RNE", "is") ++ Set("Set", "MultiSet", "Seq") val SMTreservedNames: Set[String] = Set( // Basic symbols: From afe5bbeb043731ee9aeae28e8793b388d6600f14 Mon Sep 17 00:00:00 2001 From: gauravpartha Date: Mon, 21 Nov 2022 19:41:08 +0100 Subject: [PATCH 2/7] update to Boogie 2.15.9 in CI --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 819ffed5..11848962 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -14,7 +14,7 @@ jobs: container: gobraverifier/gobra-base:v5_z3_4.8.7 # Thank you, Gobra team env: BOOGIE_EXE: "boogie/Boogie" - LINUX_BOOGIE_URL: "https://github.com/viperproject/boogie-builder/releases/download/bae82d3a7b383161/boogie-linux.zip" + LINUX_BOOGIE_URL: "https://github.com/viperproject/boogie-builder/releases/download/7449a7a899c02c95/boogie-linux.zip" steps: - name: Checkout Carbon uses: actions/checkout@v2 From 9317e1d7ba3e4b9c6c2982986779051b8703b83d Mon Sep 17 00:00:00 2001 From: gauravpartha Date: Mon, 21 Nov 2022 19:44:15 +0100 Subject: [PATCH 3/7] output Boogie version in CI --- .github/workflows/ci.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 11848962..735a2e3c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -57,6 +57,7 @@ jobs: unzip boogie-linux.zip rm -rf boogie-linux.zip mv binaries-linux boogie + boogie/Boogie /version pwd - name: Test Carbon From 6ab496eff4bd1653179050b033190251fb4a4a0d Mon Sep 17 00:00:00 2001 From: gauravpartha Date: Mon, 19 Dec 2022 14:37:09 +0100 Subject: [PATCH 4/7] Try Boogie SMT name normalization option --- src/main/scala/viper/carbon/verifier/BoogieInterface.scala | 1 + 1 file changed, 1 insertion(+) diff --git a/src/main/scala/viper/carbon/verifier/BoogieInterface.scala b/src/main/scala/viper/carbon/verifier/BoogieInterface.scala index 501ef46e..ee66e6ba 100644 --- a/src/main/scala/viper/carbon/verifier/BoogieInterface.scala +++ b/src/main/scala/viper/carbon/verifier/BoogieInterface.scala @@ -50,6 +50,7 @@ trait BoogieInterface { def defaultOptions = Seq("/vcsCores:" + java.lang.Runtime.getRuntime.availableProcessors, "/errorTrace:0", "/errorLimit:10000000", + "/normalizeNames:1", "/proverOpt:O:smt.AUTO_CONFIG=false", "/proverOpt:O:smt.PHASE_SELECTION=0", "/proverOpt:O:smt.RESTART_STRATEGY=0", From 7d9543f3f0761744e8074f9704eb7718dd82b72a Mon Sep 17 00:00:00 2001 From: gauravpartha Date: Mon, 19 Dec 2022 15:21:22 +0100 Subject: [PATCH 5/7] Try Boogie emitDebugInformation:0 option --- src/main/scala/viper/carbon/verifier/BoogieInterface.scala | 1 + 1 file changed, 1 insertion(+) diff --git a/src/main/scala/viper/carbon/verifier/BoogieInterface.scala b/src/main/scala/viper/carbon/verifier/BoogieInterface.scala index ee66e6ba..0a5aa8ca 100644 --- a/src/main/scala/viper/carbon/verifier/BoogieInterface.scala +++ b/src/main/scala/viper/carbon/verifier/BoogieInterface.scala @@ -51,6 +51,7 @@ trait BoogieInterface { "/errorTrace:0", "/errorLimit:10000000", "/normalizeNames:1", + "/emitDebugInformation:0", "/proverOpt:O:smt.AUTO_CONFIG=false", "/proverOpt:O:smt.PHASE_SELECTION=0", "/proverOpt:O:smt.RESTART_STRATEGY=0", From 5463c0faa5299d5015256e29a3b95b6807fd188b Mon Sep 17 00:00:00 2001 From: gauravpartha Date: Wed, 21 Dec 2022 19:58:18 +0100 Subject: [PATCH 6/7] do not change options for Boogie 12.15.9 --- src/main/scala/viper/carbon/verifier/BoogieInterface.scala | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/main/scala/viper/carbon/verifier/BoogieInterface.scala b/src/main/scala/viper/carbon/verifier/BoogieInterface.scala index 0a5aa8ca..501ef46e 100644 --- a/src/main/scala/viper/carbon/verifier/BoogieInterface.scala +++ b/src/main/scala/viper/carbon/verifier/BoogieInterface.scala @@ -50,8 +50,6 @@ trait BoogieInterface { def defaultOptions = Seq("/vcsCores:" + java.lang.Runtime.getRuntime.availableProcessors, "/errorTrace:0", "/errorLimit:10000000", - "/normalizeNames:1", - "/emitDebugInformation:0", "/proverOpt:O:smt.AUTO_CONFIG=false", "/proverOpt:O:smt.PHASE_SELECTION=0", "/proverOpt:O:smt.RESTART_STRATEGY=0", From b5ee3dbf863e8d6191352a68583bf074e0ce6a19 Mon Sep 17 00:00:00 2001 From: gauravpartha Date: Wed, 21 Dec 2022 20:04:03 +0100 Subject: [PATCH 7/7] update Silver dependency --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 9888c231..2705edcc 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 9888c23199672bb01c8729eeedd9e18479ff15da +Subproject commit 2705edccab1e95b3df4ea2a0961225b0bcd5338b