Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
pub
frama-c
Commits
4ddc7cfc
Commit
4ddc7cfc
authored
Jul 05, 2019
by
David Bühler
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
[Ival] Implements fold_int_decreasing, which iterates on decreasing order.
parent
a0ce5873
Changes
8
Hide whitespace changes
Inline
Side-by-side
Showing
8 changed files
with
35 additions
and
18 deletions
+35
-18
src/kernel_services/abstract_interp/int_interval.ml
src/kernel_services/abstract_interp/int_interval.ml
+4
-2
src/kernel_services/abstract_interp/int_interval.mli
src/kernel_services/abstract_interp/int_interval.mli
+1
-1
src/kernel_services/abstract_interp/int_set.ml
src/kernel_services/abstract_interp/int_set.ml
+4
-1
src/kernel_services/abstract_interp/int_set.mli
src/kernel_services/abstract_interp/int_set.mli
+1
-1
src/kernel_services/abstract_interp/int_val.ml
src/kernel_services/abstract_interp/int_val.ml
+11
-11
src/kernel_services/abstract_interp/int_val.mli
src/kernel_services/abstract_interp/int_val.mli
+3
-2
src/kernel_services/abstract_interp/ival.ml
src/kernel_services/abstract_interp/ival.ml
+6
-0
src/kernel_services/abstract_interp/ival.mli
src/kernel_services/abstract_interp/ival.mli
+5
-0
No files found.
src/kernel_services/abstract_interp/int_interval.ml
View file @
4ddc7cfc
...
...
@@ -415,10 +415,12 @@ let cardinal_zero_or_one t =
let
diff
v
_
=
`Value
v
let
diff_if_one
v
_
=
`Value
v
let
fold_int
f
t
acc
=
let
fold_int
?
(
increasing
=
true
)
f
t
acc
=
match
t
.
min
,
t
.
max
with
|
None
,
_
|
_
,
None
->
raise
Error_Top
|
Some
inf
,
Some
sup
->
Int
.
fold
f
~
inf
~
sup
~
step
:
t
.
modu
acc
|
Some
inf
,
Some
sup
->
let
step
=
if
increasing
then
t
.
modu
else
Int
.
neg
t
.
modu
in
Int
.
fold
f
~
inf
~
sup
~
step
acc
let
fold_enum
f
v
acc
=
fold_int
(
fun
x
acc
->
f
(
inject_singleton
x
)
acc
)
v
acc
...
...
src/kernel_services/abstract_interp/int_interval.mli
View file @
4ddc7cfc
...
...
@@ -87,4 +87,4 @@ val subdivide: t -> t * t
val
reduce_sign
:
t
->
bool
->
t
or_bottom
val
reduce_bit
:
int
->
t
->
bool
->
t
or_bottom
val
fold_int
:
(
Integer
.
t
->
'
a
->
'
a
)
->
t
->
'
a
->
'
a
val
fold_int
:
?
increasing
:
bool
->
(
Integer
.
t
->
'
a
->
'
a
)
->
t
->
'
a
->
'
a
src/kernel_services/abstract_interp/int_set.ml
View file @
4ddc7cfc
...
...
@@ -148,7 +148,10 @@ let for_all f (a : Integer.t array) =
let
exists
=
Extlib
.
array_exists
let
iter
=
Array
.
iter
let
fold
=
Array
.
fold_left
let
fold
?
(
increasing
=
true
)
=
if
increasing
then
fun
f
array
acc
->
Array
.
fold_left
(
fun
acc
x
->
f
x
acc
)
acc
array
else
Array
.
fold_right
let
truncate_no_bottom
r
i
=
assert
(
i
>
0
);
...
...
src/kernel_services/abstract_interp/int_set.mli
View file @
4ddc7cfc
...
...
@@ -75,7 +75,7 @@ val cardinal: t -> int
val
for_all
:
(
Integer
.
t
->
bool
)
->
t
->
bool
val
exists
:
(
Integer
.
t
->
bool
)
->
t
->
bool
val
iter
:
(
Integer
.
t
->
unit
)
->
t
->
unit
val
fold
:
(
'
a
->
Integer
.
t
->
'
a
)
->
'
a
->
t
->
'
a
val
fold
:
?
increasing
:
bool
->
(
Integer
.
t
->
'
a
->
'
a
)
->
t
->
'
a
->
'
a
val
map
:
(
Integer
.
t
->
Integer
.
t
)
->
t
->
t
val
filter
:
(
Integer
.
t
->
bool
)
->
t
->
t
or_bottom
val
map_reduce
:
(
Integer
.
t
->
'
a
)
->
(
'
a
->
'
a
->
'
a
)
->
t
->
'
a
...
...
src/kernel_services/abstract_interp/int_val.ml
View file @
4ddc7cfc
...
...
@@ -192,12 +192,12 @@ let make_top_from_set s =
let
min
=
Int_set
.
min
s
in
let
modu
=
Int_set
.
fold
(
fun
acc
x
->
(
fun
x
acc
->
if
Int
.
equal
x
min
then
acc
else
Int
.
pgcd
(
Int
.
sub
x
min
)
acc
)
Int
.
zero
s
Int
.
zero
in
let
rem
=
Int
.
e_rem
min
modu
in
let
max
=
Some
(
Int_set
.
max
s
)
in
...
...
@@ -243,10 +243,10 @@ let contains_non_zero = function
|
Itv
_
->
true
(* at least two values *)
|
Set
_
as
s
->
not
(
is_zero
s
)
let
fold_int
f
v
acc
=
let
fold_int
?
(
increasing
=
true
)
f
v
acc
=
match
v
with
|
Itv
i
->
Int_interval
.
fold_int
f
i
acc
|
Set
s
->
Int_set
.
fold
(
fun
acc
x
->
f
x
acc
)
acc
s
|
Itv
i
->
Int_interval
.
fold_int
~
increasing
f
i
acc
|
Set
s
->
Int_set
.
fold
~
increasing
f
s
acc
let
fold_enum
f
v
acc
=
fold_int
(
fun
x
acc
->
f
(
inject_singleton
x
)
acc
)
v
acc
...
...
@@ -385,8 +385,8 @@ let join v1 v2 =
let
l
=
Int_set
.
cardinal
s
in
if
l
=
0
then
t
else
let
f
modu
elt
=
Int
.
pgcd
modu
(
Int
.
abs
(
Int
.
sub
r
elt
))
in
let
modu
=
Int_set
.
fold
f
modu
s
in
let
f
elt
modu
=
Int
.
pgcd
modu
(
Int
.
abs
(
Int
.
sub
r
elt
))
in
let
modu
=
Int_set
.
fold
f
s
modu
in
let
rem
=
Int
.
e_rem
r
modu
in
let
min
=
match
min
with
None
->
None
...
...
@@ -527,9 +527,9 @@ let div x y =
match
y
with
|
Set
sy
->
Int_set
.
fold
(
fun
acc
elt
->
(
fun
elt
acc
->
Bottom
.
join
join
acc
(
scale_div_or_bottom
~
pos
:
false
elt
x
))
`Bottom
sy
sy
`Bottom
|
Itv
iy
->
Int_interval
.
div
(
make_range
x
)
iy
>>-:
inject_itv
(* [scale_rem ~pos:false f v] is an over-approximation of the set of
...
...
@@ -550,10 +550,10 @@ let c_rem x y =
match
x
with
|
Set
xx
->
inject_set_or_top_or_bottom
(
Int_set
.
c_rem
xx
yy
)
|
Itv
_
->
let
f
acc
y
=
let
f
y
acc
=
Bottom
.
join
join
(
scale_rem_or_bottom
~
pos
:
false
y
x
)
acc
in
Int_set
.
fold
f
`Bottom
yy
Int_set
.
fold
f
yy
`Bottom
(** Computes [x (op) ({y >= 0} * 2^n)], as an auxiliary function for
[shift_left] and [shift_right]. [op] and [scale] must verify
...
...
src/kernel_services/abstract_interp/int_val.mli
View file @
4ddc7cfc
...
...
@@ -173,9 +173,10 @@ val all_values: size:Integer.t -> t -> bool
val
overlaps
:
partial
:
bool
->
size
:
Integer
.
t
->
t
->
t
->
bool
(** Iterates on all integers represented by an abstraction.
(** Iterates on all integers represented by an abstraction, in increasing order
by default. If [increasing] is set to false, iterate by decreasing order.
@raise Abstract_interp.Error_Top if the abstraction is unbounded. *)
val
fold_int
:
(
Integer
.
t
->
'
a
->
'
a
)
->
t
->
'
a
->
'
a
val
fold_int
:
?
increasing
:
bool
->
(
Integer
.
t
->
'
a
->
'
a
)
->
t
->
'
a
->
'
a
(** Low-level operation for demarshalling *)
val
rehash
:
t
->
t
src/kernel_services/abstract_interp/ival.ml
View file @
4ddc7cfc
...
...
@@ -398,6 +398,12 @@ let fold_int f v acc =
|
Float
_
->
raise
Error_Top
|
Int
i
->
Int_val
.
fold_int
f
i
acc
let
fold_int_decrease
f
v
acc
=
match
v
with
|
Bottom
->
acc
|
Float
_
->
raise
Error_Top
|
Int
i
->
Int_val
.
fold_int
~
increasing
:
false
f
i
acc
let
fold_enum
f
v
acc
=
match
v
with
|
Bottom
->
acc
...
...
src/kernel_services/abstract_interp/ival.mli
View file @
4ddc7cfc
...
...
@@ -187,6 +187,11 @@ val fold_int : (Integer.t -> 'a -> 'a) -> t -> 'a -> 'a
Raise {!Abstract_interp.Error_Top} if the argument is a float or a
potentially infinite integer. *)
val
fold_int_decrease
:
(
Integer
.
t
->
'
a
->
'
a
)
->
t
->
'
a
->
'
a
(** Iterate on the integer values of the ival in decreasing order.
Raise {!Abstract_Interp.Error_Top} if the argument is a float or a
potentially infinite integer. *)
val
fold_enum
:
(
t
->
'
a
->
'
a
)
->
t
->
'
a
->
'
a
(** Iterate on every value of the ival. Raise {!Abstract_intrep.Error_Top} if
the argument is a non-singleton float or a potentially infinite integer. *)
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment