Merge branch 'feature/andre/libc-setenv-putenv' into 'master'

synchronize with frama-c/frama-c!1717

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

src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c

@@ -39,6 +39,9 @@ int main(int argc, char const **argv)
   /*@ assert g1 ≡ \null ∨ \valid(g1); */
   {
     int __gen_e_acsl_or;
+    /*@ assert
+        Value: ptr_comparison: \pointer_comparable((void *)g1, (void *)0);
+    */
     if (g1 == (char *)0) __gen_e_acsl_or = 1;
     else {
       int __gen_e_acsl_initialized;
@@ -60,6 +63,9 @@ int main(int argc, char const **argv)
   /*@ assert g2 ≡ \null ∨ \valid(g2); */
   {
     int __gen_e_acsl_or_2;
+    /*@ assert
+        Value: ptr_comparison: \pointer_comparable((void *)g2, (void *)0);
+    */
     if (g2 == (char *)0) __gen_e_acsl_or_2 = 1;
     else {
       int __gen_e_acsl_initialized_2;

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

@@ -2,10 +2,10 @@
 [e-acsl] Warning: annotating undefined function `getenv':
   the generated program may miss memory instrumentation
   if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:417: Warning: 
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:419: Warning: 
   E-ACSL construct `logic function application' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:417: Warning: 
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:419: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".