From 279b5a45b949ccefb9095c7c7d67e6fa9c2b4d10 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Tue, 13 Sep 2016 10:36:19 +0200
Subject: [PATCH] Added bts 2192 test case
---
src/plugins/e-acsl/tests/bts/bts2192.c | 11 +++++++++++
.../e-acsl/tests/bts/oracle/bts2192.err.oracle | 0
.../e-acsl/tests/bts/oracle/bts2192.res.oracle | 6 ++++++
src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c | 15 +++++++++++++++
4 files changed, 32 insertions(+)
create mode 100644 src/plugins/e-acsl/tests/bts/bts2192.c
create mode 100644 src/plugins/e-acsl/tests/bts/oracle/bts2192.err.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c
diff --git a/src/plugins/e-acsl/tests/bts/bts2192.c b/src/plugins/e-acsl/tests/bts/bts2192.c
new file mode 100644
index 00000000000..89fdf25dae7
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/bts2192.c
@@ -0,0 +1,11 @@
+/* run.config
+ COMMENT: bts #2292, failures due to unregistered RTL functions
+*/
+
+#include <stdlib.h>
+
+int a;
+char *n = "134";
+int main(int argc, char **argv) {
+ a = argc = atoi(n);
+}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2192.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2192.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle
new file mode 100644
index 00000000000..d122567f658
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle
@@ -0,0 +1,6 @@
+[e-acsl] beginning translation.
+[e-acsl] warning: annotating undefined function `atoi':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+FRAMAC_SHARE/libc/stdlib.h:160:[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".
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c
new file mode 100644
index 00000000000..85c23235916
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c
@@ -0,0 +1,15 @@
+/* Generated by Frama-C */
+int a;
+char *n = (char *)"134";
+int main(int argc, char **argv)
+{
+ int __retres;
+ { /* sequence */
+ argc = __gen_e_acsl_atoi((char const *)n);
+ a = argc;
+ }
+ __retres = 0;
+ return __retres;
+}
+
+
--
GitLab