Added test case for errno

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

+/* run.config
+   COMMENT: Check whether location of errno is recorded
+*/
+
+#include <errno.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+int main(int argc, const char **argv) {
+  int *p = &errno;
+  /*@ assert \valid(p); */
+  return 0;
+}

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

+[e-acsl] beginning translation.
+FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+[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.

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

+/* Generated by Frama-C */
+void __e_acsl_globals_init(void)
+{
+  __e_acsl_store_block((void *)(& __FC_errno),4UL);
+  __e_acsl_full_init((void *)(& __FC_errno));
+  return;
+}
+
+int main(int argc, char const **argv)
+{
+  int __retres;
+  int *p;
+  __e_acsl_memory_init(& argc,(char ***)(& argv),8UL);
+  __e_acsl_globals_init();
+  __e_acsl_store_block((void *)(& p),8UL);
+  __e_acsl_full_init((void *)(& p));
+  p = & __FC_errno;
+  /*@ assert \valid(p); */
+  {
+    int __gen_e_acsl_initialized;
+    int __gen_e_acsl_and;
+    __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& p),
+                                                    sizeof(int *));
+    if (__gen_e_acsl_initialized) {
+      int __gen_e_acsl_valid;
+      __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int));
+      __gen_e_acsl_and = __gen_e_acsl_valid;
+    }
+    else __gen_e_acsl_and = 0;
+    __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",(char *)"main",
+                    (char *)"\\valid(p)",11);
+  }
+  __retres = 0;
+  __e_acsl_delete_block((void *)(& __FC_errno));
+  __e_acsl_delete_block((void *)(& p));
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+