Commit 760e4405 authored by Tristan Le Gall's avatar Tristan Le Gall
Browse files

correction about TCastE

parent 7d8106d9
......@@ -135,6 +135,23 @@ let rec infer t =
let i1 = infer t1 in
let i2 = infer t2 in
Ival.bitwise_or i1 i2
| TCastE (ty, t) ->
(try
let it = infer t in
let ity = interv_of_typ ty in
Ival.meet it ity
with Not_an_integer ->
if Cil.isIntegralType ty then begin
(* heterogeneous cast from a non-integral term to an integral type:
consider that one eventually gets an integral type even if it is
not sure. *)
Options.warning
~once:true "possibly unsafe cast from term '%a' to type '%a'."
Printer.pp_term t
Printer.pp_typ ty;
interv_of_typ ty
end else
raise Not_an_integer)
| Tif (_, t2, t3) ->
let i2 = infer t2 in
let i3 = infer t3 in
......@@ -196,8 +213,7 @@ let rec infer t =
| TUpdate (_,_,_)
| Ttypeof _
| Ttype _
| Tempty_set
| TCastE (_,_) -> raise Not_an_integer
| Tempty_set -> raise Not_an_integer
and infer_term_lval (host, offset as tlv) =
match offset with
......
......@@ -391,6 +391,20 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
| TBinOp (BXor, _, _) -> Error.not_yet "bitwise xor"
| TBinOp (BOr, _, _) -> Error.not_yet "bitwise or"
| TCastE(_, t') ->
let ctx =
try
(* compute the smallest interval from the whole term [t] *)
let i = Interval.infer t in
(* nothing more to do: [i] is already more precise than what we
could infer from the arguments of the cast. *)
ty_of_interv ?ctx i
with Interval.Not_an_integer ->
Other
in
ignore (type_term ~use_gmp_opt:true ~ctx t');
dup ctx
| Tif (t1, t2, t3) ->
let ctx1 =
mk_ctx ~use_gmp_opt:false c_int (* an int must be generated *)
......@@ -466,8 +480,7 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
| TConst (LStr _ | LWStr _ | LReal _)
| Ttypeof _
| Ttype _
| Tempty_set
| TCastE (_,_) -> dup Other
| Tempty_set -> dup Other
in
Memo.memo
(fun t ->
......
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