Revision 9a9058f4
Added by PierreLoïc Garoche over 5 years ago
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
More work on Salsa plugin