Commit 84c7824a authored by Julien Signoles's avatar Julien Signoles
Browse files

[typing] fix bug with floats/reals; more generally force typing of every non-integer term

parent 4ded561b
......@@ -6,4 +6,5 @@ tests/bts/bts1307.i:11:[e-acsl] warning: approximating a real number by a float
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] user error: type long double not implemented. Using double instead
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status invalid.
tests/bts/bts1307.i:23:[value] warning: function bar, behavior UnderEstimate_Motoring: postcondition got status unknown.
tests/bts/bts1307.i:23:[value] warning: function __gen_e_acsl_bar, behavior UnderEstimate_Motoring: postcondition got status unknown.
......@@ -254,9 +254,9 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
sizeof(float));
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"foo",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at)",11);
__e_acsl_assert(*__gen_e_acsl_at == *__gen_e_acsl_at_2 + (long double)(
(long double)5 - ((long double)(
5 / 80) * *__gen_e_acsl_at_3) * 0.4),
__e_acsl_assert(*__gen_e_acsl_at == *__gen_e_acsl_at_2 + ((long double)5 -
((long double)(
5 / 80) * *__gen_e_acsl_at_3) * 0.4),
(char *)"Postcondition",(char *)"foo",
(char *)"*\\old(Mtmax_out) == *\\old(Mtmax_in)+(5-((5/80)**\\old(Mwmax))*0.4)",
11);
......
......@@ -5,13 +5,15 @@ tests/e-acsl-runtime/valid.c:14:[e-acsl] warning: E-ACSL construct `complete beh
Ignoring annotation.
tests/e-acsl-runtime/valid.c:14:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
FRAMAC_SHARE/libc/stdlib.h:179:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
......
......@@ -192,11 +192,11 @@ let rec type_term env ~ctx t =
let ty =
try
let i = Interval.infer env t in
type_term_lval env tlv;
ty_of_interv ~ctx i
with Interval.Not_an_integer ->
Other
in
type_term_lval env tlv;
dup ty
| Toffset(_, t')
......@@ -210,7 +210,7 @@ let rec type_term env ~ctx t =
ignore (type_term env ~ctx:Other t');
ty_of_interv ~ctx i
with Interval.Not_an_integer ->
Other
assert false
in
dup ty
......@@ -223,50 +223,51 @@ let rec type_term env ~ctx t =
ignore (type_term env ~ctx:Other t2);
ty_of_interv ~ctx i
with Interval.Not_an_integer ->
Other
assert false
in
dup ty
| TUnOp (unop, t') ->
let ty =
let i = Interval.infer env t in
let i' = Interval.infer env t' in
let ctx = mk_ctx (ty_of_interv ~ctx (Interval.join i i')) in
ignore (type_term env ~ctx t');
ctx
let ctx =
try
let i = Interval.infer env t in
let i' = Interval.infer env t' in
mk_ctx (ty_of_interv ~ctx (Interval.join i i'))
with Interval.Not_an_integer ->
Other (* real *)
in
ignore (type_term env ~ctx t');
(match unop with
| LNot -> c_int, ty (* converted into [t == 0] in casse of GMP *)
| Neg | BNot -> dup ty)
| LNot -> c_int, ctx (* converted into [t == 0] in casse of GMP *)
| Neg | BNot -> dup ctx)
| TBinOp((PlusA | MinusA | Mult | Div | Mod | Shiftlt | Shiftrt), t1, t2) ->
let ty =
let i = Interval.infer env t in
let i1 = Interval.infer env t1 in
let i2 = Interval.infer env t2 in
let ctx =
let ctx =
try
let i = Interval.infer env t in
let i1 = Interval.infer env t1 in
let i2 = Interval.infer env t2 in
mk_ctx (ty_of_interv ~ctx (Interval.join i (Interval.join i1 i2)))
in
ignore (type_term env ~ctx t1);
ignore (type_term env ~ctx t2);
ctx
with Interval.Not_an_integer ->
Other (* real *)
in
dup ty
ignore (type_term env ~ctx t1);
ignore (type_term env ~ctx t2);
dup ctx
| TBinOp ((Lt | Gt | Le | Ge | Eq | Ne), t1, t2) ->
assert (compare ctx c_int >= 0);
let ty =
let ctx =
try
let i1 = Interval.infer env t1 in
let i2 = Interval.infer env t2 in
mk_ctx (ty_of_interv ~ctx (Interval.join i1 i2))
with Interval.Not_an_integer ->
Other
in
ignore (type_term env ~ctx t1);
ignore (type_term env ~ctx t2);
match ctx with
let ctx =
try
let i1 = Interval.infer env t1 in
let i2 = Interval.infer env t2 in
mk_ctx (ty_of_interv ~ctx (Interval.join i1 i2))
with Interval.Not_an_integer ->
Other
in
ignore (type_term env ~ctx t1);
ignore (type_term env ~ctx t2);
let ty = match ctx with
| Other -> c_int
| Gmp | C_type _ -> ctx
in
......@@ -274,14 +275,16 @@ let rec type_term env ~ctx t =
| TBinOp ((LAnd | LOr), t1, t2) ->
let ty =
assert (compare ctx c_int >= 1);
let i1 = Interval.infer env t1 in
let i2 = Interval.infer env t2 in
(* both operands fit in an int. *)
ignore (type_term env ~ctx:c_int t1);
ignore (type_term env ~ctx:c_int t2);
ty_of_interv ~ctx (Interval.join i1 i2)
try
let i1 = Interval.infer env t1 in
let i2 = Interval.infer env t2 in
ty_of_interv ~ctx (Interval.join i1 i2)
with Interval.Not_an_integer ->
Other
in
(* both operands fit in an int. *)
ignore (type_term env ~ctx:c_int t1);
ignore (type_term env ~ctx:c_int t2);
dup ty
| TBinOp (BAnd, _, _) -> Error.not_yet "bitwise and"
......@@ -290,55 +293,51 @@ let rec type_term env ~ctx t =
| TCastE(_, t')
| TCoerce(t', _) ->
let ty =
(* in any case, must type the subterms *)
let ctx =
try
let i = Interval.infer env t' in
(* nothing to do more: [i] is already more precise than what we could
infer from the arguments of the cast. Also, do not type the
(* nothing to do more: [i] is already more precise than what we
could infer from the arguments of the cast. Also, do not type the
internal term: possibly it is not even an integer *)
let ty = ty_of_interv ~ctx i in
ignore (type_term env ~ctx:ty t');
ty
ty_of_interv ~ctx i
with Interval.Not_an_integer ->
ignore (type_term env ~ctx:Other t');
Other
in
dup ty
ignore (type_term env ~ctx t');
dup ctx
| Tif (t1, t2, t3) ->
let ty =
let ctx = mk_ctx c_int in
ignore (type_term env ~ctx t1);
let i = Interval.infer env t in
let ctx =
try
let i2 = Interval.infer env t2 in
let i3 = Interval.infer env t3 in
mk_ctx (ty_of_interv ~ctx (Interval.join i (Interval.join i2 i3)))
with Interval.Not_an_integer ->
Other
in
ignore (type_term env ~ctx t2);
ignore (type_term env ~ctx t3);
ctx
let ctx = mk_ctx c_int in
ignore (type_term env ~ctx t1);
let i = Interval.infer env t in
let ctx =
try
let i2 = Interval.infer env t2 in
let i3 = Interval.infer env t3 in
mk_ctx (ty_of_interv ~ctx (Interval.join i (Interval.join i2 i3)))
with Interval.Not_an_integer ->
Other
in
dup ty
ignore (type_term env ~ctx t2);
ignore (type_term env ~ctx t3);
dup ctx
| Tat (t, _)
| TLogic_coerce (_, t) -> dup (type_term env ~ctx t).ty
| TCoerceE (t1, t2) ->
let ty =
let i = Interval.infer env t in
let i1 = Interval.infer env t1 in
let i2 = Interval.infer env t2 in
let ty = ty_of_interv ~ctx (Interval.join i (Interval.join i1 i2)) in
ignore (type_term env ~ctx:ty t1);
ignore (type_term env ~ctx:ty t2);
ty
let ctx =
try
let i = Interval.infer env t in
let i1 = Interval.infer env t1 in
let i2 = Interval.infer env t2 in
ty_of_interv ~ctx (Interval.join i (Interval.join i1 i2))
with Interval.Not_an_integer ->
Other
in
dup ty
ignore (type_term env ~ctx t1);
ignore (type_term env ~ctx t2);
dup ctx
| TAddrOf tlv
| TStartOf tlv ->
......@@ -516,13 +515,21 @@ let get_integer_op t = (Memo.get t).op
let get_integer_op_of_predicate p =
(type_predicate_named Interval.Env.empty (* the env is useless *) p).op
let extract_typ t ty =
try typ_of_integer_ty ty
with Not_an_integer ->
let ty = t.term_type in
if Cil.isLogicRealType ty then TFloat(FLongDouble, [])
else if Cil.isLogicFloatType ty then Logic_utils.logicCType ty
else assert false
let get_typ t =
let info = Memo.get t in
try typ_of_integer_ty info.ty with Not_an_integer -> assert false
extract_typ t info.ty
let get_op t =
let info = Memo.get t in
try typ_of_integer_ty info.op with Not_an_integer -> assert false
extract_typ t info.op
let get_cast t =
Cil.CurrentLoc.set t.term_loc;
......
......@@ -58,7 +58,7 @@ val get_integer_op: term -> integer_ty
val get_integer_op_of_predicate: predicate named -> integer_ty
val get_typ: term -> typ
(** Get the type of the given term which must be an integer.
(** Get the type of the given term.
{!type_named_predicate} must already have been called on the englobing
predicate. *)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment