Penetrating by blocks

Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs

@@ -182,8 +182,8 @@ void AddIteratorWellformednessCheck(IteratorDecl iter, Procedure proc) {
       var th = new ThisExpr(iter);  // resolve here
       var rds = new MemberSelectExpr(iter.tok, th, iter.Member_Reads);
       var mod = new MemberSelectExpr(iter.tok, th, iter.Member_Modifies);
-      builder.Add(new Bpl.CallCmd(iter.tok, "$IterHavoc0",
-        new List<Bpl.Expr>() { etran.TrExpr(th), etran.TrExpr(rds), etran.TrExpr(mod) },
+      builder.Add(Call(builder.Context, iter.tok, "$IterHavoc0",
+        new List<Expr>() { etran.TrExpr(th), etran.TrExpr(rds), etran.TrExpr(mod) },
         new List<Bpl.IdentifierExpr>()));
 
       // assume the automatic yield-requires precondition (which is always well-formed):  this.Valid()
@@ -206,7 +206,7 @@ void AddIteratorWellformednessCheck(IteratorDecl iter, Procedure proc) {
       builder.Add(Bpl.Cmd.SimpleAssign(iter.tok, new Bpl.IdentifierExpr(iter.tok, oldIterHeap), etran.HeapExpr));
       // simulate a modifies this, this._modifies, this._new;
       var nw = new MemberSelectExpr(iter.tok, th, iter.Member_New);
-      builder.Add(new Bpl.CallCmd(iter.tok, "$IterHavoc1",
+      builder.Add(Call(builder.Context, iter.tok, "$IterHavoc1",
         new List<Bpl.Expr>() { etran.TrExpr(th), etran.TrExpr(mod), etran.TrExpr(nw) },
         new List<Bpl.IdentifierExpr>()));
       // assume the implicit postconditions promised by MoveNext:
@@ -387,7 +387,7 @@ void YieldHavoc(IToken tok, IteratorDecl iter, BoogieStmtListBuilder builder, Ex
       var th = new ThisExpr(iter);
       var rds = new MemberSelectExpr(tok, th, iter.Member_Reads);
       var nw = new MemberSelectExpr(tok, th, iter.Member_New);
-      builder.Add(new Bpl.CallCmd(tok, "$YieldHavoc",
+      builder.Add(Call(builder.Context, tok, "$YieldHavoc",
         new List<Bpl.Expr>() { etran.TrExpr(th), etran.TrExpr(rds), etran.TrExpr(nw) },
         new List<Bpl.IdentifierExpr>()));
       // assume YieldRequires;

Source/DafnyCore/Verifier/BoogieGenerator.cs

@@ -2801,6 +2801,7 @@ private Bpl.Function GetCanCallFunction(Function f) {
     /// Note that SpecWellformedness and Implementation have procedure implementations
     /// but no callers, and vice versa for InterModuleCall, IntraModuleCall, and CoCall.
     /// </summary>
+    /// Remy: TODO Simplify
     enum MethodTranslationKind { SpecWellformedness, CallPre, CallPost, CoCallPre, CoCallPost, Implementation, OverrideCheck }
 
     private static readonly Dictionary<MethodTranslationKind, string> kindSanitizedPrefix =
@@ -2848,14 +2849,16 @@ private static void AddSmtOptionAttribute(Bpl.NamedDeclaration targetDecl, strin
       targetDecl.Attributes = new QKeyValue(targetDecl.tok, "smt_option", new List<object>() { name, value }, targetDecl.Attributes);
     }
 
-    private static CallCmd Call(IToken tok, string methodName, List<Expr> ins, List<Bpl.IdentifierExpr> outs) {
+    private static CallCmd Call(BodyTranslationContext context, IToken tok, string methodName, 
+      List<Expr> ins, List<Bpl.IdentifierExpr> outs) {
       Contract.Requires(tok != null);
       Contract.Requires(methodName != null);
       Contract.Requires(ins != null);
       Contract.Requires(outs != null);
 
-      CallCmd call;
-      call = new CallCmd(tok, methodName, ins, outs);
+      var call = new CallCmd(tok, methodName, ins, outs) {
+        IsFree = context.AssertMode == AssertMode.Assume
+      };
       // CLEMENT enable this: call.ErrorData = "possible violation of function precondition";
       return call;
     }

Source/DafnyCore/Verifier/BoogieStmtListBuilder.cs

@@ -36,9 +36,9 @@ public BoogieStmtListBuilder(BoogieGenerator tran, DafnyOptions options, BodyTra
     public void Add(Cmd cmd) {
       Commands.Add(cmd);
       builder.Add(cmd);
-      if (cmd is Boogie.AssertCmd) {
+      if (cmd is AssertCmd) {
         tran.assertionCount++;
-      } else if (cmd is Boogie.CallCmd call) {
+      } else if (cmd is CallCmd call) {
         // A call command may involve a precondition, but we can't tell for sure until the callee
         // procedure has been generated. Therefore, to be on the same side, we count this call
         // as a possible assertion, unless it's a procedure that's part of the translation and

Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs

@@ -2026,7 +2026,7 @@ void AddCall(BoogieStmtListBuilder callBuilder) {
         callBuilder.Add(new CommentCmd($"ProcessCallStmt: Check precondition"));
         // Make the call
         AddReferencedMember(callee);
-        Bpl.CallCmd call = Call(tok, MethodName(callee, isCoCall ? MethodTranslationKind.CoCallPre : MethodTranslationKind.CallPre), ins, new List<Bpl.IdentifierExpr>());
+        var call = Call(callBuilder.Context, tok, MethodName(callee, isCoCall ? MethodTranslationKind.CoCallPre : MethodTranslationKind.CallPre), ins, new List<Bpl.IdentifierExpr>());
         proofDependencies?.AddProofDependencyId(call, tok, new CallDependency(cs));
         if (
           (assertionOnlyFilter != null && !assertionOnlyFilter(tok)) ||
@@ -2042,7 +2042,8 @@ void AddCall(BoogieStmtListBuilder callBuilder) {
       }
 
       builder.Add(new CommentCmd("ProcessCallStmt: Make the call"));
-      CallCmd post = Call(tok, MethodName(callee, isCoCall ? MethodTranslationKind.CoCallPost : MethodTranslationKind.CallPost), ins, outs);
+      var post = Call(builder.Context, tok, 
+        MethodName(callee, isCoCall ? MethodTranslationKind.CoCallPost : MethodTranslationKind.CallPost), ins, outs);
       proofDependencies?.AddProofDependencyId(post, tok, new CallDependency(cs));
       builder.Add(post);
 
@@ -2220,7 +2221,7 @@ void RecordNewObjectsIn_New(IToken tok, IteratorDecl iter, Bpl.Expr initHeap, Bp
       // call $iter_newUpdate := $IterCollectNewObjects(initHeap, $Heap, this, _new);
       var th = new Bpl.IdentifierExpr(iter.tok, etran.This, predef.RefType);
       var nwField = new Bpl.IdentifierExpr(tok, GetField(iter.Member_New));
-      Bpl.Cmd cmd = new CallCmd(iter.tok, "$IterCollectNewObjects",
+      var cmd = Call(builder.Context, iter.tok, "$IterCollectNewObjects",
         new List<Bpl.Expr>() { initHeap, etran.HeapExpr, th, nwField },
         new List<Bpl.IdentifierExpr>() { updatedSetIE });
       builder.Add(cmd);