extracted/untrusted/compute_fixpoints.ml

   1 module Label_ImperativeMap = struct
   2
   3   type key = Graphs.label
   4
   5   type 'data t = 'data Graphs.graph ref
   6
   7   let create () = ref (Identifiers.empty_map PreIdentifiers.LabelTag)
   8
   9   let clear t =
  10     t := Identifiers.empty_map PreIdentifiers.LabelTag
  11
  12   let add k d t =
  13     t := Identifiers.add PreIdentifiers.LabelTag !t k d
  14
  15   let find k t =
  16    match Identifiers.lookup PreIdentifiers.LabelTag !t k with
  17       Types.Some res -> res
  18     | Types.None -> raise Not_found
  19
  20   let iter f t =
  21    Identifiers.foldi PreIdentifiers.LabelTag (fun k v () -> f k v) !t ()
  22
  23 end
  24
  25 (** val compute_fixpoint : Fixpoints.fixpoint_computer **)
  26 let compute_fixpoint latt =
  27  let module L : Fix.PROPERTY with type property = Preamble.__ =
  28   struct
  29    type property = Preamble.__
  30    let bottom = Fixpoints.l_bottom latt
  31    let equal x y = Fixpoints.l_equal latt x y = Bool.True
  32    let is_maximal x = Fixpoints.l_is_maximal latt x = Bool.True
  33   end in
  34  let module F = Fix.Make (Label_ImperativeMap) (L) in
  35   F.lfp