Project

General

Profile

Revision 151117f7

View differences:

src/plugins/salsa/machine_salsa_opt.ml
634 634
	      Printers.pp_expr value.LT.eexpr_qfexpr; 
635 635
	    assert false 
636 636
	in
637
	let minv:Salsa.NumMartel.num = Salsa.NumMartel.of_num (get_cst minv) and
638
	    maxv = Salsa.NumMartel.of_num (get_cst maxv) in
637
	(* let minv = Salsa.Float.Domain.of_num (get_cst minv) and *)
638
	(*     maxv = Salsa.Float.Domain.of_num (get_cst maxv) in *)
639 639
	(* if !debug then Format.eprintf "variable %s in [%s, %s]@ " v (Num.string_of_num minv) (Num.string_of_num maxv); *)
640
	RangesInt.enlarge ranges v (Salsa.Float.Domain.nnew minv maxv)
640
	RangesInt.enlarge ranges v (Salsa.Float.Domain.inject_nums (get_cst minv) (get_cst maxv))
641 641
      )
642 642
      | _ -> 
643 643
	Format.eprintf 
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 *)
src/plugins/salsa/salsa_plugin.ml
13 13
  
14 14
  let options = [
15 15
        "-debug", Arg.Set SalsaDatatypes.debug, "debug salsa plugin";
16
        "-slice-depth", Arg.Set_int Salsa.Prelude.sliceSize, "salsa slice depth (default is 5)";
16 17
      ]
17 18

  
18 19
  let activate () = salsa_enabled := true

Also available in: Unified diff