diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Core/LambdaHelper.ssc | 17 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.ssc | 20 |
2 files changed, 37 insertions, 0 deletions
diff --git a/Source/Core/LambdaHelper.ssc b/Source/Core/LambdaHelper.ssc index 218379b0..716ea7ae 100644 --- a/Source/Core/LambdaHelper.ssc +++ b/Source/Core/LambdaHelper.ssc @@ -41,6 +41,23 @@ namespace Microsoft.Boogie { internal List<Function!>! lambdaFunctions = new List<Function!>();
static int lambdaid = 0;
+ public override Program! VisitProgram(Program! prog)
+ {
+ foreach (Declaration! decl in prog.TopLevelDeclarations) {
+ if (decl is Axiom) {
+ this.Visit(decl);
+ }
+ }
+
+ return prog;
+ }
+
+ public override Procedure! VisitProcedure(Procedure! node)
+ {
+ // do not visit requires/ensures when calling this on Implementation
+ return node;
+ }
+
public override Absy! Visit(Absy! node)
{
node = base.Visit(node);
diff --git a/Source/VCGeneration/VC.ssc b/Source/VCGeneration/VC.ssc index 7f890826..5c844953 100644 --- a/Source/VCGeneration/VC.ssc +++ b/Source/VCGeneration/VC.ssc @@ -1778,6 +1778,26 @@ namespace VC }
#endregion Peep-hole optimizations
+ if (CommandLineOptions.Clo.ExpandLambdas)
+ {
+ List<Expr!>! axioms;
+ List<Function!>! functions;
+ LambdaHelper.Desugar(impl, out axioms, out functions);
+ // TODO: do something with functions (Z3 currently doesn't need them)
+
+ if (axioms.Count > 0) {
+ CmdSeq cmds = new CmdSeq();
+ foreach (Expr! ax in axioms) {
+ cmds.Add(new AssumeCmd(ax.tok, ax));
+ }
+ Block! entryBlock = (!) impl.Blocks[0];
+ cmds.AddRange(entryBlock.Cmds);
+ entryBlock.Cmds = cmds;
+ }
+ }
+
+
+
// #region Constant Folding
// #endregion
// #region Debug Tracing
|