Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
frama-c
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container Registry
Model registry
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pub
frama-c
Commits
9e882764
Commit
9e882764
authored
3 years ago
by
Andre Maroneze
Browse files
Options
Downloads
Patches
Plain Diff
[analysis-scripts] estimate-difficulty: improve estimation and warnings
parent
a504b1e2
No related branches found
No related tags found
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
share/analysis-scripts/estimate_difficulty.py
+31
-16
31 additions, 16 deletions
share/analysis-scripts/estimate_difficulty.py
with
31 additions
and
16 deletions
share/analysis-scripts/estimate_difficulty.py
+
31
−
16
View file @
9e882764
...
@@ -82,7 +82,7 @@ re_include = re.compile(r'\s*#\s*include\s*("|<)([^">]+)("|>)')
...
@@ -82,7 +82,7 @@ re_include = re.compile(r'\s*#\s*include\s*("|<)([^">]+)("|>)')
def
grep_includes_in_file
(
filename
):
def
grep_includes_in_file
(
filename
):
file_content
=
source_filter
.
open_and_filter
(
filename
,
not
under_test
)
file_content
=
source_filter
.
open_and_filter
(
filename
,
not
under_test
)
i
=
0
i
=
0
for
line
in
f
.
read
lines
():
for
line
in
f
ile_content
.
split
lines
():
i
+=
1
i
+=
1
m
=
re_include
.
match
(
line
)
m
=
re_include
.
match
(
line
)
if
m
:
if
m
:
...
@@ -165,9 +165,10 @@ for callee in sorted(callees):
...
@@ -165,9 +165,10 @@ for callee in sorted(callees):
warnings
+=
1
warnings
+=
1
if
verbose
or
debug
or
status
==
"
warning
"
:
if
verbose
or
debug
or
status
==
"
warning
"
:
print
(
f
"
-
{
status
}
:
{
callee
}
(
{
standard
}
)
{
reason
}
"
)
print
(
f
"
-
{
status
}
:
{
callee
}
(
{
standard
}
)
{
reason
}
"
)
#print(f"callee: {callee}")
is_problematic
=
callee
in
posix_identifiers
and
"
notes
"
in
posix_identifiers
[
callee
]
and
"
fc-support
"
in
posix_identifiers
[
callee
][
"
notes
"
]
and
posix_identifiers
[
callee
][
"
notes
"
][
"
fc-support
"
]
==
"
problematic
"
if
callee
in
posix_identifiers
:
if
callee
in
posix_identifiers
:
used_headers
.
add
(
posix_identifiers
[
callee
][
"
header
"
])
used_headers
.
add
(
posix_identifiers
[
callee
][
"
header
"
])
status_emitted
=
False
# to avoid re-emitting a message for functions in both C11 and POSIX
if
callee
in
c11_functions
:
if
callee
in
c11_functions
:
standard
=
"
C11
"
standard
=
"
C11
"
# check that the callee is not a macro or type (e.g. va_arg);
# check that the callee is not a macro or type (e.g. va_arg);
...
@@ -175,30 +176,40 @@ for callee in sorted(callees):
...
@@ -175,30 +176,40 @@ for callee in sorted(callees):
# so we must test membership before checking the POSIX type
# so we must test membership before checking the POSIX type
if
callee
in
posix_identifiers
and
posix_identifiers
[
callee
][
"
id_type
"
]
!=
"
function
"
:
if
callee
in
posix_identifiers
and
posix_identifiers
[
callee
][
"
id_type
"
]
!=
"
function
"
:
continue
continue
#print(f"C11 function: {callee}")
if
(
not
is_problematic
)
and
callee
in
libc_specified_functions
:
if
callee
in
libc_specified_functions
:
callee_status
(
"
good
"
,
standard
,
"
is specified in Frama-C
'
s libc
"
)
callee_status
(
"
good
"
,
standard
,
"
is specified in Frama-C
'
s libc
"
)
elif
callee
in
libc_defined_functions
:
status_emitted
=
True
elif
(
not
is_problematic
)
and
callee
in
libc_defined_functions
:
callee_status
(
"
ok
"
,
standard
,
"
is defined in Frama-C
'
s libc
"
)
callee_status
(
"
ok
"
,
standard
,
"
is defined in Frama-C
'
s libc
"
)
status_emitted
=
True
else
:
else
:
# Some functions without specification are actually variadic
if
callee
not
in
posix_identifiers
:
# (and possibly handled by the Variadic plug-in)
if
callee
in
posix_identifiers
and
"
notes
"
in
posix_identifiers
[
callee
]
and
"
variadic-plugin
"
in
posix_identifiers
[
callee
][
"
notes
"
]:
callee_status
(
"
ok
"
,
standard
,
"
is handled by the Variadic plug-in
"
)
else
:
callee_status
(
"
warning
"
,
standard
,
"
has neither code nor spec in Frama-C
'
s libc
"
)
callee_status
(
"
warning
"
,
standard
,
"
has neither code nor spec in Frama-C
'
s libc
"
)
elif
callee
in
posix_identifiers
:
status_emitted
=
True
if
not
status_emitted
and
callee
in
posix_identifiers
:
standard
=
"
POSIX
"
standard
=
"
POSIX
"
# check that the callee is not a macro or type (e.g. va_arg)
# check that the callee is not a macro or type (e.g. va_arg)
if
posix_identifiers
[
callee
][
"
id_type
"
]
!=
"
function
"
:
if
posix_identifiers
[
callee
][
"
id_type
"
]
!=
"
function
"
:
continue
continue
#print(f"Non-C11, POSIX function: {callee}")
if
(
not
is_problematic
)
and
callee
in
libc_specified_functions
:
if
callee
in
libc_specified_functions
:
callee_status
(
"
good
"
,
standard
,
"
specified in Frama-C
'
s libc
"
)
callee_status
(
"
good
"
,
standard
,
"
specified in Frama-C
'
s libc
"
)
elif
callee
in
libc_defined_functions
:
status_emitted
=
True
elif
(
not
is_problematic
)
and
callee
in
libc_defined_functions
:
callee_status
(
"
ok
"
,
standard
,
"
defined in Frama-C
'
s libc
"
)
callee_status
(
"
ok
"
,
standard
,
"
defined in Frama-C
'
s libc
"
)
status_emitted
=
True
else
:
else
:
callee_status
(
"
warning
"
,
standard
,
"
has neither code nor spec in Frama-C
'
s libc
"
)
# Some functions without specification are actually variadic
# (and possibly handled by the Variadic plug-in)
if
"
notes
"
in
posix_identifiers
[
callee
]:
if
"
variadic-plugin
"
in
posix_identifiers
[
callee
][
"
notes
"
]:
callee_status
(
"
ok
"
,
standard
,
"
is handled by the Variadic plug-in
"
)
status_emitted
=
True
elif
is_problematic
:
callee_status
(
"
warning
"
,
standard
,
"
is known to be problematic for code analysis
"
)
status_emitted
=
True
if
not
status_emitted
:
callee_status
(
"
warning
"
,
standard
,
"
has neither code nor spec in Frama-C
'
s libc
"
)
print
(
f
"
Function-related warnings:
{
warnings
}
"
)
print
(
f
"
Function-related warnings:
{
warnings
}
"
)
if
(
verbose
or
debug
)
and
used_headers
:
if
(
verbose
or
debug
)
and
used_headers
:
...
@@ -217,12 +228,15 @@ def is_local_header(header_dirs, header):
...
@@ -217,12 +228,15 @@ def is_local_header(header_dirs, header):
print
(
f
"
Estimating difficulty for
{
len
(
chevron_includes
)
}
'
#include <header>
'
directives...
"
)
print
(
f
"
Estimating difficulty for
{
len
(
chevron_includes
)
}
'
#include <header>
'
directives...
"
)
non_posix_headers
=
[]
non_posix_headers
=
[]
header_warnings
=
0
for
header
in
sorted
(
chevron_includes
,
key
=
str
.
casefold
):
for
header
in
sorted
(
chevron_includes
,
key
=
str
.
casefold
):
if
header
in
posix_headers
:
if
header
in
posix_headers
:
fc_support
=
posix_headers
[
header
][
"
fc-support
"
]
fc_support
=
posix_headers
[
header
][
"
fc-support
"
]
if
fc_support
==
"
unsupported
"
:
if
fc_support
==
"
unsupported
"
:
header_warnings
+=
1
print
(
f
"
- WARNING: included header <
{
header
}
> is explicitly unsupported by Frama-C
"
)
print
(
f
"
- WARNING: included header <
{
header
}
> is explicitly unsupported by Frama-C
"
)
elif
fc_support
==
"
none
"
:
elif
fc_support
==
"
none
"
:
header_warnings
+=
1
print
(
f
"
- warning: included header <
{
header
}
> not currently included in Frama-C
'
s libc
"
)
print
(
f
"
- warning: included header <
{
header
}
> not currently included in Frama-C
'
s libc
"
)
else
:
else
:
if
verbose
or
debug
:
if
verbose
or
debug
:
...
@@ -234,8 +248,9 @@ for header in sorted(chevron_includes, key=str.casefold):
...
@@ -234,8 +248,9 @@ for header in sorted(chevron_includes, key=str.casefold):
print
(
f
"
- ok: included header <
{
header
}
> seems to be available locally
"
)
print
(
f
"
- ok: included header <
{
header
}
> seems to be available locally
"
)
else
:
else
:
non_posix_headers
.
append
(
header
)
non_posix_headers
.
append
(
header
)
header_warnings
+=
1
print
(
f
"
- warning: included non-POSIX header <
{
header
}
>
"
)
print
(
f
"
- warning: included non-POSIX header <
{
header
}
>
"
)
print
(
f
"
Header-related warnings:
{
len
(
non_posix_headers
)
}
"
)
print
(
f
"
Header-related warnings:
{
header_warnings
}
"
)
# dynamic allocation
# dynamic allocation
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment