Project

General

Profile

Revision ef598ac3 src/plugins/salsa/salsaDatatypes.ml

View differences:

src/plugins/salsa/salsaDatatypes.ml
116 116
    | LT.Const_real r -> (* TODO: this is incorrect. We should rather
117 117
				  compute the error associated to the float *)
118 118
       (* let f = float_of_string s in *)
119
       let n = Real.to_num r in
120
       Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_num n)
119
       let n = Real.to_q r in
120
       Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_q n)
121 121
       
122 122
       (* let r = Salsa.Prelude.r_of_f_aux r in *)
123 123
       (* Salsa.Builder.mk_cst (Float.Domain.nnew r r) *)

Also available in: Unified diff