diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml
index 18b1377826141d01e28e5e7f4474e61cd8d2c104..1d9bd77bc5d609d0c388d032435bb4e81757a869 100644
--- a/src/plugins/e-acsl/interval.ml
+++ b/src/plugins/e-acsl/interval.ml
@@ -190,7 +190,7 @@ let rec infer t =
| Tunion _ -> Error.not_yet "tset union"
| Tinter _ -> Error.not_yet "tset intersection"
| Tcomprehension (_,_,_) -> Error.not_yet "tset comprehension"
- | Trange (_,_) -> Error.not_yet "trange"
+ | Trange (_,_) -> Ival.inject_range None None
| Tlet (li,t) ->
let li_t = Misc.term_of_li li in
diff --git a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
index 8d84c2c3338b650cba314a8fc9a998e0dda1322c..72731f940f00df5cf7fccaa6f458428c7b854c64 100644
--- a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
@@ -21,7 +21,8 @@
E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:328: Warning:
- E-ACSL construct `trange' is not yet supported. Ignoring annotation.
+ E-ACSL construct `logic function returning an integer' is not yet supported.
+ Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:330: Warning:
E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:330: Warning:
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_ranges_in_builtins.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_ranges_in_builtins.c
new file mode 100644
index 0000000000000000000000000000000000000000..08868218838618ba4c349dedee30f59d0b7a498e
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_ranges_in_builtins.c
@@ -0,0 +1,71 @@
+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+int main(void)
+{
+ int __retres;
+ int *a;
+ char *b;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_store_block((void *)(& b),(size_t)8);
+ __e_acsl_store_block((void *)(& a),(size_t)8);
+ __e_acsl_full_init((void *)(& a));
+ a = (int *)malloc((unsigned long)10 * sizeof(int));
+ /*@ assert \valid(a + (0 .. 4)); */
+ {
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)((char *)a + 4 * 0),
+ (size_t)(4 * (4 - 0)),(void *)a,
+ (void *)(& a));
+ __e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(a + (0 .. 4))",13);
+ }
+ int j = 2;
+ /*@ assert \valid(a + (4 .. 8 + j)); */
+ {
+ int __gen_e_acsl_valid_2;
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)((char *)a + 4 * 4),
+ (size_t)((int)(4 * ((8L + j) - 4))),
+ (void *)a,(void *)(& a));
+ __e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(a + (4 .. 8 + j))",15);
+ }
+ /*@ assert ¬\valid(a + (10 .. 11)); */
+ {
+ int __gen_e_acsl_valid_3;
+ __gen_e_acsl_valid_3 = __e_acsl_valid((void *)((char *)a + 4 * 10),
+ (size_t)(4 * (11 - 10)),(void *)a,
+ (void *)(& a));
+ __e_acsl_assert(! __gen_e_acsl_valid_3,(char *)"Assertion",
+ (char *)"main",(char *)"!\\valid(a + (10 .. 11))",16);
+ }
+ free((void *)a);
+ __e_acsl_full_init((void *)(& b));
+ b = (char *)malloc((unsigned long)10 * sizeof(char));
+ /*@ assert \valid(b + (0 .. 10)); */
+ {
+ int __gen_e_acsl_valid_4;
+ __gen_e_acsl_valid_4 = __e_acsl_valid((void *)(b + 1 * 0),
+ (size_t)(1 * (10 - 0)),(void *)b,
+ (void *)(& b));
+ __e_acsl_assert(__gen_e_acsl_valid_4,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(b + (0 .. 10))",21);
+ }
+ /*@ assert ¬\valid(b + (11 .. 15)); */
+ {
+ int __gen_e_acsl_valid_5;
+ __gen_e_acsl_valid_5 = __e_acsl_valid((void *)(b + 1 * 11),
+ (size_t)(1 * (15 - 11)),(void *)b,
+ (void *)(& b));
+ __e_acsl_assert(! __gen_e_acsl_valid_5,(char *)"Assertion",
+ (char *)"main",(char *)"!\\valid(b + (11 .. 15))",22);
+ }
+ free((void *)b);
+ __retres = 0;
+ __e_acsl_delete_block((void *)(& b));
+ __e_acsl_delete_block((void *)(& a));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/ranges_in_builtins.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/ranges_in_builtins.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/ranges_in_builtins.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/ranges_in_builtins.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..aa7cb1cc0b159670847cf9d9733cad1da4797d0e
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/oracle/ranges_in_builtins.res.oracle
@@ -0,0 +1,6 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/runtime/ranges_in_builtins.c:13: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/runtime/ranges_in_builtins.c:15: Warning:
+ assertion got status invalid (stopping propagation).
diff --git a/src/plugins/e-acsl/tests/runtime/ranges_in_builtins.c b/src/plugins/e-acsl/tests/runtime/ranges_in_builtins.c
new file mode 100644
index 0000000000000000000000000000000000000000..4e9b84077745bc8e6faf8c91b64a70127a6ade49
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/ranges_in_builtins.c
@@ -0,0 +1,24 @@
+/* run.config
+ COMMENT: ranges in builtins
+*/
+
+#include "stdlib.h"
+
+extern void *malloc(size_t p);
+extern void free(void* p);
+
+int main(void) {
+ int *a;
+ a = malloc(10*sizeof(int));
+ /*@ assert \valid(a + (0 .. 4)); */ ;
+ int j = 2;
+ /*@ assert \valid(a + (4 .. 8+j)); */ ;
+ /*@ assert !\valid(a + (10 .. 11)); */ ;
+ free(a);
+
+ char *b;
+ b = malloc(10*sizeof(char));
+ /*@ assert \valid(b + (0 .. 10)); */ ;
+ /*@ assert !\valid(b + (11 .. 15)); */ ;
+ free(b);
+}
\ No newline at end of file
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c
index db3449211e250fc288fea13ddad23c447bafd4c6..7eeaecdb7fd41d6d1c516231b6f790657f38525d 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c
@@ -154,7 +154,6 @@ int main(void)
__e_acsl_temporal_store_nblock((void *)(& q),(void *)*(& q));
__e_acsl_temporal_store_nblock((void *)p,(void *)(& a));
__e_acsl_initialize((void *)p,sizeof(int *));
- /*@ assert Value: mem_access: \valid(p); */
*p = & a;
__e_acsl_temporal_store_nblock((void *)(p + 1),(void *)(& a));
__e_acsl_initialize((void *)(p + 1),sizeof(int *));
@@ -237,8 +236,6 @@ int main(void)
else __gen_e_acsl_and_10 = 0;
__e_acsl_assert(__gen_e_acsl_and_10,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(q)",44);
- /*@ assert Value: initialization: \initialized(q); */
- /*@ assert Value: mem_access: \valid_read(q); */
__gen_e_acsl_valid_9 = __e_acsl_valid((void *)*q,sizeof(int),
(void *)*q,(void *)q);
__gen_e_acsl_and_11 = __gen_e_acsl_valid_9;
@@ -262,8 +259,6 @@ int main(void)
(void *)(& q));
__e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(q + 1)",45);
- /*@ assert Value: initialization: \initialized(q + 1); */
- /*@ assert Value: mem_access: \valid_read(q + 1); */
__gen_e_acsl_valid_10 = __e_acsl_valid((void *)*(q + 1),sizeof(int),
(void *)*(q + 1),
(void *)(q + 1));
@@ -278,7 +273,6 @@ int main(void)
tmp_1 = (int *)0;
__e_acsl_temporal_store_nreferent((void *)(q + 1),(void *)(& tmp_1));
__e_acsl_initialize((void *)(q + 1),sizeof(int *));
- /*@ assert Value: mem_access: \valid(q + 1); */
*(q + 1) = tmp_1;
__e_acsl_temporal_store_nreferent((void *)q,(void *)(& tmp_1));
__e_acsl_initialize((void *)q,sizeof(int *));
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
index 1ee3a3f75cca44508a2b01dd512fc7a640d32b8c..4fc4f50e6201997a2bb714a745dc15ca0e331f6d 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
@@ -7,18 +7,12 @@
if there are memory-related annotations.
[e-acsl] FRAMAC_SHARE/libc/string.h:78: Warning:
E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:101: Warning:
- E-ACSL construct `trange' is not yet supported. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:101: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:104: Warning:
E-ACSL construct `user-defined logic type' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:78: Warning:
- E-ACSL construct `trange' is not yet supported. Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:79: Warning:
- E-ACSL construct `trange' is not yet supported. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:81: Warning:
E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:81: Warning:
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index db194ddf24c866de12f554363f968aaa1ca29651..a02e378f5ae379e7312f2619319a4ae071547a7f 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -597,6 +597,68 @@ and mmodel_call_with_size ~loc kf name ctx env t =
res, env
and mmodel_call_valid ~loc kf name ctx env t =
+ match t.term_node with
+ | TBinOp(PlusPI, p, r) when Logic_utils.isLogicPointer p && is_trange r ->
+ let n1, n2 = match r.term_node with
+ | Trange(Some n1, Some n2) ->
+ n1, n2
+ | Trange(None, _) | Trange(_, None) ->
+ Options.fatal "unbounded ranges are not part of E-ACSL"
+ | _ ->
+ assert false
+ in
+ (* s *)
+ let ty = match Cil.unrollType (get_c_term_type p.term_type) with
+ | TPtr(ty, _) -> ty
+ | _ -> assert false
+ in
+ let s = Logic_const.term ~loc (TSizeOf ty) Linteger in
+ (* ptr *)
+ let typ_charptr = TPtr(TInt(IChar, []), []) in
+ let ptr = Logic_const.term
+ ~loc
+ (TBinOp(
+ PlusPI,
+ Logic_const.term ~loc (TCastE(typ_charptr, p)) (Ctype typ_charptr),
+ Logic_const.term ~loc (TBinOp(Mult, s, n1)) Linteger))
+ (Ctype typ_charptr)
+ in
+ Typing.type_term ~use_gmp_opt:false ~ctx:Typing.other ptr;
+ let ptr, env = term_to_exp kf (Env.rte env true) ptr in
+ (* size *)
+ let size = Logic_const.term
+ ~loc
+ (TBinOp(
+ Mult,
+ s,
+ Logic_const.term ~loc (TBinOp(MinusA, n2, n1)) Linteger))
+ Linteger
+ in
+ let ctx_ity = Typing.integer_ty_of_typ ctx in
+ Typing.type_term ~use_gmp_opt:true ~ctx:ctx_ity size;
+ let size, env = term_to_exp kf env size in
+ (* base and base_addr *)
+ let base, _ = Misc.ptr_index ~loc ptr in
+ let base_addr = match base.enode with
+ | AddrOf _ | Const _ -> Cil.zero ~loc
+ | Lval(lv) | StartOf(lv) -> Cil.mkAddrOrStartOf ~loc lv
+ | _ -> assert false
+ in
+ (* generating env *)
+ let _, res, env =
+ Env.new_var
+ ~loc
+ ~name
+ env
+ None
+ ctx
+ (fun v _ ->
+ let fname = Functions.RTL.mk_api_name name in
+ let args = [ ptr; size; base; base_addr ] in
+ [ Misc.mk_call ~loc ~result:(Cil.var v) fname args ])
+ in
+ res, env
+ | _ ->
let e, env = term_to_exp kf (Env.rte env true) t in
let base, _ = Misc.ptr_index ~loc e in
let base_addr = match base.enode with
@@ -620,6 +682,10 @@ and mmodel_call_valid ~loc kf name ctx env t =
in
res, env
+and is_trange t = match t.term_node with
+ | Trange _ -> true
+ | _ -> false
+
and at_to_exp env t_opt label e =
let stmt = E_acsl_label.get_stmt (Env.get_visitor env) label in
(* generate a new variable denoting [\at(t',label)].
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index c28740c7124aea6ff8b5b207a9b135f270c45f8b..38a5dcfe4b5598c4623513f9ccd971596596a996 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -165,6 +165,8 @@ let ty_of_logic_ty = function
| Ltype _ -> Error.not_yet "user-defined logic type"
| Lvar _ -> Error.not_yet "type variable"
+let integer_ty_of_typ ty = ty_of_logic_ty (Ctype ty)
+
(* Compute the smallest type (bigger than [int]) which can contain the whole
interval. It is the \theta operator of the JFLA's paper. *)
let ty_of_interv ?ctx i =
@@ -472,7 +474,7 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
| Tunion _ -> Error.not_yet "tset union"
| Tinter _ -> Error.not_yet "tset intersection"
| Tcomprehension (_,_,_) -> Error.not_yet "tset comprehension"
- | Trange (_,_) -> Error.not_yet "trange"
+ | Trange (_,_) -> dup Gmp
| Tlet(li, t) ->
infer_if_integer li;
let li_t = Misc.term_of_li li in
diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli
index d1d62ef8232b4107b21ab2efe4140354a8e2595e..2319e9c37671cae5d175c52d98a31045472de96a 100644
--- a/src/plugins/e-acsl/typing.mli
+++ b/src/plugins/e-acsl/typing.mli
@@ -73,6 +73,9 @@ val typ_of_integer_ty: integer_ty -> typ
for [Gmp] and [TInt(ik, [[]])] for [Ctype ik].
@raise Not_an_integer in case of {!Other}. *)
+val integer_ty_of_typ: typ -> integer_ty
+(** Reverse of [typ_of_integer_ty] *)
+
val join: integer_ty -> integer_ty -> integer_ty
(** {!integer_ty} is a join-semi-lattice if you do not consider [Other]. If
there is no [Other] in argument, this function computes the join of this