Revision 151117f7
Added by PierreLoïc Garoche about 6 years ago
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 
"slicedepth", 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
Homogenizing the API for salsa and its use within the plugin