CONTRACTS: cleanup TODOs

Author: Remi Delmas

src/goto-instrument/contracts/dynamic-frames/dfcc.cpp

@@ -6,9 +6,6 @@ Author: Remi Delmas, [email protected]
 
 \*******************************************************************/
 
-// TODO havoc global statics
-// TODO move disable assigns clause pragma into utils
-// TODO prune includes
 #include "dfcc.h"
 
 #include <util/config.h>

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp

@@ -307,8 +307,6 @@ void dfcc_instrumentt::instrument_function(
   PRECONDITION_WITH_DIAGNOSTICS(
     found != goto_model.goto_functions.function_map.end(),
     "Function '" + id2string(function_id) + "' must exist in the model.");
-  // TODO instead of erroring out, create an entry in the function table
-  // and create body with assert(false); assume(false)
 
   auto &goto_function = found->second;
 
@@ -440,8 +438,6 @@ void dfcc_instrumentt::instrument_instructions(
     }
     if(target->is_dead())
     {
-      // TODO: discuss if we really need to record DEAD instructions since the
-      // default CBMC checks are already able to detect writes to DEAD objects
       instrument_dead(function_id, write_set, target, goto_program, cfg_info);
     }
     else if(target->is_assign())