From 0201d59fe2d91abc31db7dda8bec4bc921fe8a0b Mon Sep 17 00:00:00 2001 From: gauravpartha Date: Fri, 15 Sep 2023 10:14:27 +0200 Subject: [PATCH 1/3] Havoc scoped variables explicitly --- .../scala/viper/carbon/modules/impls/DefaultStmtModule.scala | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultStmtModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultStmtModule.scala index 11272560..57b4facb 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultStmtModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultStmtModule.scala @@ -253,9 +253,11 @@ class DefaultStmtModule(val verifier: Verifier) extends StmtModule with SimpleSt case sil.Seqn(ss, scopedDecls) => val locals = scopedDecls.collect {case l: sil.LocalVarDecl => l} locals map (v => mainModule.env.define(v.localVar)) // add local variables to environment - val s = + val s = { + MaybeCommentBlock("Havoc scoped variables", locals map (lv => Havoc(mainModule.env.get(lv.localVar)))) ++ MaybeCommentBlock("Assumptions about local variables", locals map (a => mainModule.allAssumptionsAboutValue(a.typ, mainModule.translateLocalVarDecl(a), true))) ++ Seqn(ss map (st => translateStmt(st, statesStack, allStateAssms, duringPackage))) + } locals map (v => mainModule.env.undefine(v.localVar)) // remove local variables from environment // return to avoid adding a comment, and to avoid the extra 'assumeGoodState' return s From 1e40bcb676c947fadd2ef7e9d7239a3f5e651479 Mon Sep 17 00:00:00 2001 From: gauravpartha Date: Fri, 15 Sep 2023 12:20:35 +0200 Subject: [PATCH 2/3] adjust silver commit (ignore array_quick_select.vpr test) --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 65ec3412..e89d532d 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 65ec3412bb9118a8c465462c94dab6d0d53da5f4 +Subproject commit e89d532d50fedaca4a0c668ba8c793fddf6ea525 From 735909860bddc1386afa21bcaeb51952bd1de887 Mon Sep 17 00:00:00 2001 From: gauravpartha Date: Fri, 15 Sep 2023 13:32:01 +0200 Subject: [PATCH 3/3] update silver submodule --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index e89d532d..65819343 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit e89d532d50fedaca4a0c668ba8c793fddf6ea525 +Subproject commit 658193435975a0deb3598eb8f03a8f3f4d43ee0b