From e3dfc90e6910caa9dd639f668abdb83a5daea21e Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 27 Oct 2014 10:00:38 +0100
Subject: [PATCH] [translation] add a missing cast when an integer is used in a
floating point/real context (was revealed by a Value's change, and now
reveals a bug with == over reals)
---
src/plugins/e-acsl/TODO | 3 +
src/plugins/e-acsl/doc/Changelog | 3 +
.../oracle/bts1307.1.res.oracle | 5 --
.../e-acsl-runtime/oracle/bts1307.res.oracle | 17 +----
.../tests/e-acsl-runtime/oracle/gen_bts1307.c | 4 +-
.../e-acsl-runtime/oracle/gen_bts13072.c | 3 +-
src/plugins/e-acsl/translate.ml | 74 +++++++++++++------
7 files changed, 66 insertions(+), 43 deletions(-)
diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index b7e35cba3ac..8a372299c04 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -81,6 +81,9 @@
- interprétation des tableaux logiques
[Dillon] Windows
- \valid(p) is not true if p is a const pointer (depend on -const-readonly)
+- utiliser == avec des real en arguments : c'est convertit en une égalité sur
+des floating points, qui ne fait notoirement pas ce qu'on veut
+(voir tests/e-acsl-runtime/bts1307.i).
[to be check]: no call to full_init or initialize for the assigned result of a
function call
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 41b61fc71f4..776b0996f4f 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,9 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
+-* E-ACSL [2014/10/27] Add a missing cast when translating an integral
+ type used in a floating point/real context in an annotation.
+
########################
Plugin E-ACSL 0.4.1 Neon
########################
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
index e97a4bc14d2..0a07b7eceec 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
@@ -50,11 +50,6 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:166:[value] Function __gmpz_tdiv_q: preconditio
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid.
[value] using specification for function __valid_read
[value] user error: type long double not implemented. Using double instead
-tests/e-acsl-runtime/bts1307.i:13:[kernel] warning: non-finite long double value ([--..--]):
- assert \is_finite((long double)(__e_acsl_4**__e_acsl_at_3));
-tests/e-acsl-runtime/bts1307.i:13:[kernel] warning: non-finite long double value ([--..--]):
- assert
- \is_finite((long double)(5-(long double)((long double)(__e_acsl_4**__e_acsl_at_3)*0.4)));
[value] using specification for function __gmpz_clear
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
tests/e-acsl-runtime/bts1307.i:13:[value] Function __e_acsl_foo, behavior OverEstimate_Motoring: postcondition got status valid.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle
index 19a39a5b1a3..8ced7d9de92 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle
@@ -36,20 +36,7 @@ tests/e-acsl-runtime/bts1307.i:9:[value] Function foo: precondition got status v
tests/e-acsl-runtime/bts1307.i:13:[value] Function foo, behavior OverEstimate_Motoring: postcondition got status valid.
[value] using specification for function __valid_read
[value] user error: type long double not implemented. Using double instead
-tests/e-acsl-runtime/bts1307.i:13:[kernel] warning: non-finite float value ([-1.79769313486e+308 .. 1.79769313486e+308]):
- assert
- \is_finite((float)(*__e_acsl_at_2+(int)(5-(long double)((float)((int)
- (5/80)**__e_acsl_at_3)*0.4))));
-tests/e-acsl-runtime/bts1307.i:13:[value] Function __e_acsl_foo, behavior OverEstimate_Motoring: postcondition got status valid.
-tests/e-acsl-runtime/bts1307.i:19:[value] Function __e_acsl_bar: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:20:[value] Function __e_acsl_bar: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:21:[value] Function __e_acsl_bar: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:19:[value] Function bar: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:20:[value] Function bar: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:21:[value] Function bar: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:25:[value] Function bar, behavior UnderEstimate_Motoring: postcondition got status unknown.
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:25:[value] Function __e_acsl_bar, behavior UnderEstimate_Motoring: postcondition got status unknown.
-[value] using specification for function __e_acsl_memory_clean
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status invalid.
+tests/e-acsl-runtime/bts1307.i:13:[value] Function __e_acsl_foo, behavior OverEstimate_Motoring: no state left in which to evaluate postcondition, status not computed.
[value] done for function main
[value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c
index d1e3c38cc94..49ba96ec713 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c
@@ -149,7 +149,9 @@ void __e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
__e_acsl_valid_read_3 = __valid_read((void *)__e_acsl_at,sizeof(float));
e_acsl_assert(__e_acsl_valid_read_3,(char *)"RTE",(char *)"foo",
(char *)"mem_access: \\valid_read(__e_acsl_at)",13);
- e_acsl_assert(*__e_acsl_at == *__e_acsl_at_2 + (5 - ((5 / 80) * *__e_acsl_at_3) * 0.4),
+ e_acsl_assert(*__e_acsl_at == *__e_acsl_at_2 + (long double)((long double)5 -
+ ((long double)(
+ 5 / 80) * *__e_acsl_at_3) * 0.4),
(char *)"Postcondition",(char *)"foo",
(char *)"*\\old(Mtmax_out) == *\\old(Mtmax_in)+(5-((5/80)**\\old(Mwmax))*0.4)",
13);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c
index c8a41f86fa9..5a1adaa3409 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c
@@ -223,7 +223,8 @@ void __e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
__e_acsl_valid_read_3 = __valid_read((void *)__e_acsl_at,sizeof(float));
e_acsl_assert(__e_acsl_valid_read_3,(char *)"RTE",(char *)"foo",
(char *)"mem_access: \\valid_read(__e_acsl_at)",13);
- e_acsl_assert(*__e_acsl_at == *__e_acsl_at_2 + (5 - (__e_acsl_4 * *__e_acsl_at_3) * 0.4),
+ e_acsl_assert(*__e_acsl_at == *__e_acsl_at_2 + ((long double)5 -
+ ((long double)__e_acsl_4 * *__e_acsl_at_3) * 0.4),
(char *)"Postcondition",(char *)"foo",
(char *)"*\\old(Mtmax_out) == *\\old(Mtmax_in)+(5-((5/80)**\\old(Mwmax))*0.4)",
13);
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 82429669ad2..d5e954eb5c1 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -131,6 +131,26 @@ let conditional_to_exp ?(name="if") loc ctx e1 (e2, env2) (e3, env3) =
in
e, env
+(* If [e] is inserted in a context of type [float] or equivalent, then an
+ explicit cast must be introduced (an explicit coercion is required in C, but
+ it is implicit in the logic world).
+ [lty] is the type of the logic context, while [lty_t] is the logic type of
+ the term which [e] comes from. *)
+let cast_integer_to_float lty lty_t e =
+ if Cil.isIntegralType (Cil.typeOf e) then
+ let ty, correct = match lty, lty_t with
+ | Ctype ty, _ -> ty, true
+ | Lreal, Linteger -> Cil.longDoubleType, false
+ | Lreal, _ -> Cil.longDoubleType, true
+ | (Ltype _ | Lvar _ | Linteger | Larrow _), _ -> assert false
+ in
+ if not correct then
+ Options.warning
+ "casting an integer to a long double without verification";
+ Cil.mkCast ~force:false ~e ~newt:ty
+ else
+ e
+
let rec thost_to_host kf env = function
| TVar { lv_origin = Some v } ->
Var (Cil.get_varinfo (Env.get_behavior env) v), env, v.vname
@@ -235,7 +255,13 @@ and context_insensitive_term_to_exp kf env t =
in
e, env, false, ""
else
- Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)), env, false, ""
+ if Logic_typing.is_integral_type t.term_type then
+ Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)), env, false, ""
+ else
+ (* floating point context: casting the arguments potentially required *)
+ let e1 = cast_integer_to_float t.term_type t1.term_type e1 in
+ let e2 = cast_integer_to_float t.term_type t2.term_type e2 in
+ Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)), env, false, ""
| TBinOp(Div | Mod as bop, t1, t2) ->
let ty = Typing.typ_of_term_operation t in
let ctx = Some ty in
@@ -276,7 +302,13 @@ and context_insensitive_term_to_exp kf env t =
e, env, false, ""
else
(* no guard required since RTEs are generated separately *)
- Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)), env, false, ""
+ if Logic_typing.is_integral_type t.term_type then
+ Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)), env, false, ""
+ else
+ (* floating point context: casting the arguments potentially required *)
+ let e1 = cast_integer_to_float t.term_type t1.term_type e1 in
+ let e2 = cast_integer_to_float t.term_type t2.term_type e2 in
+ Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)), env, false, ""
| TBinOp(Lt | Gt | Le | Ge | Eq | Ne as bop, t1, t2) ->
(* comparison operators *)
let e, env = comparison_to_exp ~loc kf env bop t1 t2 (Some t) in
@@ -638,26 +670,26 @@ and named_predicate_to_exp ?name kf ?rte env p =
and translate_rte_annots:
'a. (Format.formatter -> 'a -> unit) -> 'a ->
- kernel_function -> Env.t -> code_annotation list -> Env.t =
+ kernel_function -> Env.t -> code_annotation list -> Env.t =
fun pp elt kf env l ->
- let old_valid = !is_visiting_valid in
- let old_kind = Env.annotation_kind env in
- let env = Env.set_annotation_kind env Misc.RTE in
- let env =
- List.fold_left
- (fun env a -> match a.annot_content with
- | AAssert(_, p) ->
- handle_error
- (fun env ->
- Options.feedback ~dkey ~level:4 "prevent RTE from %a" pp elt;
- translate_named_predicate kf (Env.rte env false) p)
- env
- | _ -> assert false)
- env
- l
- in
- is_visiting_valid := old_valid;
- Env.set_annotation_kind env old_kind
+ let old_valid = !is_visiting_valid in
+ let old_kind = Env.annotation_kind env in
+ let env = Env.set_annotation_kind env Misc.RTE in
+ let env =
+ List.fold_left
+ (fun env a -> match a.annot_content with
+ | AAssert(_, p) ->
+ handle_error
+ (fun env ->
+ Options.feedback ~dkey ~level:4 "prevent RTE from %a" pp elt;
+ translate_named_predicate kf (Env.rte env false) p)
+ env
+ | _ -> assert false)
+ env
+ l
+ in
+ is_visiting_valid := old_valid;
+ Env.set_annotation_kind env old_kind
and translate_rte kf env e =
let stmt = Cil.mkStmtOneInstr ~valid_sid:true (Skip e.eloc) in
--
GitLab