apron-example/test.ml at master · SPY-Lab/apron-example · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
(* ocamlbuild -pkgs apron.boxMPQ,apron,apron.apron,apron.octMPQ test.native -- *)

(* Tests of Apron's functions *)

open Apron;;
open Mpqf;;
open Format;;

(*vars definition*)
let var_x = Var.of_string "x";;
let var_y = Var.of_string "y";;


(* box manager*)
let manBox = Box.manager_alloc();;

(* oct manager *)
let manOct = Oct.manager_alloc();;

(*Making an environment from a set of integer (empty) and real variables.*)
 let env = Environment.make
    [||]
    [|var_x; var_y|];;

(* Removing var_y to the environment *)
let env = Environment.remove env [|var_y|];;

(* Adding var_y to the environment *)
let env = Environment.add env [||] [|var_y|];;

(*how to create an abstract domain TOP*)
let abs_top = Abstract1.top manBox env;;

(*how to create an abstract domain BOTTOM*)
let abs_bottom = Abstract1.bottom manBox env;;

(*how to create an interval TOP*)
let interval_top = Interval.top;;

(*how to create an interval BOTTOM*)
let interval_bottom = Interval.bottom;;

(*how to create an interval of integer*)
let interval =  Interval.of_int 4 12;;

(* Scalar.of_infty  Create a scalar of type Float with the value multiplied
 by infinity (resulting in minus infinity, zero, or infinity) *)
let interval =  Interval.of_scalar (Scalar.of_int 0) (Scalar.of_infty 1);;

(* Change interval *)
Interval.set_infsup interval (Scalar.of_int 0) (Scalar.of_infty 1);;

(* Create an abstract domain Box *)
let abs1 = Abstract1.of_box manBox env [|var_x;var_y|]
    [|
      interval;
      Interval.of_int 3 5;
    |];;

let abs2 = Abstract1.of_box manBox env [|var_x;var_y|]
    [|
      Interval.of_int 0 14;
      Interval.of_int 7 9;
    |];;

(* Join *)
let joinBox = Abstract1.join manBox abs1 abs2;;

(* Meet *)
let meetBox = Abstract1.meet manBox abs1 abs2;;

(* Watch the interval of a variable *)
let intervallo = Abstract1.bound_variable manBox abs1 var_x;;

(* Create an Abstract Domain Oct *)
let abs3 = Abstract1.of_box manOct env [|var_x;var_y|]
    [|
      interval1;
      Interval.of_int 4 12;
    |];;

     let abs4 = Abstract1.of_box manOct env [|var_x;var_y|]
    [|
      Interval.of_int 0 14;
      Interval.of_int 4 12;
    |];;

(* Join *)
let joinOct = Abstract1.join manOct abs3 abs4;;

(* Meet *)
let meetOct = Abstract1.meet manOct abs3 abs4;;


(* Print box *)
printf "abs1=%a@.abs2=%a@.joinBox=%a@.meetBox=%a"
  Abstract1.print abs1
  Abstract1.print abs2
  Abstract1.print joinBox
  Abstract1.print meetBox
;;

printf("\n");;
printf "Intervallo var_x: %a" Interval.print intervallo;;
printf("\n");;

printf "sup: %a"
Scalar.print intervallo.sup;;

(* Print oct *)
printf "abs3=%a@.abs4=%a@.joinOct=%a@.meetOct=%a"
  Abstract1.print abs3
  Abstract1.print abs4
  Abstract1.print joinOct
  Abstract1.print meetOct
;;

printf("\n");;
printf "Intervallo var_x: %a" Interval.print intervallo;;

printf("\n");;