 Timestamp:
 Feb 23, 2013, 1:19:21 AM (8 years ago)
 Location:
 extracted
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

extracted/liveness.ml
r2717 r2718 116 116 let register_lattice = 117 117 { Fixpoints.l_bottom = 118 (Obj.magic { Types.fst = Set_adt.set_empty ; Types.snd =119 Set_adt.set_empty }); Fixpoints.l_equal = (fun left right >118 (Obj.magic { Types.fst = Set_adt.set_empty (); Types.snd = 119 Set_adt.set_empty () }); Fixpoints.l_equal = (fun left right > 120 120 Bool.andb 121 121 (Set_adt.set_equal … … 140 140 let rl_psingleton r = 141 141 Obj.magic { Types.fst = (Set_adt.set_singleton r); Types.snd = 142 Set_adt.set_empty }142 Set_adt.set_empty () } 143 143 144 144 (** val rl_hsingleton : I8051.register > __ **) 145 145 let rl_hsingleton r = 146 Obj.magic { Types.fst = Set_adt.set_empty ; Types.snd =146 Obj.magic { Types.fst = Set_adt.set_empty (); Types.snd = 147 147 (Set_adt.set_singleton r) } 148 148 … … 167 167  Joint.COST_LABEL clabel > rl_bottom 168 168  Joint.CALL (x, x0, x1) > 169 Obj.magic { Types.fst = Set_adt.set_empty ; Types.snd =169 Obj.magic { Types.fst = Set_adt.set_empty (); Types.snd = 170 170 (Set_adt.set_from_list I8051.registerCallerSaved) } 171 171  Joint.COND (r, lbl_true) > rl_bottom … … 238 238  Joint.COST_LABEL clabel > Obj.magic rl_bottom 239 239  Joint.CALL (x, nparams, x0) > 240 { Types.fst = Set_adt.set_empty ; Types.snd =240 { Types.fst = Set_adt.set_empty (); Types.snd = 241 241 (Set_adt.set_from_list 242 242 (Util.prefix (Obj.magic nparams) I8051.registerParams)) } … … 297 297  Joint.GOTO l > Obj.magic rl_bottom 298 298  Joint.RETURN > 299 { Types.fst = Set_adt.set_empty ; Types.snd =299 { Types.fst = Set_adt.set_empty (); Types.snd = 300 300 (Set_adt.set_union (Set_adt.set_from_list I8051.registerCalleeSaved) 301 301 ret_regs) } 
extracted/set_adt.ml
r2717 r2718 128 128 129 129 (** val set_empty : 'a1 set0 **) 130 let set_empty =130 let set_empty _ = 131 131 failwith "AXIOM TO BE REALIZED" 132 132 … … 187 187 (** val set_singleton : 'a1 > 'a1 set0 **) 188 188 let set_singleton elt = 189 set_insert elt set_empty189 set_insert elt (set_empty ()) 190 190 191 191 (** val set_from_list : 'a1 List.list > 'a1 set0 **) 192 192 let set_from_list the_list = 193 List.foldr set_insert set_emptythe_list193 List.foldr set_insert (set_empty ()) the_list 194 194 195 195 (** val set_split : 
extracted/set_adt.mli
r2717 r2718 77 77 val set_jmdiscr : 'a1 set0 > 'a1 set0 > __ 78 78 79 val set_empty : 'a1 set079 val set_empty : unit > 'a1 set0 80 80 81 81 val set_size : 'a1 set0 > Nat.nat
Note: See TracChangeset
for help on using the changeset viewer.