From 44ec56a40e73dc97210396729bbad0764d8018a7 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Tue, 22 Nov 2016 17:56:33 +0100
Subject: [PATCH] Added test case for errno
---
src/plugins/e-acsl/tests/runtime/errno.c | 13 ++++++
.../tests/runtime/oracle/errno.err.oracle | 0
.../tests/runtime/oracle/errno.res.oracle | 4 ++
.../e-acsl/tests/runtime/oracle/gen_errno.c | 40 +++++++++++++++++++
4 files changed, 57 insertions(+)
create mode 100644 src/plugins/e-acsl/tests/runtime/errno.c
create mode 100644 src/plugins/e-acsl/tests/runtime/oracle/errno.err.oracle
create mode 100644 src/plugins/e-acsl/tests/runtime/oracle/errno.res.oracle
create mode 100644 src/plugins/e-acsl/tests/runtime/oracle/gen_errno.c
diff --git a/src/plugins/e-acsl/tests/runtime/errno.c b/src/plugins/e-acsl/tests/runtime/errno.c
new file mode 100644
index 00000000000..6cd40348bb2
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/errno.c
@@ -0,0 +1,13 @@
+/* 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;
+}
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/errno.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/errno.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/errno.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/errno.res.oracle
new file mode 100644
index 00000000000..74b2c0f8866
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/oracle/errno.res.oracle
@@ -0,0 +1,4 @@
+[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.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_errno.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_errno.c
new file mode 100644
index 00000000000..9ed31d52411
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_errno.c
@@ -0,0 +1,40 @@
+/* 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;
+}
+
+
--
GitLab