Add /generateTestBoogie in DafnyTestGeneration

[matt4530]

Thanks to Dr. Mercer and Kyle Storey for inspiration and initial work. This just wraps it neatly into a command line option.

Specifying it like this makes sure we don't pollute std out so we can still write the generated tests to a file.

Consider this use case for it:
dafny /generateTestBoogie:hw5.bpl /definiteAssignment:3 /generateTestMode:Block hw5.dfy > hw5_test_block.dfy

hw5.dfy:

module M {
  method foobar(v:int) returns (i:int) {
    // captures 5+
    if(v >= 5){
      return 0;
    }
    // capture 4+
    if(v >= 4){
      return 1;
    }
    // capture none, since 5+ was already caught
    if(v >= 6) {
      return 2;
    }
    // capture 3-
    return 3;
  }
}

which produces hw5_modification_0.bpl (and 9 other bpl files) like this:

DafnyTestGeneration.BlockBasedModification#Impl$$M.__default.foobar :
implementation Impl$$M.__default.foobar(v#0: int) returns (defass#i#0: bool, i#0: int, $_reverifyPost: bool)
{
  var $_Frame: <beta>[ref,Field beta]bool;

  anon0:
    assume {:print "Impl", " | ", "Impl$$M.__default.foobar", " | ", v#0} true;
    assume {:print "Types", " | ", "int"} true;
    $_Frame := (lambda<alpha> $o: ref, $f: Field alpha :: $o != null && read($Heap, $o, alloc) ==> false);
    assume {:captureState "lecture_programs/hw5.dfy(2,39): initial state"} true;
    $_reverifyPost := false;
    assume true;
    assume {:print "Block", " | ", "Impl$$M.__default.foobar", " | ", "17099"} true;
    goto anon11_Then, anon11_Else;

  anon11_Then:
    assume {:partition} v#0 >= LitInt(5);
    assume true;
    assume true;
    i#0 := LitInt(0);
    defass#i#0 := true;
    assume {:captureState "lecture_programs/hw5.dfy(5,14)"} true;
    assert defass#i#0;
    assume {:print "Block", " | ", "Impl$$M.__default.foobar", " | ", "17100"} true;
    return;

  anon11_Else:
    assume {:partition} LitInt(5) > v#0;
    assume {:print "Block", " | ", "Impl$$M.__default.foobar", " | ", "17102"} true;
    goto anon3;

  anon3:
    assume true;
    assume {:print "Block", " | ", "Impl$$M.__default.foobar", " | ", "17109"} true;
    goto anon12_Then, anon12_Else;

  anon12_Then:
    assume {:partition} v#0 >= LitInt(4);
    assume true;
    assume true;
    i#0 := LitInt(1);
    defass#i#0 := true;
    assume {:captureState "lecture_programs/hw5.dfy(9,14)"} true;
    assert defass#i#0;
    assume {:print "Block", " | ", "Impl$$M.__default.foobar", " | ", "17110"} true;
    return;

  anon12_Else:
    assume {:partition} LitInt(4) > v#0;
    assume {:print "Block", " | ", "Impl$$M.__default.foobar", " | ", "17112"} true;
    goto anon6;

  anon6:
    assume true;
    assume {:print "Block", " | ", "Impl$$M.__default.foobar", " | ", "17119"} true;
    goto anon13_Then, anon13_Else;

  anon13_Then:
    assume {:partition} v#0 >= LitInt(6);
    assume true; 

and also produces the un-shown hw5_test_block.dfy

[matt4530]

Before we merge, we might want to nuke these changes:
https://github.com/byu-dafny/dafny/pull/1/files#diff-2375e053597753dae383e30da45bce3a97e5fa2e7e9a3fc601cf68923df03516
They were debugging stuff I did to understand the boogie, so just let me know and I'll patch them out.

[matt4530]

Fixed those, is ready for merge if you want.