From bec0763cc3b19ec8d10348b5f224ceea83e46467 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Fri, 9 Aug 2024 20:21:18 +0200 Subject: [PATCH] adjust ids again --- .../dafny0/TriggerInPredicate.dfy.expect | 1 - .../Snapshots0.run.legacy.dfy.expect | 2 +- .../Snapshots1.run.legacy.dfy.expect | 2 +- .../Snapshots2.run.legacy.dfy.expect | 18 ++++++++--------- .../Snapshots5.run.legacy.dfy.expect | 8 ++++---- .../Snapshots8.run.legacy.dfy.expect | 20 +++++++++---------- .../Snapshots9.run.legacy.dfy.expect | 8 ++++---- .../git-issues/git-issue-3855.dfy.expect | 10 +++++----- .../triggers-prevent-some-inlining.dfy.expect | 2 -- 9 files changed, 34 insertions(+), 37 deletions(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TriggerInPredicate.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TriggerInPredicate.dfy.expect index 0e1599f1f50..e47d3f949d8 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TriggerInPredicate.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TriggerInPredicate.dfy.expect @@ -1,5 +1,4 @@ TriggerInPredicate.dfy(9,20): Info: Some instances of this call are not inlined. TriggerInPredicate.dfy(9,20): Info: Some instances of this call are not inlined. -TriggerInPredicate.dfy(9,20): Info: Some instances of this call are not inlined. Dafny program verifier finished with 0 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots0.run.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots0.run.legacy.dfy.expect index 711eb590f99..bc7f9c7e992 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots0.run.legacy.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots0.run.legacy.dfy.expect @@ -7,7 +7,7 @@ Processing call to procedure bar (call precondtion) in implementation foo (corre Processing call to procedure bar (call postcondition) in implementation foo (correctness) (at Snapshots0.v1.dfy(3,6)): >>> added axiom: (forall call0old#AT#$Heap: Heap, $Heap: Heap :: {:weight 30} { ##extracted_function##1(call0old#AT#$Heap, $Heap) } ##extracted_function##1(call0old#AT#$Heap, $Heap) == (true && Lit(false) && (forall $o: ref :: { $Heap[$o] } $o != null && $Unbox(read(call0old#AT#$Heap, $o, alloc)): bool ==> $Heap[$o] == call0old#AT#$Heap[$o]) && $HeapSucc(call0old#AT#$Heap, $Heap))) >>> added after: a##cached##1 := a##cached##1 && ##extracted_function##1(call0old#AT#$Heap, $Heap); -Processing command (at Snapshots0.v1.dfy(4,10)) assert {:id "id8"} Lit(false); +Processing command (at Snapshots0.v1.dfy(4,10)) assert {:id "id7"} Lit(false); >>> MarkAsPartiallyVerified Snapshots0.v1.dfy(4,9): Error: assertion might not hold diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots1.run.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots1.run.legacy.dfy.expect index 79adfe82043..6c278ab5388 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots1.run.legacy.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots1.run.legacy.dfy.expect @@ -4,7 +4,7 @@ Processing command (at Snapshots1.v0.dfy(4,10)) assert {:id "id2"} Lit(false); Dafny program verifier finished with 1 verified, 0 errors Processing call to procedure N (call postcondition) in implementation M (correctness) (at Snapshots1.v1.dfy(3,4)): >>> added after: a##cached##0 := a##cached##0 && false; -Processing command (at Snapshots1.v1.dfy(4,10)) assert {:id "id9"} Lit(false); +Processing command (at Snapshots1.v1.dfy(4,10)) assert {:id "id8"} Lit(false); >>> DoNothingToAssert Snapshots1.v1.dfy(4,9): Error: assertion might not hold diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots2.run.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots2.run.legacy.dfy.expect index b4b0df2dd7c..401acbc1f66 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots2.run.legacy.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots2.run.legacy.dfy.expect @@ -1,12 +1,12 @@ Processing command (at Snapshots2.v0.dfy(4,10)) assert {:id "id2"} Lit(false); >>> DoNothingToAssert -Processing command (at Snapshots2.v0.dfy(11,11)) assert {:id "id7"} Lit(true); +Processing command (at Snapshots2.v0.dfy(11,11)) assert {:id "id6"} Lit(true); >>> DoNothingToAssert -Processing command (at Snapshots2.v0.dfy(11,15)) assert {:id "id6"} _module.__default.P() <==> _module.__default.Q(); +Processing command (at Snapshots2.v0.dfy(11,15)) assert {:id "id5"} _module.__default.P() <==> _module.__default.Q(); >>> DoNothingToAssert -Processing command (at Snapshots2.v0.dfy(14,11)) assert {:id "id10"} Lit(true); +Processing command (at Snapshots2.v0.dfy(14,11)) assert {:id "id9"} Lit(true); >>> DoNothingToAssert -Processing command (at Snapshots2.v0.dfy(14,15)) assert {:id "id9"} _module.__default.Q() <==> Lit(_module.__default.R()); +Processing command (at Snapshots2.v0.dfy(14,15)) assert {:id "id8"} _module.__default.Q() <==> Lit(_module.__default.R()); >>> DoNothingToAssert Dafny program verifier finished with 3 verified, 0 errors @@ -16,16 +16,16 @@ Processing implementation P (well-formedness) (at Snapshots2.v1.dfy(10,11)): >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false; Processing implementation Q (well-formedness) (at Snapshots2.v1.dfy(13,11)): >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false; -Processing command (at Snapshots2.v1.dfy(4,10)) assert {:id "id15"} Lit(false); +Processing command (at Snapshots2.v1.dfy(4,10)) assert {:id "id14"} Lit(false); >>> DoNothingToAssert Snapshots2.v1.dfy(4,9): Error: assertion might not hold -Processing command (at Snapshots2.v1.dfy(11,11)) assert {:id "id20"} Lit(true); +Processing command (at Snapshots2.v1.dfy(11,11)) assert {:id "id18"} Lit(true); >>> DoNothingToAssert -Processing command (at Snapshots2.v1.dfy(11,15)) assert {:id "id19"} _module.__default.P() <==> _module.__default.Q(); +Processing command (at Snapshots2.v1.dfy(11,15)) assert {:id "id17"} _module.__default.P() <==> _module.__default.Q(); >>> DoNothingToAssert -Processing command (at Snapshots2.v1.dfy(14,11)) assert {:id "id23"} Lit(true); +Processing command (at Snapshots2.v1.dfy(14,11)) assert {:id "id21"} Lit(true); >>> DoNothingToAssert -Processing command (at Snapshots2.v1.dfy(14,15)) assert {:id "id22"} _module.__default.Q() <==> Lit(_module.__default.R()); +Processing command (at Snapshots2.v1.dfy(14,15)) assert {:id "id20"} _module.__default.Q() <==> Lit(_module.__default.R()); >>> DoNothingToAssert Dafny program verifier finished with 2 verified, 1 error diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots5.run.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots5.run.legacy.dfy.expect index 1df0bbd2479..8a6d82c8b15 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots5.run.legacy.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots5.run.legacy.dfy.expect @@ -15,13 +15,13 @@ Snapshots5.v1.dfy(13,10): Warning: Could not find a trigger for this quantifier. Snapshots5.v1.dfy(20,12): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Snapshots5.v1.dfy(22,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Snapshots5.v1.dfy(27,11): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. -Processing command (at Snapshots5.v1.dfy(10,40)) assert {:id "id14"} (forall b#1_1: bool :: b#1_1 || !b#1_1) || 0 != 0; +Processing command (at Snapshots5.v1.dfy(10,40)) assert {:id "id13"} (forall b#1_1: bool :: b#1_1 || !b#1_1) || 0 != 0; >>> MarkAsFullyVerified -Processing command (at Snapshots5.v1.dfy(13,38)) assert {:id "id17"} (forall b#1: bool :: b#1 || !b#1) || 3 != 3; +Processing command (at Snapshots5.v1.dfy(13,38)) assert {:id "id16"} (forall b#1: bool :: b#1 || !b#1) || 3 != 3; >>> MarkAsFullyVerified -Processing command (at Snapshots5.v1.dfy(20,37)) assert {:id "id18"} (exists b#3_1: bool :: Lit(true)) || 4 != 4; +Processing command (at Snapshots5.v1.dfy(20,37)) assert {:id "id17"} (exists b#3_1: bool :: Lit(true)) || 4 != 4; >>> DoNothingToAssert -Processing command (at Snapshots5.v1.dfy(22,35)) assert {:id "id19"} (exists b#3: bool :: Lit(true)) || 5 != 5; +Processing command (at Snapshots5.v1.dfy(22,35)) assert {:id "id18"} (exists b#3: bool :: Lit(true)) || 5 != 5; >>> DoNothingToAssert Dafny program verifier finished with 1 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots8.run.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots8.run.legacy.dfy.expect index 9a5c564e0d7..114c1a89a2e 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots8.run.legacy.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots8.run.legacy.dfy.expect @@ -8,35 +8,35 @@ Processing command (at Snapshots8.v0.dfy(4,8)) assert {:id "id5$id2$requires"} { Snapshots8.v0.dfy(3,11): Error: assertion might not hold Snapshots8.v0.dfy(4,7): Error: a precondition for this call could not be proved Snapshots8.v0.dfy(8,13): Related location: this is the precondition that could not be proved -Processing command (at Snapshots8.v0.dfy(13,13)) assert {:id "id11"} LitInt(2) <= z#0; +Processing command (at Snapshots8.v0.dfy(13,13)) assert {:id "id9"} LitInt(2) <= z#0; >>> DoNothingToAssert Snapshots8.v0.dfy(17,9): Error: a postcondition could not be proved on this return path Snapshots8.v0.dfy(13,12): Related location: this is the postcondition that could not be proved -Processing command (at Snapshots8.v0.dfy(23,12)) assert {:id "id13"} u#0 != 53; +Processing command (at Snapshots8.v0.dfy(23,12)) assert {:id "id11"} u#0 != 53; >>> DoNothingToAssert Snapshots8.v0.dfy(23,11): Error: assertion might not hold -Processing command (at Snapshots8.v0.dfy(28,10)) assert {:id "id14"} Lit(true); +Processing command (at Snapshots8.v0.dfy(28,10)) assert {:id "id12"} Lit(true); >>> DoNothingToAssert Dafny program verifier finished with 1 verified, 4 errors -Processing command (at Snapshots8.v1.dfy(30,17)) assert {:id "id30"} u#0 != 53; +Processing command (at Snapshots8.v1.dfy(30,17)) assert {:id "id26"} u#0 != 53; >>> RecycleError Snapshots8.v1.dfy(30,16): Error: assertion might not hold -Processing command (at Snapshots8.v1.dfy(3,15)) assert {:id "id15"} x#0 < 20 || LitInt(10) <= x#0; +Processing command (at Snapshots8.v1.dfy(3,15)) assert {:id "id13"} x#0 < 20 || LitInt(10) <= x#0; >>> MarkAsFullyVerified -Processing command (at Snapshots8.v1.dfy(5,17)) assert {:id "id16"} x#0 < 10; +Processing command (at Snapshots8.v1.dfy(5,17)) assert {:id "id14"} x#0 < 10; >>> RecycleError -Processing command (at Snapshots8.v1.dfy(6,8)) assert {:id "id21$id17$requires"} {:id "id17"} LitInt(0) <= call0formal#AT#y#0; +Processing command (at Snapshots8.v1.dfy(6,8)) assert {:id "id19$id15$requires"} {:id "id15"} LitInt(0) <= call0formal#AT#y#0; >>> RecycleError -Processing command (at Snapshots8.v1.dfy(7,12)) assert {:id "id19"} x#0 == LitInt(7); +Processing command (at Snapshots8.v1.dfy(7,12)) assert {:id "id17"} x#0 == LitInt(7); >>> DoNothingToAssert Snapshots8.v1.dfy(5,16): Error: assertion might not hold Snapshots8.v1.dfy(6,7): Error: a precondition for this call could not be proved Snapshots8.v1.dfy(12,20): Related location: this is the precondition that could not be proved Snapshots8.v1.dfy(7,11): Error: assertion might not hold -Processing command (at Snapshots8.v1.dfy(23,12)) assert {:id "id29"} Lit(true); +Processing command (at Snapshots8.v1.dfy(23,12)) assert {:id "id25"} Lit(true); >>> DoNothingToAssert -Processing command (at Snapshots8.v1.dfy(19,13)) assert {:id "id27"} LitInt(2) <= z#0; +Processing command (at Snapshots8.v1.dfy(19,13)) assert {:id "id23"} LitInt(2) <= z#0; >>> DoNothingToAssert Snapshots8.v1.dfy(24,9): Error: a postcondition could not be proved on this return path Snapshots8.v1.dfy(19,12): Related location: this is the postcondition that could not be proved diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots9.run.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots9.run.legacy.dfy.expect index dc5172019fd..36e8d43cba9 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots9.run.legacy.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots9.run.legacy.dfy.expect @@ -1,19 +1,19 @@ Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format -Processing command (at Snapshots9.v0.dfy(2,11)) assert {:id "id3"} ok#0; +Processing command (at Snapshots9.v0.dfy(2,11)) assert {:id "id2"} ok#0; >>> DoNothingToAssert Snapshots9.v0.dfy(4,7): Error: a postcondition could not be proved on this return path Snapshots9.v0.dfy(2,10): Related location: this is the postcondition that could not be proved -Processing command (at Snapshots9.v0.dfy(12,11)) assert {:id "id9"} ok#0; +Processing command (at Snapshots9.v0.dfy(12,11)) assert {:id "id7"} ok#0; >>> DoNothingToAssert Snapshots9.v0.dfy(13,0): Error: a postcondition could not be proved on this return path Snapshots9.v0.dfy(12,10): Related location: this is the postcondition that could not be proved Dafny program verifier finished with 0 verified, 2 errors -Processing command (at Snapshots9.v1.dfy(6,11)) assert {:id "id13"} ok#0; +Processing command (at Snapshots9.v1.dfy(6,11)) assert {:id "id10"} ok#0; >>> RecycleError Snapshots9.v1.dfy(8,7): Error: a postcondition could not be proved on this return path Snapshots9.v1.dfy(6,10): Related location: this is the postcondition that could not be proved -Processing command (at Snapshots9.v1.dfy(19,11)) assert {:id "id19"} ok#0; +Processing command (at Snapshots9.v1.dfy(19,11)) assert {:id "id15"} ok#0; >>> RecycleError Snapshots9.v1.dfy(21,0): Error: a postcondition could not be proved on this return path Snapshots9.v1.dfy(19,10): Related location: this is the postcondition that could not be proved diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect index efc7dd6b97d..1ba70097ea1 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect @@ -1,10 +1,10 @@ -git-issue-3855.dfy(801,0): Warning: attribute :ignore is deprecated -git-issue-3855.dfy(801,11): Error: Verification of 'Memory.dynMove' timed out after seconds -git-issue-3855.dfy(944,17): Error: a precondition for this call could not be proved +git-issue-3855.dfy(799,0): Warning: attribute :ignore is deprecated +git-issue-3855.dfy(799,11): Error: Verification of 'Memory.dynMove' timed out after seconds +git-issue-3855.dfy(942,17): Error: a precondition for this call could not be proved git-issue-3855.dfy(430,29): Related location: this is the precondition that could not be proved -git-issue-3855.dfy(944,17): Error: a precondition for this call could not be proved +git-issue-3855.dfy(942,17): Error: a precondition for this call could not be proved git-issue-3855.dfy(434,36): Related location: this is the precondition that could not be proved -git-issue-3855.dfy(1337,20): Error: a precondition for this call could not be proved +git-issue-3855.dfy(1335,20): Error: a precondition for this call could not be proved git-issue-3855.dfy(434,36): Related location: this is the precondition that could not be proved Dafny program verifier finished with 101 verified, 3 errors, 1 time out diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/triggers-prevent-some-inlining.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/triggers-prevent-some-inlining.dfy.expect index 2d3fea2d577..89c40cc572a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/triggers-prevent-some-inlining.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/triggers-prevent-some-inlining.dfy.expect @@ -3,7 +3,5 @@ triggers-prevent-some-inlining.dfy(24,10): Info: Some instances of this call are triggers-prevent-some-inlining.dfy(25,10): Info: Some instances of this call are not inlined. triggers-prevent-some-inlining.dfy(24,10): Info: Some instances of this call are not inlined. triggers-prevent-some-inlining.dfy(25,10): Info: Some instances of this call are not inlined. -triggers-prevent-some-inlining.dfy(24,10): Info: Some instances of this call are not inlined. -triggers-prevent-some-inlining.dfy(25,10): Info: Some instances of this call are not inlined. Dafny program verifier finished with 1 verified, 0 errors