Merge pull request #6576 from tautschnig/cleanup/init-function-updates

Make re-building __CPROVER_initialize safe

Author: tautschnig

doc/cprover-manual/properties.md

@@ -412,3 +412,9 @@ those two options are used, CBMC will assume that `malloc` does not fail.
 Malloc may also fail for external reasons which are not modelled by CProver. If
 you want to replicate this behaviour use the option `--malloc-may-fail` in
 conjunction with one of the above modes of failure.
+
+These malloc failure options need to be set when the C library model is added to
+the program. Typically this is upon invoking CBMC, but if the user has chosen to
+do so via `goto-instrument --add-library`, then the malloc failure mode needs to
+be specified with that `goto-instrument` invocation, i.e., as an option to
+`goto-instrument`.

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -721,10 +721,6 @@ int jbmc_parse_optionst::get_goto_program(
 
     goto_modelt &goto_model = dynamic_cast<goto_modelt &>(*goto_model_ptr);
 
-    // if we added the ansi-c library models here this should also call
-    // add_malloc_may_fail_variable_initializations(goto_model);
-    // here
-
     if(cmdline.isset("validate-goto-model"))
     {
       goto_model.validate();

regression/goto-analyzer/constant_propagation_01/test-vsd.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 16, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_01/test.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 16, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_02/test-vsd.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_02/test.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_03/test-vsd.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_03/test.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_04/test-vsd.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_04/test.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$
 --
 ^warning: ignoring