Set malloc_may_fail, malloc_failure_mode via defines

Do not fix up the value by tweaking __CPROVER_initialize. This
simplifies the code and allows us to regenerate __CPROVER_initialize at
any time (at least as far as __CPROVER_malloc_may_fail and
__CPROVER_malloc_failure_mode are concerned).

This change also avoids any cost of variables to be processed by program
analysis when they are compile-time constants. This, in turn, entails
updates to various goto-analyzer tests. These updates include removal of
redundant patterns.

Author: peterschrammel

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