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
3f793898
Commit
3f793898
authored
Jan 22, 2019
by
David Bühler
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
[Ival] Removes useless module about widen hints.
parent
934ce9f2
Changes
6
Hide whitespace changes
Inline
Side-by-side
Showing
6 changed files
with
26 additions
and
41 deletions
+26
-41
src/kernel_services/abstract_interp/ival.ml
src/kernel_services/abstract_interp/ival.ml
+1
-8
src/kernel_services/abstract_interp/ival.mli
src/kernel_services/abstract_interp/ival.mli
+1
-9
src/plugins/value_types/widen_type.ml
src/plugins/value_types/widen_type.ml
+1
-1
tests/misc/oracle/widen_hints.2.res.oracle
tests/misc/oracle/widen_hints.2.res.oracle
+6
-6
tests/misc/oracle/widen_hints.3.res.oracle
tests/misc/oracle/widen_hints.3.res.oracle
+7
-7
tests/misc/oracle/widen_hints2.0.res.oracle
tests/misc/oracle/widen_hints2.0.res.oracle
+10
-10
No files found.
src/kernel_services/abstract_interp/ival.ml
View file @
3f793898
...
...
@@ -44,13 +44,6 @@ let get_small_cardinal () = !small_cardinal
let
emitter
=
Lattice_messages
.
register
"Ival"
let
log_imprecision
s
=
Lattice_messages
.
emit_imprecision
emitter
s
module
Widen_Arithmetic_Value_Set
=
struct
include
Datatype
.
Integer
.
Set
let
default_widen_hints
=
of_list
(
List
.
map
Int
.
of_int
[
-
1
;
0
;
1
])
end
module
O
=
FCSet
.
Make
(
Integer
)
type
t
=
...
...
@@ -63,7 +56,7 @@ type t =
correct representation of [0.] *)
module
Widen_Hints
=
Widen_Arithmetic_Value_
Set
module
Widen_Hints
=
Datatype
.
Integer
.
Set
type
size_widen_hint
=
Integer
.
t
type
numerical_widen_hint
=
Widen_Hints
.
t
*
Fc_float
.
Widen_Hints
.
t
type
widen_hint
=
size_widen_hint
*
numerical_widen_hint
...
...
src/kernel_services/abstract_interp/ival.mli
View file @
3f793898
...
...
@@ -39,15 +39,7 @@ type t
and exact operations.
*)
module
Widen_Hints
:
sig
include
FCSet
.
S
with
type
elt
=
Integer
.
t
include
Datatype
.
S
with
type
t
:=
t
val
default_widen_hints
:
t
end
module
Widen_Hints
=
Datatype
.
Integer
.
Set
type
size_widen_hint
=
Integer
.
t
type
numerical_widen_hint
=
Widen_Hints
.
t
*
Fc_float
.
Widen_Hints
.
t
...
...
src/plugins/value_types/widen_type.ml
View file @
3f793898
...
...
@@ -268,7 +268,7 @@ let float_hints stmto baseo hints =
(* default set of hints. Depends on the machdep *)
let
default
()
=
let
int_default
=
Ival
.
Widen_Hints
.
default_widen_hints
in
let
int_default
=
Ival
.
Widen_Hints
.
of_list
(
List
.
map
Integer
.
of_int
[
-
1
;
0
;
1
])
in
let
float_default
=
Fc_float
.
Widen_Hints
.
default_widen_hints
in
join
(
num_hints
None
None
int_default
)
(
float_hints
None
None
float_default
)
...
...
tests/misc/oracle/widen_hints.2.res.oracle
View file @
3f793898
[kernel] Parsing tests/misc/widen_hints.c (with preprocessing)
[eva:widen-hints] computing global widen hints
[eva:widen-hints] tests/misc/widen_hints.c:71:
adding hint from annotation: a, {87} (for all statements)
adding hint from annotation: a, {
87
} (for all statements)
[eva:widen-hints] tests/misc/widen_hints.c:87:
adding hint from annotation: ss, {87} (for all statements)
adding hint from annotation: ss, {
87
} (for all statements)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
...
...
@@ -21,19 +21,19 @@
[eva:widen-hints] tests/misc/widen_hints.c:97:
computing dynamic hints for statement 48
[eva:widen-hints] tests/misc/widen_hints.c:97:
adding new base due to dynamic widen hint: ip, {87}
adding new base due to dynamic widen hint: ip, {
87
}
[eva] tests/misc/widen_hints.c:98: starting to merge loop iterations
[eva] tests/misc/widen_hints.c:97: starting to merge loop iterations
[eva:widen-hints] tests/misc/widen_hints.c:107:
computing dynamic hints for statement 67
[eva:widen-hints] tests/misc/widen_hints.c:107:
adding new base due to dynamic widen hint: ip2, {87}
adding new base due to dynamic widen hint: ip2, {
87
}
[eva] tests/misc/widen_hints.c:108: starting to merge loop iterations
[eva] tests/misc/widen_hints.c:107: starting to merge loop iterations
[eva:widen-hints] tests/misc/widen_hints.c:118:
computing dynamic hints for statement 91
[eva:widen-hints] tests/misc/widen_hints.c:118:
adding new base due to dynamic widen hint: iarray, {87}
adding new base due to dynamic widen hint: iarray, {
87
}
[eva] tests/misc/widen_hints.c:118: starting to merge loop iterations
[eva] tests/misc/widen_hints.c:116: starting to merge loop iterations
[eva] computing for function using_dynamic_global <- main.
...
...
@@ -41,7 +41,7 @@
[eva:widen-hints] tests/misc/widen_hints.c:58:
computing dynamic hints for statement 2
[eva:widen-hints] tests/misc/widen_hints.c:58:
adding new base due to dynamic widen hint: outer_i, {87}
adding new base due to dynamic widen hint: outer_i, {
87
}
[eva] Recording results for using_dynamic_global
[eva] Done for function using_dynamic_global
[eva] computing for function using_dynamic_global <- main.
...
...
tests/misc/oracle/widen_hints.3.res.oracle
View file @
3f793898
[kernel] Parsing tests/misc/widen_hints.c (with preprocessing)
[eva:widen-hints] computing global widen hints
[eva:widen-hints] tests/misc/widen_hints.c:79:
adding global hint from annotation: for all variables, {88} (for all statements)
adding global hint from annotation: for all variables, {
88
} (for all statements)
[eva:widen-hints] tests/misc/widen_hints.c:71:
adding hint from annotation: a, {87} (for all statements)
adding hint from annotation: a, {
87
} (for all statements)
[eva:widen-hints] tests/misc/widen_hints.c:87:
adding hint from annotation: ss, {87} (for all statements)
adding hint from annotation: ss, {
87
} (for all statements)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
...
...
@@ -31,19 +31,19 @@
[eva:widen-hints] tests/misc/widen_hints.c:97:
computing dynamic hints for statement 70
[eva:widen-hints] tests/misc/widen_hints.c:97:
adding new base due to dynamic widen hint: ip, {87}
adding new base due to dynamic widen hint: ip, {
87
}
[eva] tests/misc/widen_hints.c:97: starting to merge loop iterations
[eva] tests/misc/widen_hints.c:98: starting to merge loop iterations
[eva:widen-hints] tests/misc/widen_hints.c:107:
computing dynamic hints for statement 89
[eva:widen-hints] tests/misc/widen_hints.c:107:
adding new base due to dynamic widen hint: ip2, {87}
adding new base due to dynamic widen hint: ip2, {
87
}
[eva] tests/misc/widen_hints.c:107: starting to merge loop iterations
[eva] tests/misc/widen_hints.c:108: starting to merge loop iterations
[eva:widen-hints] tests/misc/widen_hints.c:118:
computing dynamic hints for statement 113
[eva:widen-hints] tests/misc/widen_hints.c:118:
adding new base due to dynamic widen hint: iarray, {87}
adding new base due to dynamic widen hint: iarray, {
87
}
[eva] tests/misc/widen_hints.c:116: starting to merge loop iterations
[eva] tests/misc/widen_hints.c:118: starting to merge loop iterations
[eva] computing for function using_dynamic_global <- main.
...
...
@@ -51,7 +51,7 @@
[eva:widen-hints] tests/misc/widen_hints.c:58:
computing dynamic hints for statement 22
[eva:widen-hints] tests/misc/widen_hints.c:58:
adding new base due to dynamic widen hint: outer_i, {87}
adding new base due to dynamic widen hint: outer_i, {
87
}
[eva] Recording results for using_dynamic_global
[eva] Done for function using_dynamic_global
[eva] tests/misc/widen_hints.c:123: starting to merge loop iterations
...
...
tests/misc/oracle/widen_hints2.0.res.oracle
View file @
3f793898
[kernel] Parsing tests/misc/widen_hints2.c (with preprocessing)
[eva:widen-hints] computing global widen hints
[eva:widen-hints] tests/misc/widen_hints2.c:46:
adding global hint from annotation: m, {
2
} (for all statements)
adding global hint from annotation: m, {
2
} (for all statements)
[eva:widen-hints] tests/misc/widen_hints2.c:60:
adding global hint from annotation: y_0, {
2
} (for all statements)
adding global hint from annotation: y_0, {
2
} (for all statements)
[eva:widen-hints] tests/misc/widen_hints2.c:20:
adding hint from annotation: for all variables, {88} (for all statements)
adding hint from annotation: for all variables, {
88
} (for all statements)
[eva:widen-hints] tests/misc/widen_hints2.c:47:
adding hint from annotation: y_0, {
5
} (for all statements)
adding hint from annotation: y_0, {
5
} (for all statements)
[eva:widen-hints] tests/misc/widen_hints2.c:49:
adding hint from annotation: a, {
2
} (for all statements)
adding hint from annotation: a, {
2
} (for all statements)
[eva:widen-hints] tests/misc/widen_hints2.c:51:
adding hint from annotation: a, {88} (for all statements)
adding hint from annotation: a, {
88
} (for all statements)
[eva:widen-hints] tests/misc/widen_hints2.c:57:
adding hint from annotation: c, {88} (for all statements)
adding hint from annotation: c, {
88
} (for all statements)
[eva:widen-hints] tests/misc/widen_hints2.c:58:
adding hint from annotation: y_0, {
1
} (for all statements)
adding hint from annotation: y_0, {
1
} (for all statements)
[eva:widen-hints] tests/misc/widen_hints2.c:70:
adding hint from annotation: c_0, {88} (for all statements)
adding hint from annotation: c_0, {
88
} (for all statements)
[eva:widen-hints] tests/misc/widen_hints2.c:78:
adding hint from annotation: glob, {88} (for all statements)
adding hint from annotation: glob, {
88
} (for all statements)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
...
...
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