From 2920db784b61f02b6d68e249bc3b1c6d1cf26efd Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Fri, 12 Jun 2015 08:28:07 +0200 Subject: Fix issue with computation of statement checksums for lambda expressions. --- Source/Core/Absy.cs | 2 ++ Source/Core/AbsyExpr.cs | 10 +++++++++- Source/Core/LambdaHelper.cs | 1 + Test/snapshots/Snapshots37.v0.bpl | 9 +++++++++ Test/snapshots/Snapshots37.v1.bpl | 9 +++++++++ Test/snapshots/runtest.snapshot | 2 +- Test/snapshots/runtest.snapshot.expect | 9 +++++++++ 7 files changed, 40 insertions(+), 2 deletions(-) create mode 100644 Test/snapshots/Snapshots37.v0.bpl create mode 100644 Test/snapshots/Snapshots37.v1.bpl diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 56bfc90f..0fedcd44 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2630,6 +2630,8 @@ namespace Microsoft.Boogie { private bool neverTrigger; private bool neverTriggerComputed; + public string OriginalLambdaExprAsString; + public Function(IToken tok, string name, List args, Variable result) : this(tok, name, new List(), args, result, null) { Contract.Requires(result != null); diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index c19140d7..c816d7f2 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -1983,7 +1983,15 @@ namespace Microsoft.Boogie { virtual public void Emit(IList args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { //Contract.Requires(stream != null); //Contract.Requires(args != null); - this.name.Emit(stream, 0xF0, false); + + if (stream.UseForComputingChecksums && Func.OriginalLambdaExprAsString != null) + { + stream.Write(Func.OriginalLambdaExprAsString); + } + else + { + this.name.Emit(stream, 0xF0, false); + } if (stream.UseForComputingChecksums) { var c = Func.DependencyChecksum; diff --git a/Source/Core/LambdaHelper.cs b/Source/Core/LambdaHelper.cs index 0d115777..a2b0f143 100644 --- a/Source/Core/LambdaHelper.cs +++ b/Source/Core/LambdaHelper.cs @@ -176,6 +176,7 @@ namespace Microsoft.Boogie { } Function fn = new Function(tok, FreshLambdaFunctionName(), freshTypeVars, formals, res, "auto-generated lambda function", Substituter.Apply(Substituter.SubstitutionFromHashtable(substFnAttrs), lambdaAttrs)); + fn.OriginalLambdaExprAsString = lam_str; fcall = new FunctionCall(new IdentifierExpr(tok, fn.Name)); fcall.Func = fn; // resolve here diff --git a/Test/snapshots/Snapshots37.v0.bpl b/Test/snapshots/Snapshots37.v0.bpl new file mode 100644 index 00000000..f32b5c90 --- /dev/null +++ b/Test/snapshots/Snapshots37.v0.bpl @@ -0,0 +1,9 @@ +procedure {:checksum "0"} P(b: bool); + +implementation {:id "P"} {:checksum "1"} P(p: bool) +{ + var l: [int]bool; + + l := (lambda n: int :: true); + assert l[0]; +} diff --git a/Test/snapshots/Snapshots37.v1.bpl b/Test/snapshots/Snapshots37.v1.bpl new file mode 100644 index 00000000..689d2533 --- /dev/null +++ b/Test/snapshots/Snapshots37.v1.bpl @@ -0,0 +1,9 @@ +procedure {:checksum "0"} P(b: bool); + +implementation {:id "P"} {:checksum "2"} P(p: bool) +{ + var l: [int]bool; + + l := (lambda n: int :: false); + assert l[0]; +} diff --git a/Test/snapshots/runtest.snapshot b/Test/snapshots/runtest.snapshot index 608ac2d2..60b101aa 100644 --- a/Test/snapshots/runtest.snapshot +++ b/Test/snapshots/runtest.snapshot @@ -1,2 +1,2 @@ -// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately -noinfer Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl Snapshots21.bpl Snapshots22.bpl Snapshots23.bpl Snapshots24.bpl Snapshots25.bpl Snapshots26.bpl Snapshots27.bpl Snapshots28.bpl Snapshots30.bpl Snapshots31.bpl Snapshots32.bpl Snapshots33.bpl Snapshots34.bpl Snapshots35.bpl Snapshots36.bpl > "%t" +// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately -noinfer Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl Snapshots21.bpl Snapshots22.bpl Snapshots23.bpl Snapshots24.bpl Snapshots25.bpl Snapshots26.bpl Snapshots27.bpl Snapshots28.bpl Snapshots30.bpl Snapshots31.bpl Snapshots32.bpl Snapshots33.bpl Snapshots34.bpl Snapshots35.bpl Snapshots36.bpl Snapshots37.bpl > "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect index 44ed6a3b..bc96cc97 100644 --- a/Test/snapshots/runtest.snapshot.expect +++ b/Test/snapshots/runtest.snapshot.expect @@ -657,3 +657,12 @@ Processing command (at Snapshots36.v1.bpl(13,5)) assert l[0]; Snapshots36.v1.bpl(13,5): Error BP5001: This assertion might not hold. Boogie program verifier finished with 0 verified, 1 error +Processing command (at Snapshots37.v0.bpl(8,5)) assert l[0]; + >>> DoNothingToAssert + +Boogie program verifier finished with 1 verified, 0 errors +Processing command (at Snapshots37.v1.bpl(8,5)) assert l[0]; + >>> DoNothingToAssert +Snapshots37.v1.bpl(8,5): Error BP5001: This assertion might not hold. + +Boogie program verifier finished with 0 verified, 1 error -- cgit v1.2.3