Project

General

Profile

« Previous | Next » 

Revision 9a9058f4

Added by Pierre-Loïc Garoche over 5 years ago

More work on Salsa plugin

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