diff options
| author |  Valentin Wüstholz <wuestholz@gmail.com> | 2015-06-12 08:28:07 +0200 |
|---|---|---|
| committer | Valentin Wüstholz <wuestholz@gmail.com> | 2015-06-12 08:28:52 +0200 |
| commit | 2920db784b61f02b6d68e249bc3b1c6d1cf26efd (patch) | |
| tree | 5d145b7a16625e2638b2c813a5c4b3b716715d65 /Source/Core | |
| parent | 0658816bbe2ea4be8785b52958a65b55c6a845a5 (diff) | |
Fix issue with computation of statement checksums for lambda expressions.
Diffstat (limited to 'Source/Core')
| -rw-r--r-- | Source/Core/Absy.cs | 2 | ||||
| -rw-r--r-- | Source/Core/AbsyExpr.cs | 10 | ||||
| -rw-r--r-- | Source/Core/LambdaHelper.cs | 1 |
3 files changed, 12 insertions, 1 deletions
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<Variable> args, Variable result)
: this(tok, name, new List<TypeVariable>(), 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<Expr> 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
|