Commit 7b8de953 authored by Julien Signoles's avatar Julien Signoles
Browse files

[Typing] minor improvements

parent 49f1f40a
......@@ -88,7 +88,7 @@ let ikind_of_interv i =
if Cil.intTypeIncluded kind IInt then IInt else kind
| None, None -> raise Cil.Not_representable (* GMP *)
| None, Some _ | Some _, None ->
Kernel.fatal ~current:true "ival: %a" Ival.pretty i
Kernel.fatal ~current:true "unexpected ival: %a" Ival.pretty i
(* function call profiles (intervals for their formal parameters) *)
module Profile = struct
......@@ -252,7 +252,7 @@ let infer_alignof ty = singleton_of_int (Cil.bytesAlignOf ty)
let rec infer_with_real t is_real =
let get_cty t = match t.term_type with Ctype ty -> ty | _ -> assert false in
match t.term_node with
| TConst (Integer (n,_)) -> Ival.inject_singleton n, is_real
| TConst (Integer (n, _)) -> Ival.inject_singleton n, is_real
| TConst (LChr c) ->
let n = Cil.charConstToInt c in
Ival.inject_singleton n, is_real
......
......@@ -124,7 +124,7 @@ let add_cast ~loc ?name env ctx strnum t_opt e =
else if Real.is_t ctx then
if Real.is_t (Cil.typeOf e) then e, env
else Real.mk_real ~loc ?name e env t_opt
else
else (* the context is neither MPZ nor MPQ *)
(* handle a C-integer context *)
if Gmp.Z.is_t ty || strnum = Str_Z then
(* we get an mpz, but it fits into a C integer: convert it *)
......@@ -605,7 +605,7 @@ and term_to_exp kf env t =
(* generate the C code equivalent to [t1 bop t2]. *)
and comparison_to_exp
~loc ?e1 kf env ity bop ?(name=Misc.name_of_binop bop) t1 t2 t_opt =
~loc ?e1 kf env ity bop ?(name = Misc.name_of_binop bop) t1 t2 t_opt =
let e1, env = match e1 with
| None ->
let e1, env = term_to_exp kf env t1 in
......
......@@ -56,19 +56,22 @@ module D =
let reprs = [ Gmpz; Real; Nan; c_int ]
include Datatype.Undefined
let compare ty1 ty2 = match ty1, ty2 with
| C_type i1, C_type i2 ->
if i1 = i2 then 0
else if Cil.intTypeIncluded i1 i2 then -1 else 1
| (C_type _ | Gmpz | Real), Nan
| (C_type _ | Gmpz), Real
| C_type _, Gmpz ->
-1
| (Gmpz | Real | Nan), C_type _
| (Real | Nan), Gmpz
| Nan, Real ->
1
| Gmpz, Gmpz | Real, Real | Nan, Nan -> 0
let compare ty1 ty2 =
if ty1 == ty2 then 0
else
match ty1, ty2 with
| C_type i1, C_type i2 ->
if i1 = i2 then 0
else if Cil.intTypeIncluded i1 i2 then -1 else 1
| (C_type _ | Gmpz | Real), Nan
| (C_type _ | Gmpz), Real
| C_type _, Gmpz ->
-1
| (Gmpz | Real | Nan), C_type _
| (Real | Nan), Gmpz
| Nan, Real ->
1
| Gmpz, Gmpz | Real, Real | Nan, Nan -> assert false
let equal = Datatype.from_compare
......@@ -192,11 +195,11 @@ end
let ty_of_interv ?ctx i =
try
let kind = Interval.ikind_of_interv i in
(* ctx type whenever possible to prevent superfluous casts in the generated
code *)
(match ctx with
| None | Some (Gmpz | Nan) -> C_type kind
| Some (C_type ik as ctx) ->
(* return [ctx] type for types smaller than int to prevent superfluous
casts in the generated code *)
if Cil.intTypeIncluded kind ik then ctx else C_type kind
| Some Real -> Real)
with Cil.Not_representable ->
......@@ -306,7 +309,7 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
that every subterm is typed, even if it is not an integer. *)
match t.term_node with
| TConst (LReal _) ->
(* TODO: real: irrationals raise not_yet *)
(* TODO RATIONAL: real: irrationals raise not_yet *)
dup real
| TConst (Integer _ | LChr _ | LEnum _)
| TSizeOf _
......
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