Merge branch 'fix/andre/string-specs-null' into 'master'

sync with frama-c!2018

See merge request frama-c/e-acsl!252

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

@@ -2,13 +2,13 @@
 [e-acsl] Warning: annotating undefined function `strlen':
   the generated program may miss memory instrumentation
   if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/string.h:111: Warning: 
+[e-acsl] FRAMAC_SHARE/libc/string.h:125: Warning: 
   E-ACSL construct `logic function application' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:111: Warning: 
+[e-acsl] FRAMAC_SHARE/libc/string.h:125: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:113: Warning: 
+[e-acsl] FRAMAC_SHARE/libc/string.h:127: Warning: 
   E-ACSL construct `logic function returning an integer' is not yet supported.
   Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
@@ -32,9 +32,9 @@
   function __e_acsl_assert: precondition got status unknown.
 [eva:alarm] tests/runtime/mainargs.c:18: Warning: 
   function __gen_e_acsl_strlen: precondition 'valid_string_s' got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/string.h:111: Warning: 
+[eva:alarm] FRAMAC_SHARE/libc/string.h:125: Warning: 
   function strlen: precondition 'valid_string_s' got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/string.h:113: Warning: 
+[eva:alarm] FRAMAC_SHARE/libc/string.h:127: Warning: 
   function __gen_e_acsl_strlen: postcondition 'acsl_c_equiv' got status unknown.
 [eva:alarm] tests/runtime/mainargs.c:19: Warning: assertion got status unknown.
 [eva:alarm] tests/runtime/mainargs.c:20: Warning: assertion got status unknown.

src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle

@@ -5,20 +5,29 @@
 [e-acsl] Warning: annotating undefined function `memset':
   the generated program may miss memory instrumentation
   if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/string.h:78: Warning: 
+[e-acsl] FRAMAC_SHARE/libc/string.h:92: Warning: 
   E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:101: Warning: 
+[e-acsl] FRAMAC_SHARE/libc/string.h:115: Warning: 
+  E-ACSL construct `logic function application' is not yet supported.
+  Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:115: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:104: Warning: 
+[e-acsl] FRAMAC_SHARE/libc/string.h:118: Warning: 
   E-ACSL construct `user-defined logic type' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:81: Warning: 
+[e-acsl] FRAMAC_SHARE/libc/string.h:92: Warning: 
+  E-ACSL construct `logic function application' is not yet supported.
+  Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:93: Warning: 
+  E-ACSL construct `logic function application' is not yet supported.
+  Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:95: Warning: 
   E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:81: Warning: 
+[e-acsl] FRAMAC_SHARE/libc/string.h:95: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:84: Warning: 
+[e-acsl] FRAMAC_SHARE/libc/string.h:98: Warning: 
   E-ACSL construct `logic function returning an integer' is not yet supported.
   Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".