diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 4adf3772d04bbd70aff6198441d842f4e4728849..28491dc946d12ff5e0477f746c16667acd265071 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/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
diff --git a/src/plugins/e-acsl/tests/bts/bts2386.c b/src/plugins/e-acsl/tests/bts/bts2386.c
new file mode 100644
index 0000000000000000000000000000000000000000..a401b20823cd417e42a59a1a715fedb30bbc8d89
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/bts2386.c
@@ -0,0 +1,24 @@
+/* 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
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2386.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2386.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..3ca31dcb9c97db331c81385797932d2c038224e4
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts2386.0.res.oracle
@@ -0,0 +1,4 @@
+[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.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2386.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2386.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..efd026311297e55d8fefb674326118e6ece88624
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts2386.1.res.oracle
@@ -0,0 +1,2 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2386.2.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2386.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..164b435ffa8cf0a6fb91adc0137d5ff98940874e
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts2386.2.res.oracle
@@ -0,0 +1,6 @@
+[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.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2386.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2386.c
new file mode 100644
index 0000000000000000000000000000000000000000..d47410c51d3b6a88f4df8a59814d623ad2c2c78e
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2386.c
@@ -0,0 +1,64 @@
+/* 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;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2386_2.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2386_2.c
new file mode 100644
index 0000000000000000000000000000000000000000..2a19e9fec90cc827e3934db39135b12a1e85ebfa
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2386_2.c
@@ -0,0 +1,48 @@
+/* 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;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2386_3.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2386_3.c
new file mode 100644
index 0000000000000000000000000000000000000000..d47595442fc7d28e0b3d52165a7d75142d1c5a54
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2386_3.c
@@ -0,0 +1,77 @@
+/* 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;
+}
+
+
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 8afed8ab60fd26c4412c5a6d3b2fa3d27ac2deee..d77e94913a3f42b92033be7f940c98921a2d98d9 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/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