Update CLI for applyin loop contracts with dfcc

Author: qinheping

regression/contracts-dfcc/invar_assigns_opt/test.desc

@@ -1,18 +1,18 @@
 CORE
 main.c
---dfcc main
+--dfcc main --apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
-^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
-^\[main.assertion.\d+\] .* assertion r1 == 0: SUCCESS$
-^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
-^\[main.assigns.\d+\] .* Check that s2 is assignable: SUCCESS$
-^\[main.assigns.\d+\] .* Check that r2 is assignable: SUCCESS$
-^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
-^\[main.assertion.\d+\] .* assertion r2 == 0: SUCCESS$
+^\[foo.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[foo.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[foo.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
+^\[foo.assertion.\d+\] .* assertion r1 == 0: SUCCESS$
+^\[foo.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[foo.assigns.\d+\] .* Check that s2 is assignable: SUCCESS$
+^\[foo.assigns.\d+\] .* Check that r2 is assignable: SUCCESS$
+^\[foo.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[foo.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
+^\[foo.assertion.\d+\] .* assertion r2 == 0: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 --

regression/contracts-dfcc/loop_assigns-01/test.desc

@@ -1,13 +1,13 @@
 CORE
 main.c
---dfcc main
+--dfcc main --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
-^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$
-^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$
-^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.\d+\] .* assertion b->data\[5\] == 0: FAILURE$
+^\[foo.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[foo.assigns.\d+\] .* Check that i is assignable: SUCCESS$
+^\[foo.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$
+^\[foo.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[foo.assertion.\d+\] .* assertion b->data\[5\] == 0: FAILURE$
 ^VERIFICATION FAILED$
 --
 --

regression/contracts-dfcc/loop_assigns_inference-02/test.desc

@@ -1,14 +1,14 @@
 CORE
 main.c
---dfcc main
+--dfcc main --apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
-^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$
-^\[main.assigns.\d+\] .* Check that b\[(.*)i\] is assignable: SUCCESS$
+^\[foo.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[foo.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[foo.assigns.\d+\] .* Check that i is assignable: SUCCESS$
+^\[foo.assigns.\d+\] .* Check that b\[(.*)i\] is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 --
-This test checks assigns clauses (i, __CPROVER_POINTER_OBJECT(b)) is inferred,
+This test checks assigns clauses (i, __CPROVER_object_whole(b)) is inferred,
 and widened correctly.

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

@@ -213,7 +213,13 @@ dfcct::dfcct(
       library,
       spec_functions,
       contract_clauses_codegen),
-    instrument(goto_model, message_handler, utils, loop_instrument, library),
+    instrument(
+      goto_model,
+      message_handler,
+      utils,
+      loop_instrument,
+      apply_loop_contracts,
+      library),
     max_assigns_clause_size(0)
 {
   transform_goto_model();

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

@@ -47,12 +47,14 @@ dfcc_instrumentt::dfcc_instrumentt(
   message_handlert &message_handler,
   dfcc_utilst &utils,
   dfcc_loop_instrumentt &loop_instrument,
+  const bool apply_loop_contracts,
   dfcc_libraryt &library)
   : goto_model(goto_model),
     message_handler(message_handler),
     log(message_handler),
     utils(utils),
     loop_instrument(loop_instrument),
+    apply_loop_contracts(apply_loop_contracts),
     library(library),
     ns(goto_model.symbol_table)
 {
@@ -475,12 +477,15 @@ void dfcc_instrumentt::instrument_function_body(
   auto &body = goto_function.body;
 
   // Instrument all loops in the function.
-  instrument_loops(
-    function_id,
-    goto_function,
-    write_set,
-    cfg_info,
-    function_pointer_contracts);
+  if(apply_loop_contracts)
+  {
+    instrument_loops(
+      function_id,
+      goto_function,
+      write_set,
+      cfg_info,
+      function_pointer_contracts);
+  }
 
   const auto &not_in_loop_filter =
     [&](const goto_programt::instructiont::targett &target) {

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

@@ -45,6 +45,7 @@ class dfcc_instrumentt
     message_handlert &message_handler,
     dfcc_utilst &utils,
     dfcc_loop_instrumentt &loop_instrument,
+    const bool apply_loop_contracts,
     dfcc_libraryt &library);
 
   /// True if id has `CPROVER_PREFIX` or `__VERIFIER` or `nondet` prefix,
@@ -162,6 +163,7 @@ class dfcc_instrumentt
   messaget log;
   dfcc_utilst &utils;
   dfcc_loop_instrumentt &loop_instrument;
+  const bool apply_loop_contracts;
   dfcc_libraryt &library;
   namespacet ns;
 

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1169,14 +1169,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
         "Use a single " FLAG_DFCC " option");
     }
 
-    if(cmdline.isset(FLAG_LOOP_CONTRACTS))
-    {
-      throw invalid_command_line_argument_exceptiont(
-        "Incompatible options detected",
-        "--" FLAG_DFCC " and --" FLAG_LOOP_CONTRACTS,
-        "Use either --" FLAG_DFCC " or --" FLAG_LOOP_CONTRACTS);
-    }
-
     do_indirect_call_and_rtti_removal();
 
     const irep_idt harness_id(cmdline.get_value(FLAG_DFCC));
@@ -1215,7 +1207,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
                          : optionalt<irep_idt>{to_enforce.front()},
       allow_recursive_calls,
       to_replace,
-      false,
+      cmdline.isset(FLAG_LOOP_CONTRACTS),
       to_exclude_from_nondet_static,
       log.get_message_handler());
   }