ironclad-apps/tools/BoogieAsm/main.fs (15 lines):
	- line 101: // TODO consult Chris about synchronization between include/import
	- line 282: // TODO: check that xc not declared twice?
	- line 406: (* TODO: check offset and scale *)
	- line 407: (* TODO: 1-byte and 2-byte mems *)
	- line 447: (* TODO: operand o3 cannot be a constant *)
	- line 453: (* TODO: operand o3 cannot be a constant *)
	- line 517: (* TODO: o1 cannot be OConst *)
	- line 518: (* TODO: support more cases ? *)
	- line 561: // TODO  | "Cmpxchg" -> print_endline ("    lock cmpxchg " ^ (cmpxchg_operands ctxt args))
	- line 605: | "ghost_IomEnabled" -> print_endline "    ; instr_ghost_IomEnabled" // TODO: this is not an instruction
	- line 646: // TODO: check for yields
	- line 689: // TODO:    | [(_, _, SInline ("instr_IRet", [])); (_, _, SIReturn)] -> print_endline "    iretd"
	- line 913: // TODO:      (if not !symdiff then emit_entry_point { print_out = stream; cur_loc = ref ("fake entry point", 1); cur_indent = ref ""; } publics);
	- line 935: (* TODO: check that procedure implementations are correctly placed and not duplicated? *)
	- line 936: (* TODO: check that no procedures are recursive, even if they aren't used (e.g. readField) *)


ironclad-apps/tools/NuBuild2/NuBuild/BootableAppVerb.cs (5 lines):
	- line 31: ////BuildObject bootloader = new BuildObject("obj\\Trusted\\BootLoader\\pxe-loader");   // TODO: Build this with the NMake verb!
	- line 59: // TODO: Create the bootloader verb.
	- line 75: ////result.Add(this.bootloader);  // TODO: Replace with the bootloader verbs's output.
	- line 111: ////result.Add(bootloaderVerb);             // TODO when we're building the bootloader as part of NuBuild.
	- line 141: // TODO: Rename obj to something meaningful.  Is it a boot file?


ironclad-apps/tools/NuBuild/NuBuild/WinLinkerVerb.cs (5 lines):
	- line 24: // TODO: We shouldn't be using absolute paths to any of these things.
	- line 35: // TODO: Fail more gracefully?  Or better yet, move these into iron/tools.
	- line 46: // TODO: Unpack/generate these automatically.
	- line 47: // TODO: Brian, we're really not going to want to cache these big, empty sources. Or compress? All big (>10MB) files.
	- line 84: // TODO: We should build this!


ironclad-apps/tools/NuBuild2/NuBuild/WinLinkerVerb.cs (5 lines):
	- line 24: // TODO: We shouldn't be using absolute paths to any of these things.
	- line 35: // TODO: Fail more gracefully?  Or better yet, move these into iron/tools.
	- line 46: // TODO: Unpack/generate these automatically.
	- line 47: // TODO: Brian, we're really not going to want to cache these big, empty sources. Or compress? All big (>10MB) files.
	- line 84: // TODO: We should build this!


ironclad-apps/tools/NuBuild/CloudExecutionWorker/CloudExecutionEngine.cs (5 lines):
	- line 51: // TODO: Clean this up.
	- line 84: // TODO: For now, we immediately delete the requests we take.
	- line 156: // TODO: The below will throw cache exceptions if something
	- line 169: // TODO: Move path/directory manipulation code into
	- line 190: null, // This is captureStdout.  TODO: Should cleanup how this is used in ProcessInvoker.


ironclad-apps/tools/NuBuild2/CloudExecutionWorker/CloudExecutionEngine.cs (5 lines):
	- line 51: // TODO: Clean this up.
	- line 84: // TODO: For now, we immediately delete the requests we take.
	- line 156: // TODO: The below will throw cache exceptions if something
	- line 169: // TODO: Move path/directory manipulation code into
	- line 190: null, // This is captureStdout.  TODO: Should cleanup how this is used in ProcessInvoker.


ironclad-apps/tools/NuBuild/NuBuild/BootableAppVerb.cs (4 lines):
	- line 58: // TODO: Create the bootloader verb.
	- line 74: result.Add(this.bootloader);  // TODO: Replace with the bootloader verbs's output.
	- line 110: ////result.Add(bootloaderVerb);             // TODO when we're building the bootloader as part of NuBuild.
	- line 140: // TODO: Rename obj to something meaningful.  Is it a boot file?


ironclad-apps/tools/Beat/main.fs (4 lines):
	- line 137: // TODO: make more robust?
	- line 1446: // TODO: clean up or eliminate?
	- line 1527: // TODO: more cases
	- line 1824: // TODO: initialize x from old__x


ironclad-apps/tools/DafnySpec/DafnySpec.cs (3 lines):
	- line 135: // TODO: use f.Reads?
	- line 322: // TODO: this should be based on attributes, not based on the name
	- line 328: // TODO: this should be based on attributes, not based on the name


ironclad-apps/tools/NuBuild2/NuBuild/BuildObject.cs (2 lines):
	- line 107: /// TODO: Replace this with a property ("RelativePath"?) that is
	- line 301: // TODO: This is a (possibly brittle) workaround for dfy .s


ironclad-apps/tools/NuBuild/NuBuild/ProcessInvoker.cs (2 lines):
	- line 104: // TODO: *All* async verbs need to list their executable (and all the libs it depends upon) as dependencies.
	- line 108: // TODO Is there a better way to escape the args to avoid problems with spaces?


ironclad-apps/tools/NuBuild2/NuBuild/DafnyTransformBaseVerb.cs (2 lines):
	- line 249: Util.Assert(basename.Equals(dfy.getFileNameWithoutExtension()));    // TODO delete prior lines.
	- line 254: {   // TODO undesirable workaround -- DafnyCC doesn't want 'seq.dfy' in its output list, but DafnySpec does...?


ironclad-apps/tools/NuBuild2/NuBuild/ProcessInvoker.cs (2 lines):
	- line 104: // TODO: *All* async verbs need to list their executable (and all the libs it depends upon) as dependencies.
	- line 108: // TODO Is there a better way to escape the args to avoid problems with spaces?


ironclad-apps/tools/NuBuild/NuBuild/Hasher.cs (2 lines):
	- line 18: /// TODO: Move contextResolutionCache to boogie/asm something or other.
	- line 19: /// TODO: Move parsedIncludesCache to BeatIncludes?


ironclad-apps/tools/NuBuild2/AzureManager/Program.cs (2 lines):
	- line 111: // TODO: Provide an unique name for each deployment?
	- line 290: // TODO: Remove hard-coded storage account name.


ironclad-apps/tools/NuBuild/NuBuild/BeatExtensions.cs (2 lines):
	- line 116: // TODO this step really should be a beat function, not part of the build system.
	- line 140: // TODO this really needs to be factored to supply the actual Beat-flavored references separately


ironclad-apps/tools/NuBuild2/NuBuild/SourcePath.cs (2 lines):
	- line 40: this.checkPrefix(sourceType, SourceType.PrebakedObjExpediency, "obj");   // TODO remove.
	- line 71: /// Used to point at bootloader, until we can get an nmake verb working. TODO remove.


ironclad-apps/tools/NuBuild2/NuBuild/Hasher.cs (2 lines):
	- line 18: /// TODO: Move contextResolutionCache to boogie/asm something or other.
	- line 19: /// TODO: Move parsedIncludesCache to BeatIncludes?


ironclad-apps/tools/NuBuild/NuBuild/BuildObject.cs (2 lines):
	- line 107: /// TODO: Replace this with a property ("RelativePath"?) that is
	- line 301: // TODO: This is a (possibly brittle) workaround for dfy .s


ironclad-apps/tools/NuBuild2/NuBuild/BeatExtensions.cs (2 lines):
	- line 116: // TODO this step really should be a beat function, not part of the build system.
	- line 140: // TODO this really needs to be factored to supply the actual Beat-flavored references separately


ironclad-apps/tools/NuBuild2/NuBuild/BoogieVerb.cs (2 lines):
	- line 40: // TODO this will probably break, since we don't know where this bplInput came from. Maybe that's okay, since the verb had to already exist to reach this point.
	- line 142: // TODO this should eventually be a BuildObject from *building* the executable.


ironclad-apps/tools/NuBuild2/NuBuild/NMakeVerb.cs (2 lines):
	- line 82: // TODO: Remove reliance on workingDirOverride, which currently hides dependency issues and other problems.
	- line 107: // TODO this should eventually be a BuildObject from *building* the executable.


ironclad-apps/tools/NuBuild/NuBuild/SourcePath.cs (2 lines):
	- line 40: this.checkPrefix(sourceType, SourceType.PrebakedObjExpediency, "obj");   // TODO remove.
	- line 71: /// Used to point at bootloader, until we can get an nmake verb working. TODO remove.


ironclad-apps/tools/BoogieAsm/emit_bpl.fs (2 lines):
	- line 187: | Procedure (_, Yields) | Procedure (_, Stable) -> "procedure" // TODO: "procedure{:yields}"
	- line 563: List.iter (fun (x, _, _) -> state.PrintLine(x + " := " + x + ";")) symdiff_mods; // make sure symdiff reports modified variables in predictable order (TODO: get /doModSetAnalysis completely turned off)


ironclad-apps/tools/NuBuild/NuBuild/EntryStitcherVerb.cs (2 lines):
	- line 88: // TODO: eliminate this special-case workaround.
	- line 148: // TODO will probably require parameterization per app


ironclad-apps/tools/NuBuild2/NuBuild/EntryStitcherVerb.cs (2 lines):
	- line 88: // TODO: eliminate this special-case workaround.
	- line 148: // TODO will probably require parameterization per app


ironclad-apps/tools/DafnySpec/DafnySpecAst/DafnySpecAst.cs (2 lines):
	- line 644: // TODO: should we implement real type inference?
	- line 799: if (Function == resolver.currentFunction) { Function.IsRecursive = true; } // TODO: mutual recursion


ironclad-apps/tools/NuBuild/NuBuild/BoogieVerb.cs (2 lines):
	- line 40: // TODO this will probably break, since we don't know where this bplInput came from. Maybe that's okay, since the verb had to already exist to reach this point.
	- line 142: // TODO this should eventually be a BuildObject from *building* the executable.


ironclad-apps/tools/NuBuild/NuBuild/DafnyTransformBaseVerb.cs (2 lines):
	- line 249: Util.Assert(basename.Equals(dfy.getFileNameWithoutExtension()));    // TODO delete prior lines.
	- line 254: {   // TODO undesirable workaround -- DafnyCC doesn't want 'seq.dfy' in its output list, but DafnySpec does...?


ironclad-apps/tools/NuBuild/AzureManager/Program.cs (2 lines):
	- line 111: // TODO: Provide an unique name for each deployment?
	- line 290: // TODO: Remove hard-coded storage account name.


ironclad-apps/tools/NuBuild/NuBuild/NMakeVerb.cs (2 lines):
	- line 82: // TODO: Remove reliance on workingDirOverride, which currently hides dependency issues and other problems.
	- line 107: // TODO this should eventually be a BuildObject from *building* the executable.


ironclad-apps/tools/NuBuild2/NuBuild/CloudExecutionQueue.cs (1 line):
	- line 109: // Work-around for running this code in CloudExecutionEngine.  TODO: Clean this up!


ironclad-apps/tools/NuBuild/NuBuild/OrderPreservingSet.cs (1 line):
	- line 54: // TODO I don't know what this property is for.


ironclad-apps/tools/NuBuild/NuBuild/DafnyExecutableDependencies.cs (1 line):
	- line 15: // TODO this should eventually be a BuildObject from *building* the executable.


ironclad-apps/tools/NuBuild/NuBuild/Scheduler.cs (1 line):
	- line 276: /// TODO: Make this private.


ironclad-apps/tools/NuBuild2/NuBuild/Scheduler.cs (1 line):
	- line 276: /// TODO: Make this private.


ironfleet/tools/scripts/build-summary.py (1 line):
	- line 60: # TODO need regex for timeouts


ironclad-apps/tools/NuBuild/NuBuild/MasmVerb.cs (1 line):
	- line 75: // TODO: "/I$SPEC_INCLUDE_DIR"


ironclad-apps/tools/NuBuild/NuBuild/VSSolutionVerb.cs (1 line):
	- line 104: // TODO: Fix absolute path to MSBuild.exe (at least use %SystemRoot%)!


ironclad-apps/tools/NuBuild/NuBuild/IroncladAppVerb.cs (1 line):
	- line 43: // TODO this is the only #define we support just yet, so I'm stuffing it in here.


ironclad-apps/tools/NuBuild2/NuBuild/DafnyVerifyTreeVerb.cs (1 line):
	- line 63: // TODO cast below assumes dafny files are always source files.


ironclad-apps/tools/NuBuild2/NuBuild/ProcessInvokeAsyncWorker.cs (1 line):
	- line 121: /// TODO: executable should be a BuildObject, like every other dependency.


ironclad-apps/tools/NuBuild2/CloudExecutionWorker/WorkerRole.cs (1 line):
	- line 41: // TODO: Multi-thread this.


ironclad-apps/tools/NuBuild2/NuBuild/IVerb.cs (1 line):
	- line 68: /// TODO: Rename to getDiagnosticOutputs().


ironclad-apps/tools/NuBuild2/NuBuild/OrderPreservingSet.cs (1 line):
	- line 54: // TODO I don't know what this property is for.


ironclad-apps/tools/NuBuild/NuBuild/Repository.cs (1 line):
	- line 336: // TODO: Verify that the object exists in the item cache!


ironclad-apps/tools/NuBuild/NuBuild/ItemCacheMultiplexer.cs (1 line):
	- line 340: // TODO present doesn't mean we don't want to overwrite it (eg when


ironclad-apps/tools/NuBuild2/NuBuild/Presentater.cs (1 line):
	- line 13: /// TODO: Rename this (and the file) to IPresentater, or maybe IPresenter.


ironclad-apps/tools/NuBuild2/NuBuild/VerificationResult.cs (1 line):
	- line 227: this._presentation.fillXml(xw);  // TODO we don't know yet how to parse this stuff back in.


ironclad-apps/tools/NuBuild/NuBuild/BeatIncludes.cs (1 line):
	- line 43: // TODO allow commented-out imports until Beat accepts (ignores) them in ifcs files.


ironclad-apps/tools/NuBuild2/NuBuild/DafnyExecutableDependencies.cs (1 line):
	- line 15: // TODO this should eventually be a BuildObject from *building* the executable.


ironclad-apps/tools/NuBuild/NuBuild/XmlFiller.cs (1 line):
	- line 14: /// TODO: Rename to IXmlFiller if we need to keep this.


ironclad-apps/tools/NuBuild/NuBuild/Program.cs (1 line):
	- line 379: // TODO need a better story for relaying failure results. Right now


ironclad-apps/tools/NuBuild/NuBuild/VerificationResult.cs (1 line):
	- line 227: this._presentation.fillXml(xw);  // TODO we don't know yet how to parse this stuff back in.


ironclad-apps/tools/NuBuild/NuBuild/DafnyVerifyTreeVerb.cs (1 line):
	- line 63: // TODO cast below assumes dafny files are always source files.


ironclad-apps/tools/NuBuild2/NuBuild/Repository.cs (1 line):
	- line 336: // TODO: Verify that the object exists in the item cache!


ironclad-apps/tools/NuBuild2/NuBuild/XmlFiller.cs (1 line):
	- line 14: /// TODO: Rename to IXmlFiller if we need to keep this.


ironclad-apps/tools/NuBuild2/NuBuild/ItemCacheMultiplexer.cs (1 line):
	- line 340: // TODO present doesn't mean we don't want to overwrite it (eg when


ironclad-apps/tools/NuBuild2/NuBuild/BeatIncludes.cs (1 line):
	- line 43: // TODO allow commented-out imports until Beat accepts (ignores) them in ifcs files.


ironclad-apps/tools/NuBuild2/NuBuild/IroncladAppVerb.cs (1 line):
	- line 43: // TODO this is the only #define we support just yet, so I'm stuffing it in here.


ironclad-apps/tools/NuBuild2/NuBuild/MasmVerb.cs (1 line):
	- line 75: // TODO: "/I$SPEC_INCLUDE_DIR"


ironclad-apps/tools/NuBuild2/NuBuild/DafnySpecVerb.cs (1 line):
	- line 60: // TODO why doesn't DafnyCC require DafnyPreludePath?


ironclad-apps/tools/NuBuild2/NuBuild/VSSolutionVerb.cs (1 line):
	- line 99: // TODO: Fix absolute path to MSBuild.exe (at least use %SystemRoot%)!


ironclad-apps/tools/NuBuild/NuBuild/DafnySpecVerb.cs (1 line):
	- line 60: // TODO why doesn't DafnyCC require DafnyPreludePath?


ironclad-apps/tools/NuBuild/NuBuild/IVerb.cs (1 line):
	- line 68: /// TODO: Rename to getDiagnosticOutputs().


ironclad-apps/tools/NuBuild/NuBuild/CloudExecutionQueue.cs (1 line):
	- line 109: // Work-around for running this code in CloudExecutionEngine.  TODO: Clean this up!


ironclad-apps/tools/DafnyCC/DafnyCC.cs (1 line):
	- line 195: /* TODO: reduce number of imports for specs


ironfleet/src/Dafny/Distributed/Common/Native/IoNative.cs (1 line):
	- line 226: // TODO: This is pretty inefficient.  Should change Dafny's interface to allow us to


ironclad-apps/tools/NuBuild/NuBuild/ProcessInvokeAsyncWorker.cs (1 line):
	- line 121: /// TODO: executable should be a BuildObject, like every other dependency.


ironclad-apps/tools/NuBuild/CloudExecutionWorker/WorkerRole.cs (1 line):
	- line 41: // TODO: Multi-thread this.


ironclad-apps/tools/NuBuild/NuBuild/Presentater.cs (1 line):
	- line 13: /// TODO: Rename this (and the file) to IPresentater, or maybe IPresenter.


ironclad-apps/tools/NuBuild2/NuBuild/Program.cs (1 line):
	- line 379: // TODO need a better story for relaying failure results. Right now