diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index 4ea21de6f5efe6f9e5efdbc6435afddffa90ba0f..db22eae4f35fc001b8ad8004919d763932defb50 100755
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
@@ -181,7 +181,7 @@ OPTION_EACSL="-e-acsl" # Specifies E-ACSL run
OPTION_FRAMA_STDLIB="-no-frama-c-stdlib" # Use Frama-C stdlib
OPTION_FULL_MMODEL= # Instrument as much as possible
OPTION_GMP= # Use GMP integers everywhere
-OPTION_FRAMAC_CPP_EXTRA="" # Extra CPP flags for Frama-C
+OPTION_FRAMAC_CPP_EXTRA="-D__NO_CTYPE" # Extra CPP flags for Frama-C*
OPTION_EACSL_MMODELS="bittree" # Memory model used
OPTION_EACSL_SHARE= # Custom E-ACSL share directory
OPTION_INSTRUMENTED_ONLY= # Do not compile original code
diff --git a/src/plugins/e-acsl/tests/runtime/ctype_macros.c b/src/plugins/e-acsl/tests/runtime/ctype_macros.c
new file mode 100644
index 0000000000000000000000000000000000000000..664996beecc4da2690be0ea8452617df66835f35
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/ctype_macros.c
@@ -0,0 +1,41 @@
+/* run.config
+ COMMENT: Tests for function-based implementation of ctype.h features
+*/
+
+/* ctype.h tests (e.g., `isalpha`, `isnumber` etc) in GLIBC are implemented as
+ macro-definitions featuring `__ctype_b_loc` function which returns an address
+ of an array with locale-specific data. Because of Frama-C normalization below
+ snippet:
+ char c = isupper(argc);
+ char *d = &c;
+ is approximately as follows:
+ char c;
+ unsigned short const **tmp;
+ char *d;
+ tmp = __ctype_b_loc();
+ d = &c;
+ Since no implementation of `__ctype_b_loc` is provided, its return address
+ is not recorded (the bounds of the array are also implementation specific).
+ Then, `d` points to some internal array on stack and the assertion below
+ does not hold (while it should).
+
+ This test checks that E-ACSL uses function-based implementations of ctype
+ tests (by defining __NO_CTYPE macro during preprocessing). Thus, the
+ normalized code should resemble the below snippet:
+ char c;
+ int tmp;
+ char *d;
+ tmp = isupper(argc);
+ c = (char)tmp;
+ d = & c;
+ Notably, since isupper returns an int, `d` points to `c` (on stack) and
+ therefore the assertion holds. */
+
+#include <ctype.h>
+
+int main(int argc, const char **argv) {
+ char c = isupper(argc);
+ char *d = &c;
+ /*@ assert \valid(d); */
+ return 0;
+}
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 0000000000000000000000000000000000000000..6cd40348bb2e39ca76689f198b44d834211470c1
--- /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/ctype_macros.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/ctype_macros.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/ctype_macros.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/ctype_macros.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..ae7eacf4a88348422f940dc6ba68a4969948f63c
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/oracle/ctype_macros.res.oracle
@@ -0,0 +1,12 @@
+[e-acsl] beginning translation.
+[e-acsl] warning: annotating undefined function `isupper':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+tests/runtime/ctype_macros.c:39:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+ Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
+FRAMAC_SHARE/libc/ctype.h:163:[value] warning: function __gen_e_acsl_isupper: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/libc/ctype.h:167:[value] warning: function __gen_e_acsl_isupper, behavior definitely_match: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/ctype.h:170:[value] warning: function __gen_e_acsl_isupper, behavior definitely_not_match: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
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 0000000000000000000000000000000000000000..74b2c0f88667ff0dbd307a6474a57f57cb8b45b7
--- /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_ctype_macros.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_ctype_macros.c
new file mode 100644
index 0000000000000000000000000000000000000000..c25ea39a532c8d3c3c0dda944ccaa204f1ac70f9
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_ctype_macros.c
@@ -0,0 +1,38 @@
+/* Generated by Frama-C */
+int main(int argc, char const **argv)
+{
+ int __retres;
+ char c;
+ int tmp;
+ char *d;
+ __e_acsl_memory_init(& argc,(char ***)(& argv),8UL);
+ __e_acsl_store_block((void *)(& d),8UL);
+ __e_acsl_store_block((void *)(& c),1UL);
+ tmp = __gen_e_acsl_isupper(argc);
+ __e_acsl_full_init((void *)(& c));
+ c = (char)tmp;
+ __e_acsl_full_init((void *)(& d));
+ d = & c;
+ /*@ assert \valid(d); */
+ {
+ int __gen_e_acsl_initialized;
+ int __gen_e_acsl_and;
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& d),
+ sizeof(char *));
+ if (__gen_e_acsl_initialized) {
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)d,sizeof(char));
+ __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(d)",39);
+ }
+ __retres = 0;
+ __e_acsl_delete_block((void *)(& d));
+ __e_acsl_delete_block((void *)(& c));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
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 0000000000000000000000000000000000000000..9ed31d5241175d807e3ab585fc42520275fc1940
--- /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;
+}
+
+