000001| (** Overall analysis lattice *)
000002|
000003| module LabelMap = Map.Make(struct type t = int
000004| let compare i i' = (*[123593]*)i - i' end)
000005|
000006| type elem = Statelattice.elem LabelMap.t
000007|
000008| (* leq : elem -> elem -> bool *)
000009| let leq st0 st1 =
000010| (*[651]*)LabelMap.fold (fun lab obj acc ->
000011| (*[7356]*)let obj' = try (*[7356]*)LabelMap.find lab st1
000012| with Not_found -> (*[1289]*)Statelattice.bot
000013| in (*[7356]*)acc && (*[4768]*)Statelattice.leq obj obj') st0 true
000014|
000015| (* eq : elem -> elem -> bool *)
000016| let eq = (*[1]*)LabelMap.equal (Statelattice.eq)
000017|
000018| (* join : elem -> elem -> elem *)
000019| let join st0 st1 = (*[2394]*)LabelMap.merge (fun lab obj0 obj1 -> match obj0,obj1 with
000020| | None,_ -> (*[18]*)obj1
000021| | _,None -> (*[55]*)obj0
000022| | Some obj0,Some obj1 -> (*[52486]*)Some (Statelattice.join obj0 obj1)) st0 st1
000023|
000024| (* meet : elem -> elem -> elem *)
000029|
000030| (* bot : elem *)
000031| let bot = (*[1]*)LabelMap.empty
000032|
000033|
000034| (** {3 Lattice operations } *)
000035|
000036| (* init : elem *)
000037| let init = (*[1]*)LabelMap.empty
000038|
000039| (* lookup : elem -> label -> Statelattice.elem *)
000040| let lookup lat lab =
000041| (*[8937]*)try (*[8937]*)LabelMap.find lab lat
000042| with Not_found -> (*[1268]*)Statelattice.bot
000043|
000044| (* add : elem -> label -> Statelattice.elem -> elem *)
000045| let add lat lab sl =
000046| (*[4587]*)LabelMap.add lab sl lat
000047|
000048|
000049| (** {2 Pretty printing} *)
000050|
000051| (* pprint : elem -> unit *)
000052| let pprint alat =
000053| begin
000054| Format.printf "{ @[<v 0>";
000055| ignore (LabelMap.fold (fun lab slat first ->
000056| begin
000057| (if first then () else Format.print_space ());
000058| Format.printf "%-is -> " lab;
000059| Statelattice.pprint slat;
000060| false
000061| end) alat true);
000062| Format.printf "@] }";
000063| end
000064|
000065| (* to_string : elem -> string *)
000066| let to_string alat =
000067| let buf = Buffer.create 512 in
000068| let out,flush = Format.get_formatter_output_functions () in (* save previous outputters *)
000069| begin
000070| Format.set_formatter_output_functions (Buffer.add_substring buf) (fun () -> ());
000071| pprint alat;
000072| Format.print_flush ();
000073| Format.set_formatter_output_functions out flush; (* restore previous outputters *)
000074| Buffer.contents buf
000075| end
000025| let meet st0 st1 = (*[0]*)LabelMap.merge (fun lab obj0 obj1 -> match obj0,obj1 with