Merge branch 'feature/andre/val-builtins-auto-default' into 'master'

synchronize with frama-c/frama-c!1214

See merge request !128

src/plugins/e-acsl/tests/bts/bts1390.c

 /* run.config
+   STDOPT: +"-no-val-builtins-auto"
    COMMENT: bts #1390, issue with typing of quantified variables
 */
 

src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle

 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/bts/bts1390.c:12:[value] warning: function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/bts/bts1390.c:12:[value] warning: function __gen_e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/bts/bts1390.c:17:[value] warning: out of bounds read. assert \valid_read(s);
+tests/bts/bts1390.c:13:[value] warning: function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:13:[value] warning: function __gen_e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:18:[value] warning: out of bounds read. assert \valid_read(s);

src/plugins/e-acsl/tests/runtime/initialized.c

 /* run.config
+   STDOPT: +"-no-val-builtins-auto"
    COMMENT: Behaviours of the \initialized E-ACSL predicate
 */
 

src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c

@@ -11,6 +11,7 @@ int main(int argc, char const **argv)
   __e_acsl_full_init((void *)(& memptr));
   int res2 =
     posix_memalign((void **)memptr,(unsigned long)256,(unsigned long)15);
+  /*@ assert Value: initialisation: \initialized(memptr); */
   /*@ assert Value: mem_access: \valid_read(memptr); */
   char *p = *memptr;
   __e_acsl_store_block((void *)(& p),(size_t)8);

src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle

 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/runtime/initialized.c:65:[value] warning: assertion got status unknown.
-tests/runtime/initialized.c:69:[value] warning: assertion got status unknown.
+tests/runtime/initialized.c:66:[value] warning: assertion got status unknown.
+tests/runtime/initialized.c:70:[value] warning: assertion got status unknown.
 FRAMAC_SHARE/libc/stdlib.h:347:[value] warning: function realloc: precondition got status unknown.
 FRAMAC_SHARE/libc/stdlib.h:362:[value] warning: function realloc, behavior dealloc: precondition got status unknown.
-tests/runtime/initialized.c:74:[value] warning: assertion got status unknown.
-tests/runtime/initialized.c:76:[value] warning: assertion got status unknown.
+tests/runtime/initialized.c:75:[value] warning: assertion got status unknown.
+tests/runtime/initialized.c:77:[value] warning: assertion got status unknown.
 FRAMAC_SHARE/libc/stdlib.h:334:[value] warning: function free, behavior deallocation: precondition 'freeable' got status unknown.
-tests/runtime/initialized.c:84:[value] warning: assertion got status unknown.
 tests/runtime/initialized.c:85:[value] warning: assertion got status unknown.
-tests/runtime/initialized.c:93:[value] warning: assertion got status unknown.
-tests/runtime/initialized.c:96:[value] warning: assertion got status unknown.
-tests/runtime/initialized.c:107:[value] warning: out of bounds write. assert \valid(partsi + i);
-tests/runtime/initialized.c:105:[value] warning: out of bounds write. assert \valid(partsc + i);
+tests/runtime/initialized.c:86:[value] warning: assertion got status unknown.
+tests/runtime/initialized.c:94:[value] warning: assertion got status unknown.
+tests/runtime/initialized.c:97:[value] warning: assertion got status unknown.
+tests/runtime/initialized.c:108:[value] warning: out of bounds write. assert \valid(partsi + i);
+tests/runtime/initialized.c:106:[value] warning: out of bounds write. assert \valid(partsc + i);

src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle

@@ -17,7 +17,8 @@ tests/runtime/mainargs.c:15:[value] warning: out of bounds read. assert \valid_r
 tests/runtime/mainargs.c:16:[value] warning: assertion got status unknown.
 tests/runtime/mainargs.c:16:[value] warning: out of bounds read. assert \valid_read(argv + argc);
 FRAMAC_SHARE/libc/string.h:92:[value] warning: function __gen_e_acsl_strlen: precondition 'valid_string_src' got status unknown.
-FRAMAC_SHARE/libc/string.h:92:[value] warning: function strlen: precondition 'valid_string_src' got status unknown.
+FRAMAC_SHARE/libc/string.h:92:[value] warning: builtin Frama_C_strlen: possibly reading indeterminate data
+                                         invalid base: NULL
 FRAMAC_SHARE/libc/string.h:94:[value] warning: function __gen_e_acsl_strlen: postcondition got status unknown.
 tests/runtime/mainargs.c:19:[value] warning: assertion got status unknown.
 tests/runtime/mainargs.c:20:[value] warning: assertion got status unknown.

src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle

 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 tests/runtime/memalign.c:12:[kernel] warning: Neither code nor specification for function posix_memalign, generating default assigns from the prototype
+tests/runtime/memalign.c:14:[value] warning: accessing uninitialized left-value. assert \initialized(memptr);
 tests/runtime/memalign.c:14:[value] warning: out of bounds read. assert \valid_read(memptr);
-tests/runtime/memalign.c:15:[value] warning: assertion got status unknown.
-FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/runtime/memalign.c:16:[value] warning: assertion got status unknown.
-tests/runtime/memalign.c:17:[value] warning: assertion got status unknown.
-FRAMAC_SHARE/libc/stdlib.h:334:[value] warning: function free, behavior deallocation: precondition 'freeable' got status unknown.
-tests/runtime/memalign.c:19:[value] warning: assertion got status unknown.
-tests/runtime/memalign.c:22:[kernel] warning: Neither code nor specification for function aligned_alloc, generating default assigns from the prototype
-tests/runtime/memalign.c:23:[value] warning: assertion got status unknown.
-tests/runtime/memalign.c:26:[value] warning: assertion got status unknown.
-tests/runtime/memalign.c:29:[value] warning: assertion got status unknown.
-tests/runtime/memalign.c:32:[value] warning: assertion got status unknown.
-tests/runtime/memalign.c:33:[value] warning: assertion got status unknown.
-tests/runtime/memalign.c:34:[value] warning: assertion got status invalid (stopping propagation).

src/plugins/e-acsl/tests/runtime/oracle/offset.res.oracle

 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-tests/runtime/offset.c:39:[value] warning: assertion got status unknown.
-FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/runtime/offset.c:40:[value] warning: assertion got status unknown.
-tests/runtime/offset.c:41:[value] warning: assertion got status unknown.
-tests/runtime/offset.c:43:[value] warning: assertion got status unknown.
-tests/runtime/offset.c:44:[value] warning: assertion got status unknown.
-tests/runtime/offset.c:49:[value] warning: assertion got status unknown.
-tests/runtime/offset.c:51:[value] warning: assertion got status unknown.
-tests/runtime/offset.c:53:[value] warning: assertion got status unknown.
-tests/runtime/offset.c:55:[value] warning: assertion got status unknown.