diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml
index 171a654d313576cffae1a2e3d1434972c0608246..80625645dac9c8ed6ec2f58bc5bf1295d21b08f3 100644
--- a/src/plugins/e-acsl/interval.ml
+++ b/src/plugins/e-acsl/interval.ml
@@ -30,6 +30,8 @@ open Cil_types
(* Basic datatypes and operations *)
(* ********************************************************************* *)
+(* TODO RATIONAL: both exceptions should be handle in the same way in this
+ module *)
exception Is_a_real
exception Not_a_number
@@ -57,21 +59,18 @@ let rec interv_of_typ_with_real ty is_real = match Cil.unrollType ty with
| TEnum(enuminfo, _) ->
interv_of_typ_with_real (TInt (enuminfo.ekind, [])) is_real
| TFloat _ ->
- (* TODO RATIONAL: examine TODO below. In particular this case is equivalent
- * to the next case when [Real.is_t ty]. *)
- (* TODO: Do not systematically consider floats as reals for efficiency *)
- Ival.bottom, true
+ raise Is_a_real
| _ when Real.is_t ty ->
- (* TODO RATIONAL: why bottom and not top? Why not raising Is_a_real? *)
- Ival.bottom, true
- | _ ->
+ raise Is_a_real
+ | TVoid _ | TPtr _ | TArray _ | TFun _ | TComp _ | TBuiltin_va_list _ ->
raise Not_a_number
+ | TNamed _ ->
+ assert false
let interv_of_logic_typ = function
| Ctype ty -> interv_of_typ_with_real ty false
| Linteger -> Ival.inject_range None None, false
- | Lreal -> Ival.bottom, true
- (* TODO RATIONAL: why bottom and not top? Why not raising Is_a_real? *)
+ | Lreal -> raise Is_a_real
| Ltype _ -> Error.not_yet "user-defined logic type"
| Lvar _ -> Error.not_yet "type variable"
| Larrow _ -> Error.not_yet "functional type"
@@ -99,6 +98,7 @@ module rec Env: sig
val remove: Cil_types.logic_var -> unit
val replace: Cil_types.logic_var -> Ival.t -> unit
end = struct
+
open Cil_datatype
let tbl: Ival.t Logic_var.Hashtbl.t = Logic_var.Hashtbl.create 7
@@ -113,7 +113,7 @@ end = struct
end
-(* Environment for handling recursive logic functions *)
+(* Environment for handling logic functions *)
and Logic_function_env: sig
val widen:
infer_with_real:(term -> bool -> Ival.t * bool) -> term -> Ival.t
@@ -327,7 +327,11 @@ let rec infer_with_real t is_real =
List.iter (fun lv -> Env.remove lv) li.l_profile;
fixpoint i
in
- fixpoint Ival.bottom
+ let i = fixpoint Ival.bottom in
+ (* call [interv_of_logic_typ] in order to raise Is_a_real or Not_a_number
+ when the function does not return an integer *)
+ Extlib.may (fun lty -> ignore (interv_of_logic_typ lty)) li.l_type;
+ i
| LBnone
| LBreads _ ->
(match li.l_type with
diff --git a/src/plugins/e-acsl/logic_functions.ml b/src/plugins/e-acsl/logic_functions.ml
index f9b4a47a05ecd427340f3f866e90c02df3179261..f865b09c954bcaf76ff2e7ceb6139a3b4557c110 100644
--- a/src/plugins/e-acsl/logic_functions.ml
+++ b/src/plugins/e-acsl/logic_functions.ml
@@ -127,10 +127,7 @@ let generate_kf ~loc fname env ret_ty params_ty li =
parameters *)
Gmp.Z.t_ptr ()
| Typing.C_type ik -> TInt(ik, [])
- | Typing.Real ->
- (* TODO RATIONAL: implement this case *)
- assert false
- | Typing.Nan -> Typing.typ_of_lty lvi.lv_type
+ | Typing.Real | Typing.Nan -> Typing.typ_of_lty lvi.lv_type
in
(* build the formals: cannot use [Cil.makeFormal] since the function
does not yet exist *)
@@ -192,12 +189,15 @@ let generate_kf ~loc fname env ret_ty params_ty li =
before generating the code (code generation invokes typing) *)
let env =
let add env lvi vi =
- (match vi.vtype with
- | TInt _ as ty -> Interval.Env.add lvi (Interval.interv_of_typ ty)
- | ty ->
- (* TODO RATIONAL: what to do with rationals? *)
- if Gmp.Z.is_t ty then
- Interval.Env.add lvi (Ival.inject_range None None));
+ let i =
+ try
+ Interval.interv_of_typ vi.vtype
+ with
+ | Interval.Not_a_number
+ | Interval.Is_a_real ->
+ Ival.inject_range None None
+ in
+ Interval.Env.add lvi i;
Env.Logic_binding.add_binding env lvi vi
in
List.fold_left2 add env li.l_profile params
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index bb76cea30ea8b5c70da5cc060ae3a35cda0c5230..63664e3a13befc7242d162a5fbe44beba9a92852 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -66,7 +66,7 @@ let name_of_mpz_arith_bop = function
type strnum =
| Str_Z (* integers *)
| Str_R (* reals *)
- | C_number (* integers AND floats) included *)
+ | C_number (* integers and floats included *)
(* convert [e] in a way that it is compatible with the given typing context. *)
let add_cast ~loc ?name env ctx strnum t_opt e =
@@ -235,15 +235,19 @@ let conditional_to_exp ?(name="if") loc t_opt e1 (e2, env2) (e3, env3) =
let rec thost_to_host kf env th = match th with
| TVar { lv_origin = Some v } ->
- Var (Visitor_behavior.Get.varinfo (Env.get_behavior env) v), env, v.vname
+ let v' = Visitor_behavior.Get.varinfo (Env.get_behavior env) v in
+ Var v', env, v.vname
| TVar ({ lv_origin = None } as logic_v) ->
- Var (Env.Logic_binding.get env logic_v), env, logic_v.lv_name
+ let v' = Env.Logic_binding.get env logic_v in
+ Var v', env, logic_v.lv_name
| TResult _typ ->
let vis = Env.get_visitor env in
let kf = Extlib.the vis#current_kf in
let lhost = Misc.result_lhost kf in
(match lhost with
- | Var v -> Var (Visitor_behavior.Get.varinfo (Env.get_behavior env) v), env, "result"
+ | Var v ->
+ let v' = Visitor_behavior.Get.varinfo (Env.get_behavior env) v in
+ Var v', env, "result"
| _ -> assert false)
| TMem t ->
let e, env = term_to_exp kf env t in
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 64f6ddf51eee5b0a0b7bcf0c2ab463d3fdd33cf1..f019204e04e53d2c095e7397385bb880c98baae8 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -52,7 +52,7 @@ module D =
Datatype.Make_with_collections
(struct
type t = number_ty
- let name = "E_ACSL.New_typing.t"
+ let name = "E_ACSL.Typing.t"
let reprs = [ Gmpz; Real; Nan; c_int ]
include Datatype.Undefined