Summary: 136 instances, 83 unique

Text	Count
// TODO: initialize x from old__x	1
/// TODO: Rename to getDiagnosticOutputs().	2
// TODO: more cases	1
// TODO: This is a (possibly brittle) workaround for dfy .s	2
// TODO: Fail more gracefully?  Or better yet, move these into iron/tools.	2
/// TODO: executable should be a BuildObject, like every other dependency.	2
/// Used to point at bootloader, until we can get an nmake verb working. TODO remove.	2
////result.Add(bootloaderVerb);             // TODO when we're building the bootloader as part of NuBuild.	2
(* TODO: operand o3 cannot be a constant *)	2
// TODO: Multi-thread this.	2
// Work-around for running this code in CloudExecutionEngine.  TODO: Clean this up!	2
// TODO: this should be based on attributes, not based on the name	2
this.checkPrefix(sourceType, SourceType.PrebakedObjExpediency, "obj");   // TODO remove.	2
// TODO: The below will throw cache exceptions if something	1
| Procedure (_, Yields) | Procedure (_, Stable) -> "procedure" // TODO: "procedure{:yields}"	1
// TODO: Remove reliance on workingDirOverride, which currently hides dependency issues and other problems.	2
// TODO: check for yields	1
////result.Add(this.bootloader);  // TODO: Replace with the bootloader verbs's output.	1
/// TODO: Rename to IXmlFiller if we need to keep this.	2
// TODO consult Chris about synchronization between include/import	1
(* TODO: support more cases ? *)	1
// TODO: check that xc not declared twice?	1
(* TODO: check offset and scale *)	1
// TODO: should we implement real type inference?	1
// TODO: Provide an unique name for each deployment?	2
// TODO: Rename obj to something meaningful.  Is it a boot file?	2
// TODO: For now, we immediately delete the requests we take.	2
// TODO: Move path/directory manipulation code into	1
null, // This is captureStdout.  TODO: Should cleanup how this is used in ProcessInvoker.	1
// TODO: Brian, we're really not going to want to cache these big, empty sources. Or compress? All big (>10MB) files.	2
// TODO this is the only #define we support just yet, so I'm stuffing it in here.	2
// TODO need a better story for relaying failure results. Right now	2
// TODO: use f.Reads?	1
// TODO this step really should be a beat function, not part of the build system.	2
// TODO this should eventually be a BuildObject from *building* the executable.	6
// TODO allow commented-out imports until Beat accepts (ignores) them in ifcs files.	2
// TODO: Move path/directory manipulation code into	1
// TODO  | "Cmpxchg" -> print_endline ("    lock cmpxchg " ^ (cmpxchg_operands ctxt args))	1
{   // TODO undesirable workaround -- DafnyCC doesn't want 'seq.dfy' in its output list, but DafnySpec does...?	2
/// TODO: Move parsedIncludesCache to BeatIncludes?	2
// TODO: Verify that the object exists in the item cache!	2
Util.Assert(basename.Equals(dfy.getFileNameWithoutExtension()));    // TODO delete prior lines.	2
(* TODO: 1-byte and 2-byte mems *)	1
/// TODO: Make this private.	2
if (Function == resolver.currentFunction) { Function.IsRecursive = true; } // TODO: mutual recursion	1
(* TODO: check that procedure implementations are correctly placed and not duplicated? *)	1
/// TODO: Move contextResolutionCache to boogie/asm something or other.	2
// TODO why doesn't DafnyCC require DafnyPreludePath?	2
// TODO:      (if not !symdiff then emit_entry_point { print_out = stream; cur_loc = ref ("fake entry point", 1); cur_indent = ref ""; } publics);	1
result.Add(this.bootloader);  // TODO: Replace with the bootloader verbs's output.	1
this._presentation.fillXml(xw);  // TODO we don't know yet how to parse this stuff back in.	2
// TODO: Remove hard-coded storage account name.	2
// TODO cast below assumes dafny files are always source files.	2
// TODO present doesn't mean we don't want to overwrite it (eg when	2
// TODO: We should build this!	2
// 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.	2
// TODO: clean up or eliminate?	1
// TODO Is there a better way to escape the args to avoid problems with spaces?	2
(* TODO: check that no procedures are recursive, even if they aren't used (e.g. readField) *)	1
// TODO: We shouldn't be using absolute paths to any of these things.	2
// TODO:    | [(_, _, SInline ("instr_IRet", [])); (_, _, SIReturn)] -> print_endline "    iretd"	1
////BuildObject bootloader = new BuildObject("obj\\Trusted\\BootLoader\\pxe-loader");   // TODO: Build this with the NMake verb!	1
// TODO: make more robust?	1
// TODO: Fix absolute path to MSBuild.exe (at least use %SystemRoot%)!	2
/* TODO: reduce number of imports for specs	1
// TODO: "/I$SPEC_INCLUDE_DIR"	2
// TODO: This is pretty inefficient.  Should change Dafny's interface to allow us to	1
// TODO: eliminate this special-case workaround.	2
// TODO will probably require parameterization per app	2
// TODO I don't know what this property is for.	2
| "ghost_IomEnabled" -> print_endline "    ; instr_ghost_IomEnabled" // TODO: this is not an instruction	1
// TODO this really needs to be factored to supply the actual Beat-flavored references separately	2
(* TODO: o1 cannot be OConst *)	1
/// TODO: Replace this with a property ("RelativePath"?) that is	2
null, // This is captureStdout.  TODO: Should cleanup how this is used in ProcessInvoker.	1
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)	1
/// TODO: Rename this (and the file) to IPresentater, or maybe IPresenter.	2
// TODO: Clean this up.	2
# TODO need regex for timeouts	1
// TODO: The below will throw cache exceptions if something	1
// TODO: Unpack/generate these automatically.	2
// TODO: *All* async verbs need to list their executable (and all the libs it depends upon) as dependencies.	2
// TODO: Create the bootloader verb.	2