Merge branch 'kostyantyn/feature/safeloc' into 'master'

Safe locations in RTL

This merge request fixes issues with `errno` and `ctype.h` macros in Patricia Trie RTL

See merge request !90

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

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

+/* 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;
+}

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/ctype_macros.res.oracle

+[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.)

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_ctype_macros.c

+/* 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;
+}
+
+

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;
+}
+
+