Commit 5ad58584 authored by Julien Signoles's avatar Julien Signoles
Browse files

move Misc.is_recursive in Interval_system and improve it

parent d5442c37
......@@ -191,7 +191,7 @@ let rec infer t =
| LBterm t' ->
(* TODO: should not be necessary to distinguish the recursive case.
Stack overflow if not distingued *)
if Misc.is_recursive li then
if Interval_system.is_recursive li then
Interval_system.build_and_solve ~infer t
else begin (* non-recursive case *)
(* add the arguments to the context *)
......
......@@ -65,6 +65,41 @@ module Ivar =
exception Not_an_integer
let is_recursive li = match li.l_body with
| LBpred _ | LBnone | LBreads _ | LBinductive _ -> false
| LBterm t ->
let rec has_recursive_call t = match t.term_node with
| TConst _ | TLval _ | TSizeOf _ | TSizeOfStr _ | TAlignOf _
| Tnull | TAddrOf _ | TStartOf _ | Tempty_set | Ttypeof _
| Ttype _->
false
| Tapp(li', _, ts) ->
String.equal li.l_var_info.lv_name li'.l_var_info.lv_name
|| List.exists has_recursive_call ts
| TUnOp(_, t) | TSizeOfE t | TCastE(_, t) | Tat(t, _) | Tlambda(_, t)
| Toffset(_, t) | Tbase_addr(_, t) | TAlignOfE t | Tblock_length(_, t)
| TLogic_coerce(_, t) | TCoerce(t, _) | Tcomprehension(t, _, _)
| Tlet(_, t) ->
has_recursive_call t
| TBinOp(_, t1, t2) | TCoerceE(t1, t2) | TUpdate(t1, _, t2) ->
has_recursive_call t1 || has_recursive_call t2
| Trange(t1_opt, t2_opt) ->
(match t1_opt with
| None -> begin match t2_opt with
| None -> false
| Some t2 -> has_recursive_call t2
end
| Some t1 -> begin match t2_opt with
| None -> has_recursive_call t1
| Some t2 -> has_recursive_call t1 || has_recursive_call t2
end)
| Tif(t0, t1, t2) ->
has_recursive_call t0 || has_recursive_call t1 || has_recursive_call t2
| TDataCons(_, ts) | Tunion ts | Tinter ts ->
List.exists has_recursive_call ts
in
has_recursive_call t
let rec interv_of_typ ty = match Cil.unrollType ty with
| TInt (k,_) as ty ->
let n = Cil.bitsSizeOf ty in
......@@ -115,7 +150,7 @@ let interv_of_typ_containing_interv i =
let build ~infer t =
let rec aux ieqs ivars t = match t.term_node with
| Tapp(li, _, args) ->
if li.l_type = Some Linteger && Misc.is_recursive li then begin
if li.l_type = Some Linteger && is_recursive li then begin
let args_lty = List.map2
(fun lv arg ->
try
......
......@@ -33,6 +33,7 @@ val build_and_solve: infer:(term -> Ival.t) -> term -> Ival.t
break mutual module dependencies *)
exception Not_an_integer
val is_recursive: logic_info -> bool
val interv_of_typ: typ -> Ival.t
val ikind_of_interv: Ival.t -> Cil_types.ikind
(*/*)
......@@ -315,43 +315,6 @@ let finite_min_and_max i = match Ival.min_and_max i with
| Some min, Some max -> min, max
| None, _ | _, None -> assert false
let is_recursive li =
match li.l_body with
| LBpred _ | LBnone | LBreads _ | LBinductive _ -> false
| LBterm t ->
let rec has_recursive_call t = match t.term_node with
| TConst _ | TLval _ | TSizeOf _ | TSizeOfStr _ | TAlignOf _
| Tnull | TAddrOf _ | TStartOf _ | Tempty_set | Ttypeof _
| Ttype _->
false
| Tapp(li', _, ts) ->
if li.l_var_info.lv_name = li'.l_var_info.lv_name then true
else List.fold_left (fun b t -> b || has_recursive_call t) false ts
| TUnOp(_, t) | TSizeOfE t | TCastE(_, t) | Tat(t, _) | Tlambda(_, t)
| Toffset(_, t) | Tbase_addr(_, t) | TAlignOfE t | Tblock_length(_, t)
| TLogic_coerce(_, t) | TCoerce(t, _) | Tcomprehension(t, _, _)
| Tlet(_, t) ->
has_recursive_call t
| TBinOp(_, t1, t2) | TCoerceE(t1, t2) | TUpdate(t1, _, t2) ->
has_recursive_call t1 || has_recursive_call t2
| Trange(t1_opt, t2_opt) ->
begin match t1_opt with
| None -> begin match t2_opt with
| None -> false
| Some t2 -> has_recursive_call t2
end
| Some t1 -> begin match t2_opt with
| None -> has_recursive_call t1
| Some t2 -> has_recursive_call t1 || has_recursive_call t2
end
end
| Tif(t0, t1, t2) ->
has_recursive_call t0 || has_recursive_call t1 || has_recursive_call t2
| TDataCons(_, ts) | Tunion ts | Tinter ts ->
List.fold_left (fun b t -> b || has_recursive_call t) false ts
in
has_recursive_call t
(*
Local Variables:
compile-command: "make"
......
......@@ -127,9 +127,6 @@ val mk_ptr_sizeof: typ -> location -> exp
val finite_min_and_max: Ival.t -> Integer.t * Integer.t
(** [finite_min_and_max i] takes the finite ival [i] and returns its bounds *)
val is_recursive: logic_info -> bool
(** [is_recursive li] returns true iff [li] is defined recursively. *)
(*
Local Variables:
compile-command: "make"
......
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