Merge pull request #7900 from qinheping/features/synthesizer-cbmc-args

SYNTHESIZER: Allow goto-synthesizer accept all CBMC options

Author: qinheping

doc/man/goto-synthesizer.1

@@ -25,7 +25,7 @@ dump the synthesized loop contracts as JSON
 .TP
 \fB\-\-json-\output\fR \fIfile\fR
 specify the output destination of the loop-contracts JSON
-.SS "Backend options:"
+.SS "Accepts all of cbmc's options plus the following backend options:"
 .TP
 \fB\-\-object\-bits\fR n
 number of bits used for object addresses

src/goto-synthesizer/goto_synthesizer_parse_options.cpp

@@ -15,17 +15,32 @@ Author: Qinheping Hu
 
 #include <goto-programs/read_goto_binary.h>
 #include <goto-programs/set_properties.h>
+#include <goto-programs/show_goto_functions.h>
+#include <goto-programs/show_properties.h>
 #include <goto-programs/write_goto_binary.h>
 
 #include <ansi-c/gcc_version.h>
+#include <cbmc/cbmc_parse_options.h>
 #include <goto-instrument/contracts/contracts.h>
 #include <goto-instrument/nondet_volatile.h>
+#include <goto-instrument/reachability_slicer.h>
 
 #include "enumerative_loop_contracts_synthesizer.h"
 
 #include <fstream>
 #include <iostream>
 
+goto_synthesizer_parse_optionst::goto_synthesizer_parse_optionst(
+  int argc,
+  const char **argv)
+  : parse_options_baset(
+      GOTO_SYNTHESIZER_OPTIONS CBMC_OPTIONS,
+      argc,
+      argv,
+      "goto-synthesizer")
+{
+}
+
 /// invoke main modules
 int goto_synthesizer_parse_optionst::doit()
 {
@@ -58,7 +73,7 @@ int goto_synthesizer_parse_optionst::doit()
     configure_gcc(gcc_version);
   }
 
-  // Get options and preprocess `goto_model`.
+  // Get options for the backend verifier and preprocess `goto_model`.
   const auto &options = get_options();
 
   // Synthesize loop invariants and annotate them into `goto_model`
@@ -231,7 +246,8 @@ void goto_synthesizer_parse_optionst::help()
     "\n"
     "Main options:\n" HELP_DUMP_LOOP_CONTRACTS HELP_LOOP_CONTRACTS_NO_UNWIND
     "\n"
-    "Backend options:\n" HELP_CONFIG_BACKEND HELP_SOLVER
+    "Accepts all of cbmc's options plus the following backend "
+    "options:\n" HELP_CONFIG_BACKEND HELP_SOLVER
     "\n"
     " {y--arrays-uf-never} \t never turn arrays into uninterpreted functions\n"
     " {y--arrays-uf-always} \t always turn arrays into uninterpreted"

src/goto-synthesizer/goto_synthesizer_parse_options.h

@@ -38,14 +38,7 @@ class goto_synthesizer_parse_optionst : public parse_options_baset
   int doit() override;
   void help() override;
 
-  goto_synthesizer_parse_optionst(int argc, const char **argv)
-    : parse_options_baset(
-        GOTO_SYNTHESIZER_OPTIONS,
-        argc,
-        argv,
-        "goto-synthesizer")
-  {
-  }
+  goto_synthesizer_parse_optionst(int argc, const char **argv);
 
 protected:
   void register_languages() override;

src/goto-synthesizer/module_dependencies.txt

@@ -1,6 +1,7 @@
 analyses
 ansi-c
 assembler
+cbmc
 cpp
 goto-checker
 goto-instrument