Project

General

Profile

Revision 151117f7 src/plugins/salsa/salsaDatatypes.ml

View differences:

src/plugins/salsa/salsaDatatypes.ml
2 2
module MT = Machine_code_types
3 3
module MC = Machine_code_common
4 4
module ST = Salsa.Types
5
module Float = Salsa.Float
6 5

  
7 6
let debug = ref false
8 7

  
......
82 81
struct
83 82
  type t = ST.abstractValue
84 83

  
85
  let pp fmt (f,r) =
84
  let pp fmt ((f,r):t) =
86 85
    let fs, rs = (Salsa.Float.Domain.print (f,r)) in
87 86
    Format.fprintf fmt "%s + %s" fs rs 
88 87
(*    match f, r with
......
100 99
    | _ -> Format.eprintf "%a cup %a failed@.@?" pp v1 pp v2; assert false 
101 100
*)
102 101
  let inject cst = match cst with  
103
    | LT.Const_int(i)  -> Salsa.Builder.mk_cst (ST.R(Salsa.NumMartel.of_int i, []), ST.R(Salsa.NumMartel.of_int i , []))
102
    | LT.Const_int(i)  -> Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_float (float_of_int i))
104 103
    | LT.Const_real (c,e,s) -> (* TODO: this is incorrect. We should rather
105 104
				  compute the error associated to the float *)
106
       let r = float_of_string s  in
107
       let r = Salsa.Prelude.r_of_f_aux r in
108
       Salsa.Builder.mk_cst (Float.Domain.nnew r r)
105
       let f = float_of_string s  in
106
       Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_float f)
107
       
108
       (* let r = Salsa.Prelude.r_of_f_aux r in *)
109
       (* Salsa.Builder.mk_cst (Float.Domain.nnew r r) *)
109 110
	 
110 111
      (* let r = float_of_string s  in *)
111 112
      (* if r = 0. then *)
......
241 242
    MC.mk_val (MT.Fun (op, [x;y])) t
242 243
  in
243 244
  match e with
244
    ST.Cst((ST.R(c,_),_),_)     -> (* We project ranges into constants. We
245
    ST.Cst(abs_val,_)     -> (* We project ranges into constants. We
245 246
					forget about errors and provide the
246 247
					mean/middle value of the interval
247
				     *)
248
      let  new_float = Salsa.NumMartel.float_of_num c in
248
			      *)
249
    let new_float = Salsa.Float.Domain.to_float abs_val in
250
      (* let  new_float = Salsa.NumMartel.float_of_num c in *)
249 251
      (* let new_float =  *)
250 252
      (* 	if f1 = f2 then *)
251 253
      (* 	  f1 *)

Also available in: Unified diff