Project

General

Profile

Revision 9a9058f4 src/plugins/salsa/salsaDatatypes.ml

View differences:

src/plugins/salsa/salsaDatatypes.ml
112 112
    | _ -> Format.eprintf "%a cup %a failed@.@?" pp v1 pp v2; assert false 
113 113
*)
114 114
  let inject cst = match cst with  
115
    | LT.Const_int(i)  -> Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_float (float_of_int i))
115
    | LT.Const_int(i)  -> Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_int i)
116 116
    | LT.Const_real (c,e,s) -> (* TODO: this is incorrect. We should rather
117 117
				  compute the error associated to the float *)
118
       let f = float_of_string s  in
119
       Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_float f)
118
       (* let f = float_of_string s in *)
119
       let n = Corelang.cst_real_to_num c e in
120
       Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_num n)
120 121
       
121 122
       (* let r = Salsa.Prelude.r_of_f_aux r in *)
122 123
       (* Salsa.Builder.mk_cst (Float.Domain.nnew r r) *)
......
128 129
      (* 	Salsa.Builder.mk_cst (ST.I(r*.(1.-.epsilon_float),r*.(1.+.epsilon_float)),Float.ulp (ST.I(r,r))) *)
129 130
    | _ -> assert false
130 131

  
131
  let leq = Salsa.Float.feSseq
132
  let leq = (* Salsa.Float.feSseq *) Salsa.Float.Domain.leq
132 133
end
133 134

  
134 135
module RangesInt = Ranges (FloatIntSalsa)

Also available in: Unified diff