Fix doxygen doc and MAN pages

Author: Remi Delmas

doc/man/cbmc.1

@@ -334,6 +334,13 @@ set malloc failure mode to return null
 \fB\-\-string\-abstraction\fR
 track C string lengths and zero\-termination
 .TP
+\fB\-\-dfcc\-debug\-lib\fR
+enable debug assertions in the cprover contracts library
+.TP
+\fB\-\-dfcc\-simple\-invalid\-pointer\-model\fR
+use simplified invalid pointer model in the cprover contracts library
+(faster, unsound)
+.TP
 \fB\-\-reachability\-slice\fR
 remove instructions that cannot appear on a trace
 from entry point to a property

doc/man/goto-analyzer.1

@@ -585,6 +585,13 @@ set malloc failure mode to return null
 .TP
 \fB\-\-string\-abstraction\fR
 track C string lengths and zero\-termination
+\fB\-\-dfcc\-debug\-lib\fR
+enable debug assertions in the cprover contracts library
+.TP
+\fB\-\-dfcc\-simple\-invalid\-pointer\-model\fR
+use simplified invalid pointer model in the cprover contracts library
+(faster, unsound)
+.TP
 .SS "Standard Checks"
 From version \fB6.0\fR onwards, \fBcbmc\fR, \fBgoto-analyzer\fR and some other tools
 apply some checks to the program by default (called the "standard checks"), with the

doc/man/goto-instrument.1

@@ -706,6 +706,13 @@ do not allow malloc calls to fail by default
 \fB\-\-string\-abstraction\fR
 track C string lengths and zero\-termination
 .TP
+\fB\-\-dfcc\-debug\-lib\fR
+enable debug assertions in the cprover contracts library
+.TP
+\fB\-\-dfcc\-simple\-invalid\-pointer\-model\fR
+use simplified invalid pointer model in the cprover contracts library
+(faster, unsound)
+.TP
 \fB\-\-model\-argc\-argv\fR \fIn\fR
 Create up to \fIn\fR non-deterministic C strings as entries to \fIargv\fR and
 set \fIargc\fR accordingly. In absence of such modelling, \fIargv\fR is left

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

@@ -80,9 +80,6 @@ class dfcc_spec_functionst
   ///
   /// \param[in] function_id function to generate instructions from
   /// \param[in] havoc_function_id write set variable to havoc
-  /// \param[in] make_havoced_pointers_invalid if true, havoc turns pointers
-  /// into invalid pointers. Otherwise, makes them nondeterministic, i.e.
-  /// range over all addresses known by symex so far.
   /// \param[out] nof_targets maximum number of targets to havoc
   void generate_havoc_function(
     const irep_idt &function_id,

src/util/config.h

@@ -83,10 +83,10 @@ class symbol_table_baset;
   "set malloc failure mode to assert-then-assume\n"                            \
   " {y--malloc-fail-null} \t set malloc failure mode to return null\n"         \
   " {y--string-abstraction} \t track C string lengths and zero-termination\n"  \
-  " {y--dfcc-debug-lib} \t enable debug assertions in the cprover_contracts "  \
+  " {y--dfcc-debug-lib} \t enable debug assertions in the cprover contracts "  \
   "library\n"                                                                  \
   " {y--dfcc-simple-invalid-pointer-model} \t use simplified invalid pointer " \
-  "model in the cprover_contracts library (faster, unsound)\n"
+  "model in the cprover contracts library (faster, unsound)\n"
 
 #define OPT_CONFIG_JAVA "(classpath)(cp)(main-class)"