[e-acsl:tests] Update tests

src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c

@@ -4,8 +4,36 @@
 char *__gen_e_acsl_literal_string;
 extern int __e_acsl_sound_verdict;
 
+/*@ requires valid_nptr: \valid_read(nptr);
+    assigns \result;
+    assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
+ */
+int __gen_e_acsl_atoi(char const *nptr);
+
 int a;
 char *n = (char *)"134";
+/*@ requires valid_nptr: \valid_read(nptr);
+    assigns \result;
+    assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
+ */
+int __gen_e_acsl_atoi(char const *nptr)
+{
+  int __retres;
+  {
+    int __gen_e_acsl_valid_read;
+    __e_acsl_store_block((void *)(& nptr),(size_t)8);
+    __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)nptr,
+                                                  sizeof(char const),
+                                                  (void *)nptr,
+                                                  (void *)(& nptr));
+    __e_acsl_assert(__gen_e_acsl_valid_read,"Precondition","atoi",
+                    "\\valid_read(nptr)","FRAMAC_SHARE/libc/stdlib.h",78);
+  }
+  __retres = atoi(nptr);
+  __e_acsl_delete_block((void *)(& nptr));
+  return __retres;
+}
+
 void __e_acsl_globals_init(void)
 {
   static char __e_acsl_already_run = 0;

src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c

@@ -38,10 +38,176 @@ char *__gen_e_acsl_literal_string_17;
 char *__gen_e_acsl_literal_string_18;
 extern int __e_acsl_sound_verdict;
 
+/*@ exits status: \exit_status ≡ \old(status);
+    ensures never_terminates: \false;
+    
+    assigns \exit_status \from status;
+ */
+void __gen_e_acsl_exit(int status);
+
+/*@ ensures
+      result_null_or_valid_fd:
+        \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 16 - 1]);
+    assigns \result;
+    assigns \result \from __fc_p_fopen;
+ */
+FILE *__gen_e_acsl_tmpfile(void);
+
+/*@ requires valid_stream: \valid(stream);
+    ensures result_zero_or_EOF: \result ≡ 0 ∨ \result ≡ -1;
+    assigns \result;
+    assigns \result \from (indirect: stream), (indirect: *stream);
+ */
+int __gen_e_acsl_fclose(FILE *stream);
+
+/*@ ensures result_ok_or_error: \result ≡ -1 ∨ \result ≥ 0;
+    ensures
+      initialization: stat_loc_init_on_success:
+        \result ≥ 0 ∧ \old(stat_loc) ≢ \null ⇒
+        \initialized(\old(stat_loc));
+    assigns \result, *stat_loc;
+    assigns \result \from (indirect: options);
+    assigns *stat_loc \from (indirect: options);
+    
+    behavior stat_loc_null:
+      assumes stat_loc_null: stat_loc ≡ \null;
+      assigns \result;
+      assigns \result \from \nothing;
+    
+    behavior stat_loc_non_null:
+      assumes stat_loc_non_null: stat_loc ≢ \null;
+      requires valid_stat_loc: \valid(stat_loc);
+ */
+pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options);
+
 /*@ assigns \result;
     assigns \result \from \nothing; */
 extern int ( /* missing proto */ fork)(void);
 
+/*@ ensures result_ok_or_error: \result ≡ -1 ∨ \result ≥ 0;
+    ensures
+      initialization: stat_loc_init_on_success:
+        \result ≥ 0 ∧ \old(stat_loc) ≢ \null ⇒
+        \initialized(\old(stat_loc));
+    assigns \result, *stat_loc;
+    assigns \result \from (indirect: options);
+    assigns *stat_loc \from (indirect: options);
+    
+    behavior stat_loc_null:
+      assumes stat_loc_null: stat_loc ≡ \null;
+      assigns \result;
+      assigns \result \from \nothing;
+    
+    behavior stat_loc_non_null:
+      assumes stat_loc_non_null: stat_loc ≢ \null;
+      requires valid_stat_loc: \valid(stat_loc);
+ */
+pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
+{
+  int *__gen_e_acsl_at_2;
+  int *__gen_e_acsl_at;
+  pid_t __retres;
+  {
+    int __gen_e_acsl_implies;
+    __e_acsl_store_block((void *)(& stat_loc),(size_t)8);
+    if (! (stat_loc != (int *)0)) __gen_e_acsl_implies = 1;
+    else {
+      int __gen_e_acsl_valid;
+      __gen_e_acsl_valid = __e_acsl_valid((void *)stat_loc,sizeof(int),
+                                          (void *)stat_loc,
+                                          (void *)(& stat_loc));
+      __gen_e_acsl_implies = __gen_e_acsl_valid;
+    }
+    __e_acsl_assert(__gen_e_acsl_implies,"Precondition","waitpid",
+                    "stat_loc != \\null ==> \\valid(stat_loc)",
+                    "FRAMAC_SHARE/libc/sys/wait.h",92);
+  }
+  __gen_e_acsl_at_2 = stat_loc;
+  __gen_e_acsl_at = stat_loc;
+  __retres = waitpid(pid,stat_loc,options);
+  {
+    int __gen_e_acsl_or;
+    int __gen_e_acsl_and;
+    int __gen_e_acsl_implies_2;
+    if (__retres == -1) __gen_e_acsl_or = 1;
+    else __gen_e_acsl_or = __retres >= 0;
+    __e_acsl_assert(__gen_e_acsl_or,"Postcondition","waitpid",
+                    "\\result == -1 || \\result >= 0",
+                    "FRAMAC_SHARE/libc/sys/wait.h",84);
+    if (__retres >= 0) __gen_e_acsl_and = __gen_e_acsl_at != (int *)0;
+    else __gen_e_acsl_and = 0;
+    if (! __gen_e_acsl_and) __gen_e_acsl_implies_2 = 1;
+    else {
+      int __gen_e_acsl_initialized;
+      __gen_e_acsl_initialized = __e_acsl_initialized((void *)__gen_e_acsl_at_2,
+                                                      sizeof(int));
+      __gen_e_acsl_implies_2 = __gen_e_acsl_initialized;
+    }
+    __e_acsl_assert(__gen_e_acsl_implies_2,"Postcondition","waitpid",
+                    "\\result >= 0 && \\old(stat_loc) != \\null ==> \\initialized(\\old(stat_loc))",
+                    "FRAMAC_SHARE/libc/sys/wait.h",86);
+    __e_acsl_delete_block((void *)(& stat_loc));
+    return __retres;
+  }
+}
+
+/*@ requires valid_stream: \valid(stream);
+    ensures result_zero_or_EOF: \result ≡ 0 ∨ \result ≡ -1;
+    assigns \result;
+    assigns \result \from (indirect: stream), (indirect: *stream);
+ */
+int __gen_e_acsl_fclose(FILE *stream)
+{
+  int __retres;
+  {
+    int __gen_e_acsl_valid;
+    __e_acsl_store_block((void *)(& stream),(size_t)8);
+    __gen_e_acsl_valid = __e_acsl_valid((void *)stream,sizeof(FILE),
+                                        (void *)stream,(void *)(& stream));
+    __e_acsl_assert(__gen_e_acsl_valid,"Precondition","fclose",
+                    "\\valid(stream)","FRAMAC_SHARE/libc/stdio.h",120);
+  }
+  __retres = fclose(stream);
+  {
+    int __gen_e_acsl_or;
+    if (__retres == 0) __gen_e_acsl_or = 1;
+    else __gen_e_acsl_or = __retres == -1;
+    __e_acsl_assert(__gen_e_acsl_or,"Postcondition","fclose",
+                    "\\result == 0 || \\result == -1",
+                    "FRAMAC_SHARE/libc/stdio.h",122);
+    __e_acsl_delete_block((void *)(& stream));
+    return __retres;
+  }
+}
+
+/*@ ensures
+      result_null_or_valid_fd:
+        \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 16 - 1]);
+    assigns \result;
+    assigns \result \from __fc_p_fopen;
+ */
+FILE *__gen_e_acsl_tmpfile(void)
+{
+  FILE *__retres;
+  __e_acsl_store_block((void *)(& __retres),(size_t)8);
+  __retres = tmpfile();
+  __e_acsl_delete_block((void *)(& __retres));
+  return __retres;
+}
+
+/*@ exits status: \exit_status ≡ \old(status);
+    ensures never_terminates: \false;
+    
+    assigns \exit_status \from status;
+ */
+void __gen_e_acsl_exit(int status)
+{
+  exit(status);
+  __e_acsl_assert(0,"Postcondition","exit","\\false",
+                  "FRAMAC_SHARE/libc/stdlib.h",473);
+  return;
+}
+
 void __e_acsl_globals_init(void)
 {
   static char __e_acsl_already_run = 0;

src/plugins/e-acsl/tests/memory/oracle_ci/gen_ctype_macros.c

@@ -4,6 +4,23 @@
 #include "stdlib.h"
 extern int __e_acsl_sound_verdict;
 
+/*@ requires c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1;
+    assigns \result;
+    assigns \result \from c;
+    
+    behavior definitely_match:
+      assumes c_upper: 'A' ≤ c ≤ 'Z';
+      ensures nonzero_result: \result < 0 ∨ \result > 0;
+    
+    behavior definitely_not_match:
+      assumes
+        c_non_upper: c ≡ -1 ∨ (0 ≤ c < 'A') ∨ ('Z' < c ≤ 127);
+      ensures zero_result: \result ≡ 0;
+    
+    disjoint behaviors definitely_not_match, definitely_match;
+ */
+int __gen_e_acsl_isupper(int c);
+
 int main(int argc, char const **argv)
 {
   int __retres;
@@ -39,4 +56,79 @@ int main(int argc, char const **argv)
   return __retres;
 }
 
+/*@ requires c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1;
+    assigns \result;
+    assigns \result \from c;
+    
+    behavior definitely_match:
+      assumes c_upper: 'A' ≤ c ≤ 'Z';
+      ensures nonzero_result: \result < 0 ∨ \result > 0;
+    
+    behavior definitely_not_match:
+      assumes
+        c_non_upper: c ≡ -1 ∨ (0 ≤ c < 'A') ∨ ('Z' < c ≤ 127);
+      ensures zero_result: \result ≡ 0;
+    
+    disjoint behaviors definitely_not_match, definitely_match;
+ */
+int __gen_e_acsl_isupper(int c)
+{
+  int __gen_e_acsl_at_2;
+  int __gen_e_acsl_at;
+  int __retres;
+  {
+    int __gen_e_acsl_and;
+    int __gen_e_acsl_or;
+    if (0 <= c) __gen_e_acsl_and = c <= 255; else __gen_e_acsl_and = 0;
+    if (__gen_e_acsl_and) __gen_e_acsl_or = 1;
+    else __gen_e_acsl_or = c == -1;
+    __e_acsl_assert(__gen_e_acsl_or,"Precondition","isupper",
+                    "(0 <= c <= 255) || c == -1","FRAMAC_SHARE/libc/ctype.h",
+                    174);
+  }
+  {
+    int __gen_e_acsl_or_3;
+    int __gen_e_acsl_or_4;
+    if (c == -1) __gen_e_acsl_or_3 = 1;
+    else {
+      int __gen_e_acsl_and_3;
+      if (0 <= c) __gen_e_acsl_and_3 = c < 65; else __gen_e_acsl_and_3 = 0;
+      __gen_e_acsl_or_3 = __gen_e_acsl_and_3;
+    }
+    if (__gen_e_acsl_or_3) __gen_e_acsl_or_4 = 1;
+    else {
+      int __gen_e_acsl_and_4;
+      if (90 < c) __gen_e_acsl_and_4 = c <= 127; else __gen_e_acsl_and_4 = 0;
+      __gen_e_acsl_or_4 = __gen_e_acsl_and_4;
+    }
+    __gen_e_acsl_at_2 = __gen_e_acsl_or_4;
+  }
+  {
+    int __gen_e_acsl_and_2;
+    if (65 <= c) __gen_e_acsl_and_2 = c <= 90; else __gen_e_acsl_and_2 = 0;
+    __gen_e_acsl_at = __gen_e_acsl_and_2;
+  }
+  __retres = isupper(c);
+  {
+    int __gen_e_acsl_implies;
+    int __gen_e_acsl_implies_2;
+    if (! __gen_e_acsl_at) __gen_e_acsl_implies = 1;
+    else {
+      int __gen_e_acsl_or_2;
+      if (__retres < 0) __gen_e_acsl_or_2 = 1;
+      else __gen_e_acsl_or_2 = __retres > 0;
+      __gen_e_acsl_implies = __gen_e_acsl_or_2;
+    }
+    __e_acsl_assert(__gen_e_acsl_implies,"Postcondition","isupper",
+                    "\\old(\'A\' <= c <= \'Z\') ==> \\result < 0 || \\result > 0",
+                    "FRAMAC_SHARE/libc/ctype.h",178);
+    if (! __gen_e_acsl_at_2) __gen_e_acsl_implies_2 = 1;
+    else __gen_e_acsl_implies_2 = __retres == 0;
+    __e_acsl_assert(__gen_e_acsl_implies_2,"Postcondition","isupper",
+                    "\\old(c == -1 || (0 <= c < \'A\') || (\'Z\' < c <= 127)) ==> \\result == 0",
+                    "FRAMAC_SHARE/libc/ctype.h",181);
+    return __retres;
+  }
+}
+
 

src/plugins/e-acsl/tests/memory/oracle_ci/gen_mainargs.c

@@ -4,6 +4,13 @@
 #include "string.h"
 extern int __e_acsl_sound_verdict;
 
+/*@ requires valid_string_s: valid_read_string(s);
+    ensures acsl_c_equiv: \result ≡ strlen(\old(s));
+    assigns \result;
+    assigns \result \from (indirect: *(s + (0 ..)));
+ */
+size_t __gen_e_acsl_strlen(char const *s);
+
 /*@ requires \valid(&argc);
     requires \valid(&argv); */
 int main(int argc, char **argv);
@@ -197,4 +204,18 @@ int main(int argc, char **argv)
   return __retres;
 }
 
+/*@ requires valid_string_s: valid_read_string(s);
+    ensures acsl_c_equiv: \result ≡ strlen(\old(s));
+    assigns \result;
+    assigns \result \from (indirect: *(s + (0 ..)));
+ */
+size_t __gen_e_acsl_strlen(char const *s)
+{
+  size_t __retres;
+  __e_acsl_store_block((void *)(& s),(size_t)8);
+  __retres = strlen(s);
+  __e_acsl_delete_block((void *)(& s));
+  return __retres;
+}
+
 

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

@@ -5,6 +5,48 @@ char *__gen_e_acsl_literal_string_2;
 char *__gen_e_acsl_literal_string;
 extern int __e_acsl_sound_verdict;
 
+/*@ requires valid_name: valid_read_string(name);
+    ensures null_or_valid_result: \result ≡ \null ∨ \valid(\result);
+    assigns \result;
+    assigns \result \from __fc_env[0 ..], (indirect: name), *(name + (0 ..));
+ */
+char *__gen_e_acsl_getenv(char const *name);
+
+/*@ requires valid_name: valid_read_string(name);
+    ensures null_or_valid_result: \result ≡ \null ∨ \valid(\result);
+    assigns \result;
+    assigns \result \from __fc_env[0 ..], (indirect: name), *(name + (0 ..));
+ */
+char *__gen_e_acsl_getenv(char const *name)
+{
+  char *__retres;
+  __e_acsl_store_block((void *)(& __retres),(size_t)8);
+  __e_acsl_temporal_reset_parameters();
+  __e_acsl_temporal_reset_return();
+  __retres = getenv(name);
+  __e_acsl_temporal_store_nblock((void *)(& __retres),(void *)*(& __retres));
+  {
+    int __gen_e_acsl_or;
+    __e_acsl_temporal_save_return((void *)(& __retres));
+    /*@ assert
+        Eva: ptr_comparison: \pointer_comparable((void *)__retres, (void *)0);
+    */
+    if (__retres == (char *)0) __gen_e_acsl_or = 1;
+    else {
+      int __gen_e_acsl_valid;
+      __gen_e_acsl_valid = __e_acsl_valid((void *)__retres,sizeof(char),
+                                          (void *)__retres,
+                                          (void *)(& __retres));
+      __gen_e_acsl_or = __gen_e_acsl_valid;
+    }
+    __e_acsl_assert(__gen_e_acsl_or,"Postcondition","getenv",
+                    "\\result == \\null || \\valid(\\result)",
+                    "FRAMAC_SHARE/libc/stdlib.h",488);
+    __e_acsl_delete_block((void *)(& __retres));
+    return __retres;
+  }
+}
+
 void __e_acsl_globals_init(void)
 {
   static char __e_acsl_already_run = 0;

src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_memcpy.c

@@ -4,6 +4,34 @@
 #include "string.h"
 extern int __e_acsl_sound_verdict;
 
+/*@ requires valid_dest: valid_or_empty(dest, n);
+    requires valid_src: valid_read_or_empty(src, n);
+    requires
+      separation:
+        \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
+    ensures
+      copied_contents:
+        memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
+        0;
+    ensures result_ptr: \result ≡ \old(dest);
+    assigns *((char *)dest + (0 .. n - 1)), \result;
+    assigns *((char *)dest + (0 .. n - 1))
+      \from *((char *)src + (0 .. n - 1));
+    assigns \result \from dest;
+ */
+void *__gen_e_acsl_memcpy(void * __restrict dest,
+                          void const * __restrict src, size_t n);
+
+/*@ requires valid_s: valid_or_empty(s, n);
+    ensures
+      acsl_c_equiv: memset((char *)\old(s), \old(c), \old(n)) ≡ \true;
+    ensures result_ptr: \result ≡ \old(s);
+    assigns *((char *)s + (0 .. n - 1)), \result;
+    assigns *((char *)s + (0 .. n - 1)) \from c;
+    assigns \result \from s;
+ */
+void *__gen_e_acsl_memset(void *s, int c, size_t n);
+
 int main(void)
 {
   int __retres;
@@ -357,4 +385,64 @@ int main(void)
   return __retres;
 }
 
+/*@ requires valid_s: valid_or_empty(s, n);
+    ensures
+      acsl_c_equiv: memset((char *)\old(s), \old(c), \old(n)) ≡ \true;
+    ensures result_ptr: \result ≡ \old(s);
+    assigns *((char *)s + (0 .. n - 1)), \result;
+    assigns *((char *)s + (0 .. n - 1)) \from c;
+    assigns \result \from s;
+ */
+void *__gen_e_acsl_memset(void *s, int c, size_t n)
+{
+  void *__gen_e_acsl_at;
+  void *__retres;
+  __e_acsl_store_block((void *)(& s),(size_t)8);
+  __e_acsl_temporal_pull_parameter((void *)(& s),0U,8UL);
+  __e_acsl_temporal_reset_parameters();
+  __e_acsl_temporal_reset_return();
+  __e_acsl_temporal_save_nreferent_parameter((void *)(& s),0U);
+  __e_acsl_temporal_memset(s,c,n);
+  __gen_e_acsl_at = s;
+  __retres = memset(s,c,n);
+  __e_acsl_assert(__retres == __gen_e_acsl_at,"Postcondition","memset",
+                  "\\result == \\old(s)","FRAMAC_SHARE/libc/string.h",119);
+  __e_acsl_delete_block((void *)(& s));
+  return __retres;
+}
+
+/*@ requires valid_dest: valid_or_empty(dest, n);
+    requires valid_src: valid_read_or_empty(src, n);
+    requires
+      separation:
+        \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
+    ensures
+      copied_contents:
+        memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
+        0;
+    ensures result_ptr: \result ≡ \old(dest);
+    assigns *((char *)dest + (0 .. n - 1)), \result;
+    assigns *((char *)dest + (0 .. n - 1))
+      \from *((char *)src + (0 .. n - 1));
+    assigns \result \from dest;
+ */
+void *__gen_e_acsl_memcpy(void * __restrict dest,
+                          void const * __restrict src, size_t n)
+{
+  void *__gen_e_acsl_at;
+  void *__retres;
+  __e_acsl_store_block((void *)(& dest),(size_t)8);
+  __e_acsl_temporal_pull_parameter((void *)(& dest),0U,8UL);
+  __e_acsl_temporal_reset_parameters();
+  __e_acsl_temporal_reset_return();
+  __e_acsl_temporal_save_nreferent_parameter((void *)(& dest),0U);
+  __e_acsl_temporal_memcpy(dest,(void *)src,n);
+  __gen_e_acsl_at = dest;
+  __retres = memcpy(dest,src,n);
+  __e_acsl_assert(__retres == __gen_e_acsl_at,"Postcondition","memcpy",
+                  "\\result == \\old(dest)","FRAMAC_SHARE/libc/string.h",99);
+  __e_acsl_delete_block((void *)(& dest));
+  return __retres;
+}
+