From d09374c876556c0b581bc2212511c152146266e8 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 4 Oct 2024 17:32:13 +0200 Subject: [PATCH 1/3] Update Source/Directory.Build.props MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Mikaël Mayer --- Source/Directory.Build.props | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props index d68939fad..2965b7047 100644 --- a/Source/Directory.Build.props +++ b/Source/Directory.Build.props @@ -2,7 +2,7 @@ - 3.3.5 + 3.3.0 net6.0 false Boogie From 7db5dee1d2b852898bc14a39f5bb61b4e31d0a92 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 4 Oct 2024 18:13:45 +0200 Subject: [PATCH 2/3] Refactorings --- Source/Core/AST/CallCmd.cs | 2 +- Source/Core/VariableDependenceAnalyser.cs | 22 ++++++++++--------- .../Counterexample/Counterexample.cs | 2 -- Source/VCGeneration/ManualSplit.cs | 4 ++-- Source/VCGeneration/Splits/BlockRewriter.cs | 10 +++++++-- .../Splits/FocusAttributeHandler.cs | 4 ++-- .../IsolateAttributeOnAssertsHandler.cs | 18 +++------------ .../Splits/IsolateAttributeOnJumpsHandler.cs | 19 +++------------- .../VCGeneration/Splits/ManualSplitFinder.cs | 4 ++-- Source/VCGeneration/Splits/PathToken.cs | 4 ++-- Source/VCGeneration/Splits/Split.cs | 2 +- .../Splits/SplitAttributeHandler.cs | 6 ++--- .../VerificationConditionGenerator.cs | 10 ++++----- 13 files changed, 44 insertions(+), 63 deletions(-) diff --git a/Source/Core/AST/CallCmd.cs b/Source/Core/AST/CallCmd.cs index d39768d22..f20360987 100644 --- a/Source/Core/AST/CallCmd.cs +++ b/Source/Core/AST/CallCmd.cs @@ -882,7 +882,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options) // Do this after copying the attributes so it doesn't get overwritten if (callId is not null) { - (a as ICarriesAttributes).CopyIdWithModificationsFrom(tok, req, + a.CopyIdWithModificationsFrom(tok, req, id => new TrackedCallRequiresGoal(callId, id)); } diff --git a/Source/Core/VariableDependenceAnalyser.cs b/Source/Core/VariableDependenceAnalyser.cs index 09fba1808..46df39226 100644 --- a/Source/Core/VariableDependenceAnalyser.cs +++ b/Source/Core/VariableDependenceAnalyser.cs @@ -533,22 +533,24 @@ private Dictionary> ComputeGlobalControlDependences() Graph callGraph = Program.BuildCallGraph(options, prog); // Add inter-procedural control dependence nodes based on calls - foreach (var Impl in prog.NonInlinedImplementations()) + foreach (var impl in prog.NonInlinedImplementations()) { - foreach (var b in Impl.Blocks) + foreach (var b in impl.Blocks) { foreach (var cmd in b.Cmds.OfType()) { - var DirectCallee = GetImplementation(cmd.callee); - if (DirectCallee != null) + var directCallee = GetImplementation(cmd.callee); + if (directCallee == null) + { + continue; + } + + var indirectCallees = ComputeIndirectCallees(callGraph, directCallee); + foreach (var control in GetControllingBlocks(b, localCtrlDeps[impl])) { - HashSet IndirectCallees = ComputeIndirectCallees(callGraph, DirectCallee); - foreach (var control in GetControllingBlocks(b, localCtrlDeps[Impl])) + foreach (var c in indirectCallees.Select(item => item.Blocks).SelectMany(Item => Item)) { - foreach (var c in IndirectCallees.Select(Item => Item.Blocks).SelectMany(Item => Item)) - { - globalCtrlDep[control].Add(c); - } + globalCtrlDep[control].Add(c); } } } diff --git a/Source/VCGeneration/Counterexample/Counterexample.cs b/Source/VCGeneration/Counterexample/Counterexample.cs index 6f7997e68..15d4cab2b 100644 --- a/Source/VCGeneration/Counterexample/Counterexample.cs +++ b/Source/VCGeneration/Counterexample/Counterexample.cs @@ -124,8 +124,6 @@ public void Print(int indent, TextWriter tw, Action blockAction = null) } else { // for ErrorTrace == 1 restrict the output; - // do not print tokens with -17:-4 as their location because they have been - // introduced in the translation and do not give any useful feedback to the user if (Options.ErrorTrace == 1 && block.tok == Token.NoToken) { continue; } diff --git a/Source/VCGeneration/ManualSplit.cs b/Source/VCGeneration/ManualSplit.cs index 95b555c6e..5b47299b7 100644 --- a/Source/VCGeneration/ManualSplit.cs +++ b/Source/VCGeneration/ManualSplit.cs @@ -8,13 +8,13 @@ namespace VC; public class ManualSplit : Split { - public ImplementationPartOrigin Token { get; } + public IImplementationPartOrigin Token { get; } public ManualSplit(VCGenOptions options, Func> blocks, VerificationConditionGenerator parent, ImplementationRun run, - ImplementationPartOrigin origin, int? randomSeed = null) + IImplementationPartOrigin origin, int? randomSeed = null) : base(options, blocks, parent, run, randomSeed) { Token = origin; diff --git a/Source/VCGeneration/Splits/BlockRewriter.cs b/Source/VCGeneration/Splits/BlockRewriter.cs index 2f0159d96..dc93dab28 100644 --- a/Source/VCGeneration/Splits/BlockRewriter.cs +++ b/Source/VCGeneration/Splits/BlockRewriter.cs @@ -15,10 +15,10 @@ public class BlockRewriter { public List OrderedBlocks { get; } public VCGenOptions Options { get; } public Graph Dag { get; } - public Func, ManualSplit> CreateSplit { get; } + public Func, ManualSplit> CreateSplit { get; } public BlockRewriter(VCGenOptions options, List blocks, - Func, ManualSplit> createSplit) { + Func, ManualSplit> createSplit) { this.Options = options; CreateSplit = createSplit; Dag = Program.GraphFromBlocks(blocks); @@ -127,4 +127,10 @@ public IEnumerable GetSplitsForIsolatedPaths(Block lastBlock, IRead BlockTransformations.DeleteBlocksNotLeadingToAssertions(newBlocks); return (newBlocks, oldToNewBlockMap); } + + + public static bool ShouldIsolate(bool splitOnEveryAssert, QKeyValue? isolateAttribute) + { + return splitOnEveryAssert || isolateAttribute != null; + } } \ No newline at end of file diff --git a/Source/VCGeneration/Splits/FocusAttributeHandler.cs b/Source/VCGeneration/Splits/FocusAttributeHandler.cs index 197bc1fe1..b9d327250 100644 --- a/Source/VCGeneration/Splits/FocusAttributeHandler.cs +++ b/Source/VCGeneration/Splits/FocusAttributeHandler.cs @@ -19,7 +19,7 @@ public class FocusAttributeHandler { /// We recurse twice for each focus, leading to potentially 2^N splits /// public static List GetParts(VCGenOptions options, ImplementationRun run, - Func, ManualSplit> createPart) + Func, ManualSplit> createPart) { var rewriter = new BlockRewriter(options, run.Implementation.Blocks, createPart); @@ -53,7 +53,7 @@ void AddSplitsFromIndex(ImmutableStack path, int focusIndex, ISet var allFocusBlocksHaveBeenProcessed = focusIndex == focusBlocks.Count; if (allFocusBlocksHaveBeenProcessed) { var (newBlocks, _) = rewriter.ComputeNewBlocks(blocksToInclude, freeAssumeBlocks); - ImplementationPartOrigin token = path.Any() + IImplementationPartOrigin token = path.Any() ? new PathOrigin(run.Implementation.tok, path.ToList()) // TODO fix : new ImplementationRootOrigin(run.Implementation); result.Add(rewriter.CreateSplit(token, newBlocks)); diff --git a/Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs b/Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs index 8950159f8..1d90a36e0 100644 --- a/Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs +++ b/Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs @@ -12,7 +12,7 @@ namespace VCGeneration; class IsolateAttributeOnAssertsHandler { public static (List IsolatedParts, ManualSplit Remainder) GetParts(VCGenOptions options, ManualSplit partToDivide, - Func, ManualSplit> createPart) { + Func, ManualSplit> createPart) { var rewriter = new BlockRewriter(options, partToDivide.Blocks, createPart); var splitOnEveryAssert = partToDivide.Options.VcsSplitOnEveryAssert; @@ -29,7 +29,7 @@ public static (List IsolatedParts, ManualSplit Remainder) GetParts( foreach (var assert in block.Cmds.OfType()) { var attributes = assert.Attributes; var isolateAttribute = QKeyValue.FindAttribute(attributes, p => p.Key == "isolate"); - if (!ShouldIsolate(splitOnEveryAssert, isolateAttribute)) { + if (!BlockRewriter.ShouldIsolate(splitOnEveryAssert, isolateAttribute)) { continue; } @@ -92,22 +92,10 @@ List GetCommands(Block block) => block.Cmds.Select(cmd => isolatedAssertions.Contains(cmd) ? rewriter.TransformAssertCmd(cmd) : cmd).ToList(); } } - - private static bool ShouldIsolate(bool splitOnEveryAssert, QKeyValue? isolateAttribute) { - if (splitOnEveryAssert) { - if (isolateAttribute == null) { - return true; - } - - return !isolateAttribute.Params.OfType().Any(p => Equals(p, "none")); - } - - return isolateAttribute != null; - } } -public class IsolatedAssertionOrigin : TokenWrapper, ImplementationPartOrigin { +public class IsolatedAssertionOrigin : TokenWrapper, IImplementationPartOrigin { public AssertCmd IsolatedAssert { get; } public IsolatedAssertionOrigin(AssertCmd isolatedAssert) : base(isolatedAssert.tok) { diff --git a/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs b/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs index a35e8f2b9..5f7c1de04 100644 --- a/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs +++ b/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs @@ -13,7 +13,7 @@ namespace VCGeneration; class IsolateAttributeOnJumpsHandler { public static (List Isolated, ManualSplit Remainder) GetParts(VCGenOptions options, ManualSplit partToDivide, - Func, ManualSplit> createPart) { + Func, ManualSplit> createPart) { var rewriter = new BlockRewriter(options, partToDivide.Blocks, createPart); @@ -33,7 +33,7 @@ public static (List Isolated, ManualSplit Remainder) GetParts(VCGen var isTypeOfAssert = gotoCmd.tok is GotoFromReturn; var isolateAttribute = QKeyValue.FindAttribute(gotoCmd.Attributes, p => p.Key == "isolate"); - var isolate = ShouldIsolate(isTypeOfAssert && splitOnEveryAssert, isolateAttribute); + var isolate = BlockRewriter.ShouldIsolate(isTypeOfAssert && splitOnEveryAssert, isolateAttribute); if (!isolate) { continue; } @@ -62,7 +62,6 @@ public static (List Isolated, ManualSplit Remainder) GetParts(VCGen return (results, GetPartWithoutIsolatedReturns()); ManualSplit GetPartWithoutIsolatedReturns() { - // TODO this needs an extra test. In case the isolated jump is followed by something it dominates var (newBlocks, mapping) = rewriter.ComputeNewBlocks(blocks.ToHashSet(), new HashSet()); foreach (var (oldBlock, newBlock) in mapping) { if (isolatedBlocks.Contains(oldBlock)) { @@ -74,22 +73,10 @@ ManualSplit GetPartWithoutIsolatedReturns() { newBlocks); } } - - private static bool ShouldIsolate(bool splitOnEveryAssert, QKeyValue? isolateAttribute) { - if (splitOnEveryAssert) { - if (isolateAttribute == null) { - return true; - } - - return !isolateAttribute.Params.OfType().Any(p => Equals(p, "none")); - } - - return isolateAttribute != null; - } } -public class ReturnOrigin : TokenWrapper, ImplementationPartOrigin { +public class ReturnOrigin : TokenWrapper, IImplementationPartOrigin { public ReturnCmd IsolatedReturn { get; } public ReturnOrigin(ReturnCmd isolatedReturn) : base(isolatedReturn.tok) { diff --git a/Source/VCGeneration/Splits/ManualSplitFinder.cs b/Source/VCGeneration/Splits/ManualSplitFinder.cs index 4be4db4fa..4b553b055 100644 --- a/Source/VCGeneration/Splits/ManualSplitFinder.cs +++ b/Source/VCGeneration/Splits/ManualSplitFinder.cs @@ -11,7 +11,7 @@ namespace VCGeneration; public static class ManualSplitFinder { public static IEnumerable GetParts(VCGenOptions options, ImplementationRun run, - Func, ManualSplit> createPart) { + Func, ManualSplit> createPart) { var focussedParts = FocusAttributeHandler.GetParts(options, run, createPart); var result = focussedParts.SelectMany(focussedPart => { @@ -27,6 +27,6 @@ public static IEnumerable GetParts(VCGenOptions options, Implementa } } -public interface ImplementationPartOrigin : IToken { +public interface IImplementationPartOrigin : IToken { string ShortName { get; } } \ No newline at end of file diff --git a/Source/VCGeneration/Splits/PathToken.cs b/Source/VCGeneration/Splits/PathToken.cs index 825176b8b..b0dabe1cd 100644 --- a/Source/VCGeneration/Splits/PathToken.cs +++ b/Source/VCGeneration/Splits/PathToken.cs @@ -8,7 +8,7 @@ namespace VCGeneration; -public class PathOrigin : TokenWrapper, ImplementationPartOrigin { +public class PathOrigin : TokenWrapper, IImplementationPartOrigin { public PathOrigin(IToken inner, List branches) : base(inner) { Branches = branches; @@ -18,7 +18,7 @@ public PathOrigin(IToken inner, List branches) : base(inner) { public string ShortName => $"/assert@{line}[{string.Join(",", Branches.Select(b => b.tok.line))}]"; } -class ImplementationRootOrigin : TokenWrapper, ImplementationPartOrigin { +class ImplementationRootOrigin : TokenWrapper, IImplementationPartOrigin { public ImplementationRootOrigin(Implementation implementation) : base(implementation.tok) { } diff --git a/Source/VCGeneration/Splits/Split.cs b/Source/VCGeneration/Splits/Split.cs index c4d33efd6..5d31404f0 100644 --- a/Source/VCGeneration/Splits/Split.cs +++ b/Source/VCGeneration/Splits/Split.cs @@ -98,7 +98,7 @@ private void PrintSplit() { Thread.Sleep(100); } - var prefix = (this is ManualSplit manualSplit) ? manualSplit.Token.ShortName : ""; + var prefix = this is ManualSplit manualSplit ? manualSplit.Token.ShortName : ""; var name = Implementation.Name + prefix; using var writer = printToConsole ? new TokenTextWriter("", Options.OutputWriter, false, Options.PrettyPrint, Options) diff --git a/Source/VCGeneration/Splits/SplitAttributeHandler.cs b/Source/VCGeneration/Splits/SplitAttributeHandler.cs index 85bcc73a8..4e145da9d 100644 --- a/Source/VCGeneration/Splits/SplitAttributeHandler.cs +++ b/Source/VCGeneration/Splits/SplitAttributeHandler.cs @@ -61,7 +61,7 @@ public static List GetParts(ManualSplit partToSplit) { } return vcs; - ManualSplit CreateVc(ImplementationPartOrigin token, List blocks) { + ManualSplit CreateVc(IImplementationPartOrigin token, List blocks) { return new ManualSplit(partToSplit.Options, () => { BlockTransformations.Optimize(blocks); return blocks; @@ -108,7 +108,7 @@ private static bool ShouldSplitHere(Cmd c) { return blockAssignments; } - private static ManualSplit? GetImplementationPartAfterSplit(Func, ManualSplit> createVc, + private static ManualSplit? GetImplementationPartAfterSplit(Func, ManualSplit> createVc, ManualSplit partToSplit, Dictionary blockStartToSplit, Block blockWithSplit, HashSet splits, Cmd? split) @@ -207,7 +207,7 @@ private static void AddJumpsToNewBlocks(Dictionary oldToNewBlockMa } } -class SplitOrigin : TokenWrapper, ImplementationPartOrigin { +class SplitOrigin : TokenWrapper, IImplementationPartOrigin { public SplitOrigin(IToken inner) : base(inner) { } diff --git a/Source/VCGeneration/VerificationConditionGenerator.cs b/Source/VCGeneration/VerificationConditionGenerator.cs index 315a6b047..9187d39c8 100644 --- a/Source/VCGeneration/VerificationConditionGenerator.cs +++ b/Source/VCGeneration/VerificationConditionGenerator.cs @@ -1351,22 +1351,22 @@ public static Counterexample AssertCmdToCounterexample(VCGenOptions options, Ass /// /// Returns a clone of "cex", but with the location stored in "cex" replaced by those from "assrt". /// - public static Counterexample AssertCmdToCloneCounterexample(VCGenOptions options, AssertCmd assrt, + public static Counterexample AssertCmdToCloneCounterexample(VCGenOptions options, AssertCmd assert, Counterexample cex, Block implEntryBlock) { - Contract.Requires(assrt != null); + Contract.Requires(assert != null); Contract.Requires(cex != null); Contract.Requires(implEntryBlock != null); Contract.Ensures(Contract.Result() != null); Counterexample cc; - if (assrt is AssertRequiresCmd assertRequiresCmd) + if (assert is AssertRequiresCmd assertRequiresCmd) { cc = new CallCounterexample(options, cex.Trace, cex.AugmentedTrace, assertRequiresCmd, cex.Model, cex.MvInfo, cex.Context, cex.ProofRun, assertRequiresCmd.Checksum); } - else if (assrt is AssertEnsuresCmd assertEnsuresCmd && cex is ReturnCounterexample returnCounterexample) + else if (assert is AssertEnsuresCmd assertEnsuresCmd && cex is ReturnCounterexample returnCounterexample) { // The first three parameters of ReturnCounterexample are: List trace, List augmentedTrace, TransferCmd failingReturn, Ensures failingEnsures. // We have the "aa" version of failingEnsures, namely aa.Ensures. The first and third parameters take more work to reconstruct. @@ -1450,7 +1450,7 @@ public static Counterexample AssertCmdToCloneCounterexample(VCGenOptions options } else { - cc = new AssertCounterexample(options, cex.Trace, cex.AugmentedTrace, assrt, cex.Model, cex.MvInfo, cex.Context, + cc = new AssertCounterexample(options, cex.Trace, cex.AugmentedTrace, assert, cex.Model, cex.MvInfo, cex.Context, cex.ProofRun); } From 6bff2ff417bf946dc070b47365c18f9e87ab187e Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Sun, 6 Oct 2024 14:59:18 +0200 Subject: [PATCH 3/3] Undo civl test changes --- Source/Concurrency/CivlUtil.cs | 6 ++++-- Source/Core/Token.cs | 3 +-- Test/civl/regression-tests/intro-nonblocking.bpl.expect | 1 + Test/civl/regression-tests/left-mover.bpl.expect | 1 + Test/civl/regression-tests/non-interference-1.bpl.expect | 1 + Test/civl/regression-tests/non-interference-2.bpl.expect | 2 ++ .../regression-tests/pa-noninterference-check.bpl.expect | 1 + Test/civl/regression-tests/parallel1.bpl.expect | 1 + Test/civl/regression-tests/parallel6.bpl.expect | 1 + Test/civl/regression-tests/pending-async-1.bpl.expect | 1 + .../pending-async-noninterference-fail.bpl.expect | 1 + Test/civl/regression-tests/refinement.bpl.expect | 5 +++++ Test/civl/regression-tests/refinement2.bpl.expect | 4 ++++ Test/civl/regression-tests/yield-invariant-fails.bpl.expect | 1 + 14 files changed, 25 insertions(+), 4 deletions(-) diff --git a/Source/Concurrency/CivlUtil.cs b/Source/Concurrency/CivlUtil.cs index ac48c1164..49ee3003c 100644 --- a/Source/Concurrency/CivlUtil.cs +++ b/Source/Concurrency/CivlUtil.cs @@ -307,14 +307,16 @@ public static HavocCmd HavocCmd(params IdentifierExpr[] vars) public static class BlockHelper { + public static readonly IToken /*!*/ ReportedNoToken = new Token(); + public static Block Block(string label, List cmds) { - return new Block(Token.NoToken, label, cmds, CmdHelper.ReturnCmd); + return new Block(ReportedNoToken, label, cmds, CmdHelper.ReturnCmd); } public static Block Block(string label, List cmds, List gotoTargets) { - return new Block(Token.NoToken, label, cmds, new GotoCmd(Token.NoToken, gotoTargets)); + return new Block(ReportedNoToken, label, cmds, new GotoCmd(Token.NoToken, gotoTargets)); } } diff --git a/Source/Core/Token.cs b/Source/Core/Token.cs index 5f7a1bb1f..27a0dd156 100644 --- a/Source/Core/Token.cs +++ b/Source/Core/Token.cs @@ -33,8 +33,7 @@ public string /*!*/ public Token next; // ML 2005-03-11 Tokens are kept in linked list - public static readonly IToken /*!*/ - NoToken = new Token(); + public static readonly IToken /*!*/ NoToken = new Token(); public Token() { diff --git a/Test/civl/regression-tests/intro-nonblocking.bpl.expect b/Test/civl/regression-tests/intro-nonblocking.bpl.expect index 08c401b27..1a747e1d9 100644 --- a/Test/civl/regression-tests/intro-nonblocking.bpl.expect +++ b/Test/civl/regression-tests/intro-nonblocking.bpl.expect @@ -1,4 +1,5 @@ intro-nonblocking.bpl(4,13): Error: Cooperation check for intro failed Execution trace: + (0,0): init Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/civl/regression-tests/left-mover.bpl.expect b/Test/civl/regression-tests/left-mover.bpl.expect index 383a2cd10..44ada71cb 100644 --- a/Test/civl/regression-tests/left-mover.bpl.expect +++ b/Test/civl/regression-tests/left-mover.bpl.expect @@ -10,5 +10,6 @@ Execution trace: left-mover.bpl(6,24): inline$inc$0$Return left-mover.bpl(26,24): Error: Cooperation check for block failed Execution trace: + (0,0): init Boogie program verifier finished with 3 verified, 3 errors diff --git a/Test/civl/regression-tests/non-interference-1.bpl.expect b/Test/civl/regression-tests/non-interference-1.bpl.expect index be24ba16a..9ed2f19b1 100644 --- a/Test/civl/regression-tests/non-interference-1.bpl.expect +++ b/Test/civl/regression-tests/non-interference-1.bpl.expect @@ -2,5 +2,6 @@ non-interference-1.bpl(25,1): Error: Non-interference check failed Execution trace: non-interference-1.bpl(7,3): anon0 non-interference-1.bpl(12,5): inline$AtomicIncr$0$anon0 + (0,0): inline$Civl_NoninterferenceChecker_yield_Yield$0$L Boogie program verifier finished with 4 verified, 1 error diff --git a/Test/civl/regression-tests/non-interference-2.bpl.expect b/Test/civl/regression-tests/non-interference-2.bpl.expect index 4bbae5629..c1176c36d 100644 --- a/Test/civl/regression-tests/non-interference-2.bpl.expect +++ b/Test/civl/regression-tests/non-interference-2.bpl.expect @@ -2,8 +2,10 @@ non-interference-2.bpl(25,1): Error: Non-interference check failed Execution trace: non-interference-2.bpl(7,3): anon0 non-interference-2.bpl(12,5): inline$AtomicIncr$0$anon0 + (0,0): inline$Civl_NoninterferenceChecker_yield_PC$0$L non-interference-2.bpl(25,1): Error: Non-interference check failed Execution trace: non-interference-2.bpl(34,3): anon0 + (0,0): inline$Civl_NoninterferenceChecker_yield_PC$0$L Boogie program verifier finished with 2 verified, 2 errors diff --git a/Test/civl/regression-tests/pa-noninterference-check.bpl.expect b/Test/civl/regression-tests/pa-noninterference-check.bpl.expect index 55715916a..b97bf307f 100644 --- a/Test/civl/regression-tests/pa-noninterference-check.bpl.expect +++ b/Test/civl/regression-tests/pa-noninterference-check.bpl.expect @@ -1,5 +1,6 @@ pa-noninterference-check.bpl(26,1): Error: Non-interference check failed Execution trace: + (0,0): init pa-noninterference-check.bpl(19,7): inline$A_Incr$0$anon0 pa-noninterference-check.bpl(16,34): inline$A_Incr$0$Return diff --git a/Test/civl/regression-tests/parallel1.bpl.expect b/Test/civl/regression-tests/parallel1.bpl.expect index 0bc33ffe1..4b52e2854 100644 --- a/Test/civl/regression-tests/parallel1.bpl.expect +++ b/Test/civl/regression-tests/parallel1.bpl.expect @@ -2,5 +2,6 @@ parallel1.bpl(25,1): Error: Non-interference check failed Execution trace: parallel1.bpl(7,3): anon0 parallel1.bpl(12,5): inline$AtomicIncr$0$anon0 + (0,0): inline$Civl_NoninterferenceChecker_yield_Yield$0$L Boogie program verifier finished with 3 verified, 1 error diff --git a/Test/civl/regression-tests/parallel6.bpl.expect b/Test/civl/regression-tests/parallel6.bpl.expect index 9a6a6e2be..0ff7beb24 100644 --- a/Test/civl/regression-tests/parallel6.bpl.expect +++ b/Test/civl/regression-tests/parallel6.bpl.expect @@ -7,5 +7,6 @@ Execution trace: parallel6.bpl(11,5): anon0_0 parallel6.bpl(30,7): inline$atomic_incr$2$anon0 parallel6.bpl(30,7): inline$atomic_incr$3$anon0 + (0,0): Civl_ReturnChecker Boogie program verifier finished with 7 verified, 1 error diff --git a/Test/civl/regression-tests/pending-async-1.bpl.expect b/Test/civl/regression-tests/pending-async-1.bpl.expect index 5e0a35e06..86c6fbf94 100644 --- a/Test/civl/regression-tests/pending-async-1.bpl.expect +++ b/Test/civl/regression-tests/pending-async-1.bpl.expect @@ -5,6 +5,7 @@ Execution trace: pending-async-1.bpl(51,3): anon0$1 pending-async-1.bpl(11,9): inline$B$1$anon0 pending-async-1.bpl(51,3): anon0$2 + (0,0): Civl_ReturnChecker pending-async-1.bpl(67,3): Error: Pending asyncs to action A created by this call are not summarized Execution trace: pending-async-1.bpl(67,3): anon0 diff --git a/Test/civl/regression-tests/pending-async-noninterference-fail.bpl.expect b/Test/civl/regression-tests/pending-async-noninterference-fail.bpl.expect index d6951c016..29a3c680e 100644 --- a/Test/civl/regression-tests/pending-async-noninterference-fail.bpl.expect +++ b/Test/civl/regression-tests/pending-async-noninterference-fail.bpl.expect @@ -1,5 +1,6 @@ pending-async-noninterference-fail.bpl(7,1): Error: Non-interference check failed Execution trace: + (0,0): init pending-async-noninterference-fail.bpl(12,5): inline$A$0$anon0 pending-async-noninterference-fail.bpl(9,32): inline$A$0$Return diff --git a/Test/civl/regression-tests/refinement.bpl.expect b/Test/civl/regression-tests/refinement.bpl.expect index 7203ec2a4..4974958b5 100644 --- a/Test/civl/regression-tests/refinement.bpl.expect +++ b/Test/civl/regression-tests/refinement.bpl.expect @@ -5,11 +5,13 @@ Execution trace: refinement.bpl(10,3): anon0$1 refinement.bpl(10,3): anon0_0 refinement.bpl(58,5): inline$INCR$1$anon0 + (0,0): Civl_ReturnChecker refinement.bpl(15,28): Error: A yield-to-yield fragment modifies layer-2 state in a way that does not match the refined atomic action Execution trace: refinement.bpl(18,3): anon0 refinement.bpl(64,5): inline$DECR$0$anon0 refinement.bpl(18,3): anon0$1 + (0,0): Civl_RefinementChecker refinement.bpl(15,28): Error: A yield-to-yield fragment modifies layer-2 state subsequent to a yield-to-yield fragment that already modified layer-2 state Execution trace: refinement.bpl(18,3): anon0 @@ -17,9 +19,11 @@ Execution trace: refinement.bpl(18,3): anon0$1 refinement.bpl(18,3): anon0_0 refinement.bpl(58,5): inline$INCR$0$anon0 + (0,0): Civl_ReturnChecker refinement.bpl(37,28): Error: On some path no yield-to-yield fragment matched the refined atomic action Execution trace: refinement.bpl(41,1): anon0 + (0,0): Civl_ReturnChecker refinement.bpl(43,28): Error: A yield-to-yield fragment illegally modifies layer-2 globals Execution trace: refinement.bpl(46,3): anon0 @@ -28,5 +32,6 @@ Execution trace: refinement.bpl(46,3): anon0_0 refinement.bpl(48,3): anon2_LoopHead refinement.bpl(58,5): inline$INCR$1$anon0 + (0,0): Civl_UnchangedChecker Boogie program verifier finished with 3 verified, 5 errors diff --git a/Test/civl/regression-tests/refinement2.bpl.expect b/Test/civl/regression-tests/refinement2.bpl.expect index 24cb32f73..3005f0993 100644 --- a/Test/civl/regression-tests/refinement2.bpl.expect +++ b/Test/civl/regression-tests/refinement2.bpl.expect @@ -1,11 +1,15 @@ refinement2.bpl(13,28): Error: On some path no yield-to-yield fragment matched the refined atomic action Execution trace: refinement2.bpl(16,5): anon0 + (0,0): Civl_call_refinement_4 refinement2.bpl(27,28): inline$atomic_nop$0$Return + (0,0): Civl_ReturnChecker refinement2.bpl(13,28): Error: A yield-to-yield fragment illegally modifies layer-2 globals Execution trace: refinement2.bpl(16,5): anon0 + (0,0): Civl_call_refinement_3 refinement2.bpl(22,7): inline$atomic_incr$0$anon0 refinement2.bpl(19,28): inline$atomic_incr$0$Return + (0,0): Civl_UnchangedChecker Boogie program verifier finished with 1 verified, 2 errors diff --git a/Test/civl/regression-tests/yield-invariant-fails.bpl.expect b/Test/civl/regression-tests/yield-invariant-fails.bpl.expect index 8bab02145..093836a59 100644 --- a/Test/civl/regression-tests/yield-invariant-fails.bpl.expect +++ b/Test/civl/regression-tests/yield-invariant-fails.bpl.expect @@ -2,5 +2,6 @@ yield-invariant-fails.bpl(7,1): Error: Non-interference check failed Execution trace: yield-invariant-fails.bpl(11,5): anon0 yield-invariant-fails.bpl(19,7): inline$atomic_A$0$anon0 + (0,0): inline$Civl_NoninterferenceChecker_yield_Inv$0$L Boogie program verifier finished with 0 verified, 1 error