Merge branch 'bugfix/fonenantsoa/bts2386' into 'master'

Subtraction between pointers gives integer.

See merge request frama-c/e-acsl!246

src/plugins/e-acsl/doc/Changelog

@@ -19,6 +19,8 @@
 #   configure	configure
 ###############################################################################
 
+-* E-ACSL       [2018/10/04] Fix bug #2386 about incorrect typing when
+                performing pointer subtraction.
 -* E-ACSL       [2018/10/04] Support for \at on purely logic variables.
                 Fix bug #1762 about out-of-scope variables when using \old.
 *  E-ACSL       [2018/10/02] Fix bug #2305 about taking the address of a

src/plugins/e-acsl/tests/bts/bts2386.c

+/* run.config, run.config_2
+   COMMENT: pointer substraction
+   COMMENT: on gcc_x86_64
+   LOG: gen_@PTEST_NAME@.c
+   OPT: -machdep gcc_x86_64 -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/bts/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -value-verbose 0
+   COMMENT: on x86_32 (default case when no machdep is given)
+   LOG: gen_@PTEST_NAME@_2.c
+   OPT: -machdep x86_32 -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/bts/result/gen_@PTEST_NAME@_2.c -kernel-verbose 0 -val -value-verbose 0
+   COMMENT: with "-e-acsl-gmp-only"
+   LOG: gen_@PTEST_NAME@_3.c
+   OPT: -e-acsl -e-acsl-gmp-only -then-last -load-script tests/print.cmxs -print -ocode tests/bts/result/gen_@PTEST_NAME@_3.c -kernel-verbose 0 -val -value-verbose 0
+*/
+
+void f(const void *s, int c, unsigned long n) {
+  const unsigned char *p = s;
+  /*@ assert p - s == n - n; */
+  /*@ assert p - s == 0; */
+}
+
+int main() {
+  const char *s = "1234567890";
+  f(s, '0', 11);
+  return 0;
+}
\ No newline at end of file

src/plugins/e-acsl/tests/bts/oracle/bts2386.0.res.oracle

+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/bts/bts2386.c:16: Warning: 
+  function __e_acsl_assert: precondition got status unknown.

src/plugins/e-acsl/tests/bts/oracle/bts2386.1.res.oracle

+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".

src/plugins/e-acsl/tests/bts/oracle/bts2386.2.res.oracle

+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/bts/bts2386.c:16: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/bts/bts2386.c:17: Warning: 
+  function __e_acsl_assert: precondition got status unknown.

src/plugins/e-acsl/tests/bts/oracle/gen_bts2386.c

+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+char *__gen_e_acsl_literal_string;
+void f(void const *s, int c, unsigned long n)
+{
+  __e_acsl_store_block((void *)(& s),(size_t)8);
+  unsigned char const *p = (unsigned char const *)s;
+  __e_acsl_store_block((void *)(& p),(size_t)8);
+  __e_acsl_full_init((void *)(& p));
+  /*@ assert p - (unsigned char const *)s ≡ n - n; */
+  {
+    __e_acsl_mpz_t __gen_e_acsl_;
+    __e_acsl_mpz_t __gen_e_acsl_n;
+    __e_acsl_mpz_t __gen_e_acsl_sub;
+    int __gen_e_acsl_eq;
+    __gmpz_init_set_ui(__gen_e_acsl_,p - (unsigned char const *)s);
+    __gmpz_init_set_ui(__gen_e_acsl_n,n);
+    __gmpz_init(__gen_e_acsl_sub);
+    __gmpz_sub(__gen_e_acsl_sub,
+               (__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
+               (__e_acsl_mpz_struct const *)(__gen_e_acsl_n));
+    __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_),
+                                 (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub));
+    __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"f",
+                    (char *)"p - (unsigned char const *)s == n - n",16);
+    __gmpz_clear(__gen_e_acsl_);
+    __gmpz_clear(__gen_e_acsl_n);
+    __gmpz_clear(__gen_e_acsl_sub);
+  }
+  /*@ assert p - (unsigned char const *)s ≡ 0; */
+  __e_acsl_assert(p - (unsigned char const *)s == 0UL,(char *)"Assertion",
+                  (char *)"f",(char *)"p - (unsigned char const *)s == 0",17);
+  __e_acsl_delete_block((void *)(& s));
+  __e_acsl_delete_block((void *)(& p));
+  return;
+}
+
+void __e_acsl_globals_init(void)
+{
+  __gen_e_acsl_literal_string = "1234567890";
+  __e_acsl_store_block((void *)__gen_e_acsl_literal_string,
+                       sizeof("1234567890"));
+  __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
+  __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
+  return;
+}
+
+int main(void)
+{
+  int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+  __e_acsl_globals_init();
+  char const *s = __gen_e_acsl_literal_string;
+  __e_acsl_store_block((void *)(& s),(size_t)8);
+  __e_acsl_full_init((void *)(& s));
+  f((void const *)s,'0',(unsigned long)11);
+  __retres = 0;
+  __e_acsl_delete_block((void *)(& s));
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+

src/plugins/e-acsl/tests/bts/oracle/gen_bts2386_2.c

+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+char *__gen_e_acsl_literal_string;
+void f(void const *s, int c, unsigned long n)
+{
+  __e_acsl_store_block((void *)(& s),(size_t)4);
+  unsigned char const *p = (unsigned char const *)s;
+  __e_acsl_store_block((void *)(& p),(size_t)4);
+  __e_acsl_full_init((void *)(& p));
+  /*@ assert p - (unsigned char const *)s ≡ n - n; */
+  __e_acsl_assert(p - (unsigned char const *)s == n - (long long)n,
+                  (char *)"Assertion",(char *)"f",
+                  (char *)"p - (unsigned char const *)s == n - n",16);
+  /*@ assert p - (unsigned char const *)s ≡ 0; */
+  __e_acsl_assert(p - (unsigned char const *)s == 0U,(char *)"Assertion",
+                  (char *)"f",(char *)"p - (unsigned char const *)s == 0",17);
+  __e_acsl_delete_block((void *)(& s));
+  __e_acsl_delete_block((void *)(& p));
+  return;
+}
+
+void __e_acsl_globals_init(void)
+{
+  __gen_e_acsl_literal_string = "1234567890";
+  __e_acsl_store_block((void *)__gen_e_acsl_literal_string,
+                       sizeof("1234567890"));
+  __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
+  __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
+  return;
+}
+
+int main(void)
+{
+  int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)4);
+  __e_acsl_globals_init();
+  char const *s = __gen_e_acsl_literal_string;
+  __e_acsl_store_block((void *)(& s),(size_t)4);
+  __e_acsl_full_init((void *)(& s));
+  f((void const *)s,'0',(unsigned long)11);
+  __retres = 0;
+  __e_acsl_delete_block((void *)(& s));
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+

src/plugins/e-acsl/tests/bts/oracle/gen_bts2386_3.c

+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+char *__gen_e_acsl_literal_string;
+void f(void const *s, int c, unsigned long n)
+{
+  __e_acsl_store_block((void *)(& s),(size_t)4);
+  unsigned char const *p = (unsigned char const *)s;
+  __e_acsl_store_block((void *)(& p),(size_t)4);
+  __e_acsl_full_init((void *)(& p));
+  /*@ assert p - (unsigned char const *)s ≡ n - n; */
+  {
+    __e_acsl_mpz_t __gen_e_acsl_;
+    __e_acsl_mpz_t __gen_e_acsl_n;
+    __e_acsl_mpz_t __gen_e_acsl_sub;
+    int __gen_e_acsl_eq;
+    __gmpz_init_set_ui(__gen_e_acsl_,
+                       (unsigned long)(p - (unsigned char const *)s));
+    __gmpz_init_set_ui(__gen_e_acsl_n,n);
+    __gmpz_init(__gen_e_acsl_sub);
+    __gmpz_sub(__gen_e_acsl_sub,
+               (__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
+               (__e_acsl_mpz_struct const *)(__gen_e_acsl_n));
+    __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_),
+                                 (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub));
+    __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"f",
+                    (char *)"p - (unsigned char const *)s == n - n",16);
+    __gmpz_clear(__gen_e_acsl_);
+    __gmpz_clear(__gen_e_acsl_n);
+    __gmpz_clear(__gen_e_acsl_sub);
+  }
+  /*@ assert p - (unsigned char const *)s ≡ 0; */
+  {
+    __e_acsl_mpz_t __gen_e_acsl__2;
+    __e_acsl_mpz_t __gen_e_acsl__3;
+    int __gen_e_acsl_eq_2;
+    __gmpz_init_set_ui(__gen_e_acsl__2,
+                       (unsigned long)(p - (unsigned char const *)s));
+    __gmpz_init_set_si(__gen_e_acsl__3,0L);
+    __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__2),
+                                   (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
+    __e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",(char *)"f",
+                    (char *)"p - (unsigned char const *)s == 0",17);
+    __gmpz_clear(__gen_e_acsl__2);
+    __gmpz_clear(__gen_e_acsl__3);
+  }
+  __e_acsl_delete_block((void *)(& s));
+  __e_acsl_delete_block((void *)(& p));
+  return;
+}
+
+void __e_acsl_globals_init(void)
+{
+  __gen_e_acsl_literal_string = "1234567890";
+  __e_acsl_store_block((void *)__gen_e_acsl_literal_string,
+                       sizeof("1234567890"));
+  __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
+  __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
+  return;
+}
+
+int main(void)
+{
+  int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)4);
+  __e_acsl_globals_init();
+  char const *s = __gen_e_acsl_literal_string;
+  __e_acsl_store_block((void *)(& s),(size_t)4);
+  __e_acsl_full_init((void *)(& s));
+  f((void const *)s,'0',(unsigned long)11);
+  __retres = 0;
+  __e_acsl_delete_block((void *)(& s));
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+

src/plugins/e-acsl/translate.ml

@@ -483,7 +483,7 @@ and context_insensitive_term_to_exp kf env t =
   | TBinOp((BOr | BXor | BAnd), _, _) ->
     (* other logic/arith operators  *)
     not_yet env "missing binary bitwise operator"
-  | TBinOp(PlusPI | IndexPI | MinusPI | MinusPP as bop, t1, t2) ->
+  | TBinOp(PlusPI | IndexPI | MinusPI as bop, t1, t2) ->
     if Misc.is_set_of_ptr_or_array t1.term_type ||
       Misc.is_set_of_ptr_or_array t2.term_type then
         (* case of arithmetic over set of pointers (due to use of ranges)
@@ -497,6 +497,18 @@ and context_insensitive_term_to_exp kf env t =
     let e1, env = term_to_exp kf env t1 in
     let e2, env = term_to_exp kf env t2 in
     Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)), env, false, ""
+  | TBinOp(MinusPP, t1, t2) ->
+    begin match Typing.get_integer_ty t with
+      | Typing.C_type _ ->
+        let e1, env = term_to_exp kf env t1 in
+        let e2, env = term_to_exp kf env t2 in
+        let ty = Typing.get_typ t in
+        Cil.new_exp ~loc (BinOp(MinusPP, e1, e2, ty)), env, false, ""
+      | Typing.Gmp ->
+        not_yet env "pointer subtraction resulting in gmp"
+      | Typing.Other ->
+        assert false
+    end
   | TCastE(ty, t') ->
     let e, env = term_to_exp kf env t' in
     let e, env = add_cast ~loc ~name:"cast" env (Some ty) false (Some t) e in