source: extracted/compute_fixpoints.ml @ 2736

Last change on this file since 2736 was 2736, checked in by sacerdot, 6 years ago

Untrusted fixpoint computation branched in.

File size: 989 bytes
Line 
1module 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.lookup0 PreIdentifiers.LabelTag !t k with
17      Types.Some res -> res
18    | Types.None -> raise Not_found
19
20  let iter f t =
21   Identifiers.foldi0 PreIdentifiers.LabelTag (fun k v () -> f k v) !t ()
22
23end
24
25(** val compute_fixpoint : Fixpoints.fixpoint_computer **)
26let 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
Note: See TracBrowser for help on using the repository browser.