Check dependencies between commandline options for incremental

Author: peterschrammel

src/cbmc/cbmc_parse_options.cpp

@@ -461,6 +461,50 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
 
 /*******************************************************************\
 
+Function: cbmc_parse_optionst::options_exclusive
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: check conflicts between options: not allowed together
+
+\*******************************************************************/
+
+bool cbmc_parse_optionst::options_exclusive(const char *opt1, const char *opt2)
+{
+  if(cmdline.isset(opt1) && cmdline.isset(opt2))
+  {
+    error() << "--" << opt1 << " cannot be used with --" << opt2 << eom;
+    return true;
+  }
+  return false;
+}
+
+/*******************************************************************\
+
+Function: cbmc_parse_optionst::options_inclusive
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: check conflicts between options: opt1 only if opt2
+
+\*******************************************************************/
+
+bool cbmc_parse_optionst::options_inclusive(const char *opt1, const char *opt2)
+{
+  if(cmdline.isset(opt1) && !cmdline.isset(opt2))
+  {
+    error() << "--" << opt1 << " can only be used with --" << opt2 << eom;
+    return true;
+  }
+  return false;
+}
+
+/*******************************************************************\
+
 Function: cbmc_parse_optionst::doit
 
   Inputs:
@@ -507,6 +551,13 @@ int cbmc_parse_optionst::doit()
     return 1; // should contemplate EX_USAGE from sysexits.h
   }
 
+  if(options_exclusive("incremental", "unwind") ||
+     options_exclusive("incremental", "incremental-check") ||
+     options_inclusive("earliest-loop-exit", "incremental"))
+  {
+    return 1;
+  }
+
   register_languages();
 
   if(cmdline.isset("test-preprocessor"))

src/cbmc/cbmc_parse_options.h

@@ -97,6 +97,9 @@ class cbmc_parse_optionst:
 
   void eval_verbosity();
 
+  bool options_exclusive(const char *opt1, const char *opt2);
+  bool options_inclusive(const char *opt1, const char *opt2);
+
   // get any additional stuff before finalizing
   virtual int get_modules(bmct &bmc)
   {