From a0e03fe9a08aa610bfb3b8a805ae619a9f8150a7 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 21 Mar 2016 11:12:10 +0100
Subject: [PATCH] [typing] fix one incorrect assertion
---
src/plugins/e-acsl/new_typing.ml | 10 +++++-----
src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c | 12 ++++++------
src/plugins/e-acsl/translate.ml | 3 ++-
3 files changed, 13 insertions(+), 12 deletions(-)
diff --git a/src/plugins/e-acsl/new_typing.ml b/src/plugins/e-acsl/new_typing.ml
index e00af8bec52..f8f4952a7fc 100644
--- a/src/plugins/e-acsl/new_typing.ml
+++ b/src/plugins/e-acsl/new_typing.ml
@@ -219,7 +219,7 @@ let rec type_term env ~ctx t =
ignore (type_term env ~ctx t2);
ctx
| TBinOp ((Lt | Gt | Le | Ge | Eq | Ne), t1, t2) ->
- assert (compare ctx c_int >= 1);
+ assert (compare ctx c_int >= 0);
let ctx =
try
let i1 = Interval.infer env t1 in
@@ -302,7 +302,7 @@ let rec type_term env ~ctx t =
Other
| TBinOp ((PlusPI | IndexPI | MinusPI), t1, t2) ->
-(* Options.feedback "BIN PI"; (* HERE *)*)
+(* Options.feedback "BIN PI %a ; %a" Printer.pp_term t1 Printer.pp_term t2; (* HERE *)*)
(* it is a pointer, as well as [t1], while [t2] is a size_t.
Both [t1] and [t2] must be typed. *)
ignore (type_term env ~ctx:Other t1);
@@ -438,12 +438,12 @@ let rec type_predicate_named env p =
coerce ~ctx:c_int ty
let type_term ~ctx t =
- Options.feedback ~dkey ~level:4 "typing term %a."
- Printer.pp_term t;
+ Options.feedback ~dkey ~level:4 "typing term '%a' in ctx '%a'."
+ Printer.pp_term t pretty ctx;
ignore (type_term Interval.Env.empty ~ctx t)
let type_named_predicate ?(must_clear=true) p =
- Options.feedback ~dkey ~level:3 "typing predicate %a."
+ Options.feedback ~dkey ~level:3 "typing predicate '%a'."
Printer.pp_predicate_named p;
if must_clear then Memo.clear ();
ignore (type_predicate_named Interval.Env.empty p)
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
index 3c0c69ee916..1dcf27f839c 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
@@ -80,20 +80,20 @@ int __gen_e_acsl_sorted(int *t, int n)
{
int __gen_e_acsl_valid_read;
int __gen_e_acsl_valid_read_2;
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(t + __gen_e_acsl_i),
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(t + (unsigned long)((unsigned int)__gen_e_acsl_i)),
sizeof(int));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",
(char *)"sorted",
- (char *)"mem_access: \\valid_read(t+__gen_e_acsl_i)",
+ (char *)"mem_access: \\valid_read(t+(unsigned long)__gen_e_acsl_i)",
6);
- __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(t + (
- (long)__gen_e_acsl_i - (long)1)),
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(t + (unsigned long)(
+ __gen_e_acsl_i - 1)),
sizeof(int));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",
(char *)"sorted",
- (char *)"mem_access: \\valid_read(t+(long)((long)__gen_e_acsl_i-1))",
+ (char *)"mem_access: \\valid_read(t+(unsigned long)((long)(__gen_e_acsl_i-1)))",
6);
- if (*(t + ((long)__gen_e_acsl_i - (long)1)) <= *(t + __gen_e_acsl_i))
+ if (*(t + (unsigned long)(__gen_e_acsl_i - 1)) <= *(t + (unsigned long)__gen_e_acsl_i))
;
else {
__gen_e_acsl_forall = 0;
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 7a40bfe6e03..665f09ba460 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -550,7 +550,8 @@ and mmodel_call_with_size ~loc kf name ctx env t =
| TPtr (t', _) -> Cil.new_exp ~loc (SizeOf t')
| _ -> assert false
in
- [ Misc.mk_call ~loc ~result:(Cil.var v) ("__" ^ name) [ e; sizeof ] ])
+ [ Misc.mk_call
+ ~loc ~result:(Cil.var v) (Misc.mk_api_name name) [ e; sizeof ] ])
in
res, env
--
GitLab