CONTRACTS (DFCC) add new command line switch --dyncontracts

Author: Remi Delmas

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1145,10 +1145,49 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     // recalculate numbers, etc.
     goto_model.goto_functions.update();
   }
+  bool new_contracts = false;
+  if(cmdline.isset(FLAG_DFCC))
+  {
+    new_contracts = true;
+    if(cmdline.get_values(FLAG_DFCC).size() == 1)
+    {
+      const std::string &harness_id = *cmdline.get_values(FLAG_DFCC).begin();
+
+      do_indirect_call_and_rtti_removal();
+
+      std::set<std::string> to_replace(
+        cmdline.get_values(FLAG_REPLACE_CALL).begin(),
+        cmdline.get_values(FLAG_REPLACE_CALL).end());
+
+      std::set<std::string> to_check(
+        cmdline.get_values(FLAG_ENFORCE_CONTRACT).begin(),
+        cmdline.get_values(FLAG_ENFORCE_CONTRACT).end());
+
+      std::set<std::string> to_exclude_from_nondet_static(
+        cmdline.get_values("nondet-static-exclude").begin(),
+        cmdline.get_values("nondet-static-exclude").end());
+
+      dfcc(
+        goto_model,
+        harness_id,
+        to_check,
+        to_replace,
+        cmdline.isset(FLAG_LOOP_CONTRACTS),
+        to_exclude_from_nondet_static,
+        log);
+    }
+    else
+    {
+      log.error() << "only one --dyncontracts entry point allowed"
+                  << messaget::eom;
+      throw 0;
+    }
+  }
 
   if(
-    cmdline.isset(FLAG_LOOP_CONTRACTS) || cmdline.isset(FLAG_REPLACE_CALL) ||
-    cmdline.isset(FLAG_ENFORCE_CONTRACT))
+    !new_contracts &&
+    (cmdline.isset(FLAG_LOOP_CONTRACTS) || cmdline.isset(FLAG_REPLACE_CALL) ||
+     cmdline.isset(FLAG_ENFORCE_CONTRACT)))
   {
     do_indirect_call_and_rtti_removal();
     code_contractst contracts(goto_model, log);
@@ -1894,6 +1933,7 @@ void goto_instrument_parse_optionst::help()
     "                             force aggressive slicer to preserve all direct paths\n" // NOLINT(*)
     "\n"
     "Code contracts:\n"
+    HELP_DFCC
     HELP_LOOP_CONTRACTS
     HELP_REPLACE_CALL
     HELP_ENFORCE_CONTRACT

src/goto-instrument/goto_instrument_parse_options.h

@@ -41,6 +41,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "unwindset.h"
 
 #include "contracts/contracts.h"
+#include "contracts/dfcc.h"
 #include "wmm/weak_memory.h"
 
 // clang-format off
@@ -95,6 +96,7 @@ Author: Daniel Kroening, kroening@kroening.com
   "(z3)(add-library)(show-dependence-graph)" \
   "(horn)(skip-loops):(model-argc-argv):" \
   "(" FLAG_LOOP_CONTRACTS ")" \
+  "(" FLAG_DFCC "):" \
   "(" FLAG_REPLACE_CALL "):" \
   "(" FLAG_ENFORCE_CONTRACT "):" \
   "(show-threaded)(list-calls-args)" \