[eacsl:tests] Remove obsolete oracles

src/plugins/e-acsl/tests/constructs/oracle_dev/false.res.oracle

-[kernel] Parsing tests/constructs/false.i (no preprocessing)

src/plugins/e-acsl/tests/constructs/oracle_dev/function_contract.res.oracle

-[kernel] Parsing tests/constructs/function_contract.i (no preprocessing)

src/plugins/e-acsl/tests/constructs/oracle_dev/ghost.res.oracle

-[kernel] Parsing tests/constructs/ghost.i (no preprocessing)

src/plugins/e-acsl/tests/constructs/oracle_dev/invariant.res.oracle

-[kernel] Parsing tests/constructs/invariant.i (no preprocessing)

src/plugins/e-acsl/tests/constructs/oracle_dev/labeled_stmt.res.oracle

-[kernel] Parsing tests/constructs/labeled_stmt.i (no preprocessing)

src/plugins/e-acsl/tests/constructs/oracle_dev/lazy.res.oracle

-[kernel] Parsing tests/constructs/lazy.i (no preprocessing)

src/plugins/e-acsl/tests/constructs/oracle_dev/loop.res.oracle

-[kernel] Parsing tests/constructs/loop.i (no preprocessing)

src/plugins/e-acsl/tests/constructs/oracle_dev/nested_code_annot.res.oracle

-[kernel] Parsing tests/constructs/nested_code_annot.i (no preprocessing)

src/plugins/e-acsl/tests/constructs/oracle_dev/result.res.oracle

-[kernel] Parsing tests/constructs/result.i (no preprocessing)

src/plugins/e-acsl/tests/constructs/oracle_dev/stmt_contract.res.oracle

-[kernel] Parsing tests/constructs/stmt_contract.i (no preprocessing)

src/plugins/e-acsl/tests/constructs/oracle_dev/true.res.oracle

-[kernel] Parsing tests/constructs/true.i (no preprocessing)

src/plugins/e-acsl/tests/constructs/oracle_dev/typedef.res.oracle

-[kernel] Parsing tests/constructs/typedef.i (no preprocessing)

src/plugins/e-acsl/tests/examples/oracle_dev/functions_contiki.res.oracle

-[kernel] Parsing tests/examples/functions_contiki.c (with preprocessing)

src/plugins/e-acsl/tests/examples/oracle_dev/linear_search.res.oracle

-[kernel] Parsing tests/examples/linear_search.i (no preprocessing)

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

-/* Generated by Frama-C */
-#include "signal.h"
-#include "stdio.h"
-#include "stdlib.h"
-#include "string.h"
-#include "sys/time.h"
-#include "sys/wait.h"
-#include "time.h"
-#include "unistd.h"
-#include "wchar.h"
-char *__gen_e_acsl_literal_string_6;
-char *__gen_e_acsl_literal_string_8;
-char *__gen_e_acsl_literal_string_5;
-char *__gen_e_acsl_literal_string_9;
-char *__gen_e_acsl_literal_string_7;
-char *__gen_e_acsl_literal_string;
-char *__gen_e_acsl_literal_string_2;
-char *__gen_e_acsl_literal_string_4;
-char *__gen_e_acsl_literal_string_3;
-void signal_eval(int status, int expect_signal, char const *at)
-{
-  __e_acsl_store_block((void *)(& at),(size_t)8);
-  __e_acsl_store_block((void *)(& expect_signal),(size_t)4);
-  __e_acsl_store_block((void *)(& status),(size_t)4);
-  int signalled = (int)((signed char)((status & 0x7f) + 1)) >> 1 > 0;
-  __e_acsl_store_block((void *)(& signalled),(size_t)4);
-  __e_acsl_full_init((void *)(& signalled));
-  if (signalled) {
-    if (expect_signal) __e_acsl_builtin_printf("s",
-                                               __gen_e_acsl_literal_string,
-                                               at);
-    else goto _LAND_1;
-  }
-  else 
-    _LAND_1:
-    if (! signalled) {
-      if (! expect_signal) __e_acsl_builtin_printf("s",
-                                                   __gen_e_acsl_literal_string_2,
-                                                   at);
-      else goto _LAND_0;
-    }
-    else 
-      _LAND_0:
-      if (! signalled) {
-        if (expect_signal) {
-          __e_acsl_builtin_printf("s",__gen_e_acsl_literal_string_3,at);
-          __gen_e_acsl_exit(1);
-        }
-        else goto _LAND;
-      }
-      else {
-        _LAND: ;
-        if (signalled) 
-          if (! expect_signal) {
-            __e_acsl_builtin_printf("s",__gen_e_acsl_literal_string_4,at);
-            __gen_e_acsl_exit(2);
-          }
-      }
-  __e_acsl_delete_block((void *)(& at));
-  __e_acsl_delete_block((void *)(& expect_signal));
-  __e_acsl_delete_block((void *)(& status));
-  __e_acsl_delete_block((void *)(& signalled));
-  return;
-}
-
-char const *valid_specifiers = "diouxfFeEgGaAcspn";
-void apply_specifier(char *format, int spec)
-{
-  int n;
-  char *tmp_1;
-  __e_acsl_store_block((void *)(& tmp_1),(size_t)8);
-  __e_acsl_store_block((void *)(& n),(size_t)4);
-  __e_acsl_store_block((void *)(& spec),(size_t)4);
-  __e_acsl_store_block((void *)(& format),(size_t)8);
-  void *p = (void *)0;
-  __e_acsl_store_block((void *)(& p),(size_t)8);
-  __e_acsl_full_init((void *)(& p));
-  __e_acsl_full_init((void *)(& tmp_1));
-  tmp_1 = __gen_e_acsl_strchr(__gen_e_acsl_literal_string_5,spec);
-  if (tmp_1 != (char *)0) __e_acsl_builtin_printf("e",(char const *)format,
-                                                  1.0);
-  else {
-    char *tmp_0;
-    __e_acsl_store_block((void *)(& tmp_0),(size_t)8);
-    __e_acsl_full_init((void *)(& tmp_0));
-    tmp_0 = __gen_e_acsl_strchr(__gen_e_acsl_literal_string_6,spec);
-    if (tmp_0 != (char *)0) __e_acsl_builtin_printf("D",(char const *)format,
-                                                    1U);
-    else {
-      char *tmp;
-      __e_acsl_store_block((void *)(& tmp),(size_t)8);
-      __e_acsl_full_init((void *)(& tmp));
-      tmp = __gen_e_acsl_strchr(__gen_e_acsl_literal_string_7,spec);
-      if (tmp != (char *)0) __e_acsl_builtin_printf("d",(char const *)format,
-                                                    97);
-      else 
-        if (spec == 's') __e_acsl_builtin_printf("s",(char const *)format,
-                                                 __gen_e_acsl_literal_string_8);
-        else 
-          if (spec == 'n') __e_acsl_builtin_printf("i",(char const *)format,
-                                                   & n);
-          else 
-            if (spec == 'p') __e_acsl_builtin_printf("p",
-                                                     (char const *)format,p);
-            else __gen_e_acsl_abort();
-      __e_acsl_delete_block((void *)(& tmp));
-    }
-    __e_acsl_delete_block((void *)(& tmp_0));
-  }
-  __e_acsl_delete_block((void *)(& spec));
-  __e_acsl_delete_block((void *)(& format));
-  __e_acsl_delete_block((void *)(& tmp_1));
-  __e_acsl_delete_block((void *)(& p));
-  __e_acsl_delete_block((void *)(& n));
-  return;
-}
-
-/*@ assigns \nothing; */
- __attribute__((__FC_BUILTIN__)) void __e_acsl_delete_block(void *);
-
-/* compiler builtin: 
-   void *__builtin_alloca(unsigned long);   */
-void test_specifier_application(char const *allowed, char const *fmt,
-                                int only_negative, char *at)
-{
-  size_t tmp;
-  unsigned long __lengthof_format;
-  __e_acsl_store_block((void *)(& __lengthof_format),(size_t)8);
-  __e_acsl_store_block((void *)(& tmp),(size_t)8);
-  __e_acsl_store_block((void *)(& at),(size_t)8);
-  __e_acsl_store_block((void *)(& only_negative),(size_t)4);
-  __e_acsl_store_block((void *)(& fmt),(size_t)8);
-  __e_acsl_store_block((void *)(& allowed),(size_t)8);
-  __e_acsl_full_init((void *)(& tmp));
-  tmp = __gen_e_acsl_strlen(fmt);
-  int len = (int)tmp;
-  __e_acsl_store_block((void *)(& len),(size_t)4);
-  __e_acsl_full_init((void *)(& len));
-  /*@ assert
-      alloca_bounds: 0 < sizeof(char) * (len + 1) ≤ 18446744073709551615;
-  */
-  {
-    int __gen_e_acsl_and;
-    if (0L < 1L * (len + 1L)) {
-      __e_acsl_mpz_t __gen_e_acsl_;
-      __e_acsl_mpz_t __gen_e_acsl__2;
-      int __gen_e_acsl_le;
-      __gmpz_init_set_si(__gen_e_acsl_,1L * (len + 1L));
-      __gmpz_init_set_ui(__gen_e_acsl__2,18446744073709551615UL);
-      __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_),
-                                   (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
-      __gen_e_acsl_and = __gen_e_acsl_le <= 0;
-      __gmpz_clear(__gen_e_acsl_);
-      __gmpz_clear(__gen_e_acsl__2);
-    }
-    else __gen_e_acsl_and = 0;
-    __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",
-                    (char *)"test_specifier_application",
-                    (char *)"alloca_bounds: 0 < sizeof(char) * (len + 1) <= 18446744073709551615",
-                    82);
-  }
-  __e_acsl_full_init((void *)(& __lengthof_format));
-  __lengthof_format = (unsigned long)(len + 1);
-  char *format = __builtin_alloca(sizeof(char) * __lengthof_format);
-  __e_acsl_store_block((void *)format,sizeof(char) * __lengthof_format);
-  __e_acsl_store_block((void *)(& format),(size_t)8);
-  __e_acsl_full_init((void *)(& format));
-  __gen_e_acsl_strcpy(format,fmt);
-  {
-    int i_0 = 0;
-    __e_acsl_store_block((void *)(& i_0),(size_t)4);
-    __e_acsl_full_init((void *)(& i_0));
-    while (1) {
-      size_t tmp_3;
-      __e_acsl_store_block((void *)(& tmp_3),(size_t)8);
-      __e_acsl_full_init((void *)(& tmp_3));
-      tmp_3 = __gen_e_acsl_strlen(valid_specifiers);
-      ;
-      if (! ((size_t)i_0 < tmp_3)) {
-        __e_acsl_delete_block((void *)(& tmp_3));
-        break;
-      }
-      {
-        char *tmp_2;
-        __e_acsl_store_block((void *)(& tmp_2),(size_t)8);
-        int c = (int)*(valid_specifiers + i_0);
-        __e_acsl_store_block((void *)(& c),(size_t)4);
-        __e_acsl_full_init((void *)(& c));
-        __e_acsl_initialize((void *)(format + (len - 1)),sizeof(char));
-        *(format + (len - 1)) = (char)c;
-        __e_acsl_full_init((void *)(& tmp_2));
-        tmp_2 = __gen_e_acsl_strchr(allowed,c);
-        if (tmp_2) {
-          if (! only_negative) {
-            {
-              pid_t pid = fork();
-              __e_acsl_store_block((void *)(& pid),(size_t)4);
-              __e_acsl_full_init((void *)(& pid));
-              if (! pid) {
-                apply_specifier(format,c);
-                __gen_e_acsl_exit(0);
-              }
-              else {
-                int process_status;
-                __e_acsl_store_block((void *)(& process_status),(size_t)4);
-                waitpid(pid,& process_status,0);
-                signal_eval(process_status,0,(char const *)at);
-                __e_acsl_delete_block((void *)(& process_status));
-              }
-              __e_acsl_delete_block((void *)(& pid));
-            }
-          }
-        }
-        else {
-          {
-            pid_t pid_0 = fork();
-            __e_acsl_store_block((void *)(& pid_0),(size_t)4);
-            __e_acsl_full_init((void *)(& pid_0));
-            if (! pid_0) {
-              apply_specifier(format,c);
-              __gen_e_acsl_exit(0);
-            }
-            else {
-              int process_status_0;
-              __e_acsl_store_block((void *)(& process_status_0),(size_t)4);
-              waitpid(pid_0,& process_status_0,0);
-              signal_eval(process_status_0,1,(char const *)at);
-              __e_acsl_delete_block((void *)(& process_status_0));
-            }
-            __e_acsl_delete_block((void *)(& pid_0));
-          }
-        }
-        __e_acsl_delete_block((void *)(& tmp_2));
-        __e_acsl_delete_block((void *)(& c));
-      }
-      __e_acsl_full_init((void *)(& i_0));
-      i_0 ++;
-      __e_acsl_delete_block((void *)(& tmp_3));
-    }
-    __e_acsl_delete_block((void *)(& i_0));
-  }
-  __e_acsl_delete_block((void *)format);
-  __e_acsl_delete_block((void *)(& at));
-  __e_acsl_delete_block((void *)(& only_negative));
-  __e_acsl_delete_block((void *)(& fmt));
-  __e_acsl_delete_block((void *)(& allowed));
-  __e_acsl_delete_block((void *)(& __lengthof_format));
-  __e_acsl_delete_block((void *)(& format));
-  __e_acsl_delete_block((void *)(& tmp));
-  __e_acsl_delete_block((void *)(& len));
-  return;
-}
-
-void __e_acsl_globals_init(void)
-{
-  __gen_e_acsl_literal_string_6 = "uoxX";
-  __e_acsl_store_block((void *)__gen_e_acsl_literal_string_6,sizeof("uoxX"));
-  __e_acsl_full_init((void *)__gen_e_acsl_literal_string_6);
-  __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_6);
-  __gen_e_acsl_literal_string_8 = "foo";
-  __e_acsl_store_block((void *)__gen_e_acsl_literal_string_8,sizeof("foo"));
-  __e_acsl_full_init((void *)__gen_e_acsl_literal_string_8);
-  __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_8);
-  __gen_e_acsl_literal_string_5 = "fFeEgGaA";
-  __e_acsl_store_block((void *)__gen_e_acsl_literal_string_5,
-                       sizeof("fFeEgGaA"));
-  __e_acsl_full_init((void *)__gen_e_acsl_literal_string_5);
-  __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_5);
-  __gen_e_acsl_literal_string_9 = "diouxfFeEgGaAcspn";
-  __e_acsl_store_block((void *)__gen_e_acsl_literal_string_9,
-                       sizeof("diouxfFeEgGaAcspn"));
-  __e_acsl_full_init((void *)__gen_e_acsl_literal_string_9);
-  __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_9);
-  __gen_e_acsl_literal_string_7 = "dic";
-  __e_acsl_store_block((void *)__gen_e_acsl_literal_string_7,sizeof("dic"));
-  __e_acsl_full_init((void *)__gen_e_acsl_literal_string_7);
-  __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_7);
-  __gen_e_acsl_literal_string = "OK: expected signal at %s\n";
-  __e_acsl_store_block((void *)__gen_e_acsl_literal_string,
-                       sizeof("OK: expected signal at %s\n"));
-  __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
-  __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
-  __gen_e_acsl_literal_string_2 = "OK: Expected execution at %s\n";
-  __e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,
-                       sizeof("OK: Expected execution at %s\n"));
-  __e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
-  __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_2);
-  __gen_e_acsl_literal_string_4 = "FAIL: Unexpected signal at %s\n";
-  __e_acsl_store_block((void *)__gen_e_acsl_literal_string_4,
-                       sizeof("FAIL: Unexpected signal at %s\n"));
-  __e_acsl_full_init((void *)__gen_e_acsl_literal_string_4);
-  __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_4);
-  __gen_e_acsl_literal_string_3 = "FAIL: Unexpected execution at %s\n";
-  __e_acsl_store_block((void *)__gen_e_acsl_literal_string_3,
-                       sizeof("FAIL: Unexpected execution at %s\n"));
-  __e_acsl_full_init((void *)__gen_e_acsl_literal_string_3);
-  __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_3);
-  __e_acsl_store_block((void *)(& __gen_e_acsl_strcpy),(size_t)1);
-  __e_acsl_full_init((void *)(& __gen_e_acsl_strcpy));
-  __e_acsl_store_block((void *)(& __gen_e_acsl_strchr),(size_t)1);
-  __e_acsl_full_init((void *)(& __gen_e_acsl_strchr));
-  __e_acsl_store_block((void *)(& __gen_e_acsl_strlen),(size_t)1);
-  __e_acsl_full_init((void *)(& __gen_e_acsl_strlen));
-  __e_acsl_store_block((void *)(& __gen_e_acsl_exit),(size_t)1);
-  __e_acsl_full_init((void *)(& __gen_e_acsl_exit));
-  __e_acsl_store_block((void *)(& __gen_e_acsl_abort),(size_t)1);
-  __e_acsl_full_init((void *)(& __gen_e_acsl_abort));
-  __e_acsl_store_block((void *)(& test_specifier_application),(size_t)1);
-  __e_acsl_full_init((void *)(& test_specifier_application));
-  __e_acsl_store_block((void *)(& apply_specifier),(size_t)1);
-  __e_acsl_full_init((void *)(& apply_specifier));
-  __e_acsl_store_block((void *)(& valid_specifiers),(size_t)8);
-  __e_acsl_full_init((void *)(& valid_specifiers));
-  __e_acsl_store_block((void *)(& signal_eval),(size_t)1);
-  __e_acsl_full_init((void *)(& signal_eval));
-  __e_acsl_store_block((void *)(& __fc_p_time_tm),(size_t)8);
-  __e_acsl_full_init((void *)(& __fc_p_time_tm));
-  __e_acsl_store_block((void *)(& __fc_time_tm),(size_t)36);
-  __e_acsl_full_init((void *)(& __fc_time_tm));
-  __e_acsl_store_block((void *)(__fc_fds),(size_t)4096);
-  __e_acsl_full_init((void *)(& __fc_fds));
-  __e_acsl_store_block((void *)(& __fc_fds_state),(size_t)4);
-  __e_acsl_full_init((void *)(& __fc_fds_state));
-  __e_acsl_store_block((void *)(& __fc_time),(size_t)4);
-  __e_acsl_full_init((void *)(& __fc_time));
-  __e_acsl_store_block((void *)(& __fc_p_fopen),(size_t)8);
-  __e_acsl_full_init((void *)(& __fc_p_fopen));
-  __e_acsl_store_block((void *)(__fc_fopen),(size_t)4096);
-  __e_acsl_full_init((void *)(& __fc_fopen));
-  __e_acsl_store_block((void *)(& __fc_rand_max),(size_t)8);
-  __e_acsl_full_init((void *)(& __fc_rand_max));
-  return;
-}
-
-int main(int argc, char const **argv)
-{
-  int __retres;
-  __e_acsl_memory_init(& argc,(char ***)(& argv),(size_t)8);
-  __e_acsl_globals_init();
-  __e_acsl_store_block((void *)(& __retres),(size_t)4);
-  __e_acsl_full_init((void *)(& __retres));
-  __retres = 0;
-  __e_acsl_delete_block((void *)(& argv));
-  __e_acsl_delete_block((void *)(& argc));
-  __e_acsl_delete_block((void *)(& test_specifier_application));
-  __e_acsl_delete_block((void *)(& apply_specifier));
-  __e_acsl_delete_block((void *)(& valid_specifiers));
-  __e_acsl_delete_block((void *)(& signal_eval));
-  __e_acsl_delete_block((void *)(& __fc_p_time_tm));
-  __e_acsl_delete_block((void *)(& __fc_time_tm));
-  __e_acsl_delete_block((void *)(__fc_fds));
-  __e_acsl_delete_block((void *)(& __fc_fds_state));
-  __e_acsl_delete_block((void *)(& __fc_time));
-  __e_acsl_delete_block((void *)(& __fc_p_fopen));
-  __e_acsl_delete_block((void *)(__fc_fopen));
-  __e_acsl_delete_block((void *)(& __fc_rand_max));
-  __e_acsl_delete_block((void *)(& __retres));
-  __e_acsl_memory_clean();
-  return __retres;
-}
-
-

src/plugins/e-acsl/tests/format/oracle_ci/printf.0.res.oracle

-[e-acsl] beginning translation.
-[e-acsl] warning: annotating undefined function `abort':
-                  the generated program may miss memory instrumentation
-                  if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `exit':
-                  the generated program may miss memory instrumentation
-                  if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `strlen':
-                  the generated program may miss memory instrumentation
-                  if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `strchr':
-                  the generated program may miss memory instrumentation
-                  if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `strcpy':
-                  the generated program may miss memory instrumentation
-                  if there are memory-related annotations.
-FRAMAC_SHARE/libc/stdio.h:150:[kernel] warning: Neither code nor specification for function printf, generating default assigns from the prototype
-FRAMAC_SHARE/libc/unistd.h:785:[kernel] warning: Neither code nor specification for function fork, generating default assigns from the prototype
-FRAMAC_SHARE/libc/sys/wait.h:57:[kernel] warning: Neither code nor specification for function waitpid, generating default assigns from the prototype
-:0:[kernel] warning: Neither code nor specification for function __fc_vla_free, generating default assigns from the prototype
-:0:[kernel] warning: Neither code nor specification for function __fc_vla_alloc, generating default assigns from the prototype
-FRAMAC_SHARE/libc/string.h:221:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:222:[e-acsl] warning: E-ACSL construct `trange' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:224:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:224:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:227:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:227:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:124:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:127:[e-acsl] warning: E-ACSL construct `user-defined logic type' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:134:[e-acsl] warning: E-ACSL construct `user-defined logic type' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:92:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:92:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:94:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:94:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:396:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
-                  Ignoring annotation.
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value:initial-state] Values of globals at initialization
-  __fc_rand_max ∈ {32767}
-  __fc_heap_status ∈ [--..--]
-  __e_acsl_init ∈ [--..--]
-  __fc_fopen[0..511] ∈ {0}
-  __fc_p_fopen ∈ {{ &__fc_fopen[0] }}
-  __e_acsl_internal_heap ∈ [--..--]
-  __e_acsl_heap_allocation_size ∈ [--..--]
-  __e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
-  __e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
-  __e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
-  __fc_time ∈ [--..--]
-  __fc_fds_state ∈ [--..--]
-  __fc_fds[0..1023] ∈ {0}
-  __fc_time_tm ∈ {0}
-  __fc_p_time_tm ∈ {{ &__fc_time_tm }}
-  valid_specifiers ∈ {{ "diouxfFeEgGaAcspn" }}
-  __gen_e_acsl_literal_string ∈ {0}
-  __gen_e_acsl_literal_string_2 ∈ {0}
-  __gen_e_acsl_literal_string_3 ∈ {0}
-  __gen_e_acsl_literal_string_4 ∈ {0}
-  __gen_e_acsl_literal_string_5 ∈ {0}
-  __gen_e_acsl_literal_string_6 ∈ {0}
-  __gen_e_acsl_literal_string_7 ∈ {0}
-  __gen_e_acsl_literal_string_8 ∈ {0}
-[value] using specification for function __e_acsl_memory_init
-[value] using specification for function __e_acsl_store_block
-[value] using specification for function __e_acsl_full_init
-[value] using specification for function __e_acsl_mark_readonly
-[value] using specification for function __e_acsl_delete_block
-[value] using specification for function __e_acsl_memory_clean
-[value] done for function main

src/plugins/e-acsl/tests/format/oracle_ci/printf.1.res.oracle

-[e-acsl] beginning translation.
-[e-acsl] warning: annotating undefined function `abort':
-                  the generated program may miss memory instrumentation
-                  if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `exit':
-                  the generated program may miss memory instrumentation
-                  if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `strlen':
-                  the generated program may miss memory instrumentation
-                  if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `strchr':
-                  the generated program may miss memory instrumentation
-                  if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `strcpy':
-                  the generated program may miss memory instrumentation
-                  if there are memory-related annotations.
-FRAMAC_SHARE/libc/stdio.h:150:[kernel] warning: Neither code nor specification for function printf, generating default assigns from the prototype
-FRAMAC_SHARE/libc/unistd.h:785:[kernel] warning: Neither code nor specification for function fork, generating default assigns from the prototype
-FRAMAC_SHARE/libc/sys/wait.h:57:[kernel] warning: Neither code nor specification for function waitpid, generating default assigns from the prototype
-:0:[kernel] warning: Neither code nor specification for function __fc_vla_free, generating default assigns from the prototype
-:0:[kernel] warning: Neither code nor specification for function __fc_vla_alloc, generating default assigns from the prototype
-FRAMAC_SHARE/libc/string.h:221:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:222:[e-acsl] warning: E-ACSL construct `trange' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:224:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:224:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:227:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:227:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:124:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:127:[e-acsl] warning: E-ACSL construct `user-defined logic type' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:134:[e-acsl] warning: E-ACSL construct `user-defined logic type' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:92:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:92:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:94:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:94:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:396:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
-                  Ignoring annotation.
-[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value:initial-state] Values of globals at initialization
-  __fc_rand_max ∈ {32767}
-  __fc_heap_status ∈ [--..--]
-  __e_acsl_init ∈ [--..--]
-  __fc_fopen[0..511] ∈ {0}
-  __fc_p_fopen ∈ {{ &__fc_fopen[0] }}
-  __e_acsl_internal_heap ∈ [--..--]
-  __e_acsl_heap_allocation_size ∈ [--..--]
-  __e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
-  __e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
-  __e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
-  __fc_time ∈ [--..--]
-  __fc_fds_state ∈ [--..--]
-  __fc_fds[0..1023] ∈ {0}
-  __fc_time_tm ∈ {0}
-  __fc_p_time_tm ∈ {{ &__fc_time_tm }}
-  valid_specifiers ∈ {{ "diouxfFeEgGaAcspn" }}
-  __gen_e_acsl_literal_string ∈ {0}
-  __gen_e_acsl_literal_string_2 ∈ {0}
-  __gen_e_acsl_literal_string_3 ∈ {0}
-  __gen_e_acsl_literal_string_4 ∈ {0}
-  __gen_e_acsl_literal_string_5 ∈ {0}
-  __gen_e_acsl_literal_string_6 ∈ {0}
-  __gen_e_acsl_literal_string_7 ∈ {0}
-  __gen_e_acsl_literal_string_8 ∈ {0}
-  __gen_e_acsl_literal_string_9 ∈ {0}
-[value] using specification for function __e_acsl_memory_init
-[value] using specification for function __e_acsl_store_block
-[value] using specification for function __e_acsl_full_init
-[value] using specification for function __e_acsl_mark_readonly
-[value] using specification for function __e_acsl_delete_block
-[value] using specification for function __e_acsl_memory_clean
-[value] done for function main

src/plugins/e-acsl/tests/format/oracle_dev/fprintf.res.oracle

-[kernel] Parsing tests/format/fprintf.c (with preprocessing)