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
ff9f5326
Commit
ff9f5326
authored
4 years ago
by
Valentin Perrelle
Committed by
Andre Maroneze
4 years ago
Browse files
Options
Downloads
Patches
Plain Diff
[Compliance] Light (only one use of GADT) refactoring
parent
e12caedd
No related branches found
Branches containing commit
No related tags found
Tags containing commit
No related merge requests found
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
tests/libc/check_compliance.ml
+36
-48
36 additions, 48 deletions
tests/libc/check_compliance.ml
tests/libc/oracle/fc_libc.4.res.oracle
+5
-5
5 additions, 5 deletions
tests/libc/oracle/fc_libc.4.res.oracle
with
41 additions
and
53 deletions
tests/libc/check_compliance.ml
+
36
−
48
View file @
ff9f5326
...
@@ -45,53 +45,41 @@ let run_once = ref false
...
@@ -45,53 +45,41 @@ let run_once = ref false
module
StringSet
=
Set
.
Make
(
String
)
module
StringSet
=
Set
.
Make
(
String
)
let
set_of_data_from_list
dir
f
=
module
Json
=
let
file
=
Filename
.
concat
dir
f
in
struct
let
open
Yojson
.
Basic
.
Util
in
open
Yojson
.
Basic
Kernel
.
feedback
"parsing %s"
f
;
open
Util
let
json
=
Yojson
.
Basic
.
from_file
file
in
let
elements
=
json
|>
member
"data"
|>
to_list
in
List
.
fold_left
(
fun
acc
e
->
StringSet
.
add
(
e
|>
to_string
)
acc
)
StringSet
.
empty
elements
let
parse
dir
f
=
let
file
=
Filename
.
concat
dir
f
in
Kernel
.
feedback
"Parsing %s"
f
;
let
json
=
Yojson
.
Basic
.
from_file
file
in
member
"data"
json
let
set_of_data_from_assoc
dir
f
=
let
to_set
(
json
:
t
)
:
StringSet
.
t
=
let
file
=
Filename
.
concat
dir
f
in
json
|>
to_list
|>
List
.
map
to_string
|>
StringSet
.
of_list
let
open
Yojson
.
Basic
.
Util
in
Kernel
.
feedback
"parsing %s"
f
;
let
json
=
Yojson
.
Basic
.
from_file
file
in
let
elements
=
json
|>
member
"data"
|>
to_assoc
in
List
.
fold_left
(
fun
acc
(
ident
,
_
)
->
StringSet
.
add
ident
acc
)
StringSet
.
empty
elements
let
hashtable_of_ident_headers
dir
f
=
let
keys
(
json
:
t
)
:
StringSet
.
t
=
let
file
=
Filename
.
concat
dir
f
in
json
|>
to_assoc
|>
List
.
map
fst
|>
StringSet
.
of_list
let
idents
=
Hashtbl
.
create
500
in
let
open
Yojson
.
Basic
.
Util
in
Kernel
.
feedback
"parsing %s"
f
;
let
json
=
Yojson
.
Basic
.
from_file
file
in
let
elements
=
json
|>
member
"data"
|>
to_assoc
in
List
.
iter
(
fun
(
ident
,
values
)
->
let
header
=
values
|>
member
"header"
|>
to_string
in
Hashtbl
.
replace
idents
ident
header
)
elements
;
idents
let
hashtable_of_ident_headers_and_extensions
dir
f
=
type
_
table_format
=
let
file
=
Filename
.
concat
dir
f
in
|
HeadersOnly
:
string
table_format
let
idents
=
Hashtbl
.
create
500
in
|
HeadersAndExtensions
:
(
string
*
t
list
)
table_format
let
open
Yojson
.
Basic
.
Util
in
Kernel
.
feedback
"parsing %s"
f
;
let
to_table
:
type
a
.
a
table_format
->
t
->
(
string
,
a
)
Hashtbl
.
t
=
let
json
=
Yojson
.
Basic
.
from_file
file
in
let
convert
json
:
a
table_format
->
a
=
function
let
elements
=
json
|>
member
"data"
|>
to_assoc
in
|
HeadersOnly
->
List
.
iter
(
fun
(
ident
,
values
)
->
json
|>
member
"header"
|>
to_string
let
header
=
values
|>
member
"header"
|>
to_string
in
|
HeadersAndExtensions
->
let
extensions
=
values
|>
member
"extensions"
|>
to_list
in
json
|>
member
"header"
|>
to_string
,
Hashtbl
.
replace
idents
ident
(
header
,
extensions
)
json
|>
member
"extensions"
|>
to_list
)
elements
;
in
idents
fun
format
json
->
let
table
=
Hashtbl
.
create
500
in
json
|>
to_assoc
|>
List
.
iter
(
fun
(
ident
,
values
)
->
Hashtbl
.
replace
table
ident
(
convert
values
format
));
table
end
let
()
=
let
()
=
Db
.
Main
.
extend
(
fun
()
->
Db
.
Main
.
extend
(
fun
()
->
...
@@ -101,11 +89,11 @@ let () =
...
@@ -101,11 +89,11 @@ let () =
ignore
(
Visitor
.
visitFramacFile
(
vis
:>
Visitor
.
frama_c_visitor
)
(
Ast
.
get
()
));
ignore
(
Visitor
.
visitFramacFile
(
vis
:>
Visitor
.
frama_c_visitor
)
(
Ast
.
get
()
));
let
fc_stdlib_idents
=
vis
#
get_idents
in
let
fc_stdlib_idents
=
vis
#
get_idents
in
let
dir
=
Filename
.
concat
Fc_config
.
datadir
"compliance"
in
let
dir
=
Filename
.
concat
Fc_config
.
datadir
"compliance"
in
let
c11_idents
=
hashtable_of_ident_headers
dir
"c11_functions.json"
in
let
c11_idents
=
Json
.(
to_table
HeadersOnly
(
parse
dir
"c11_functions.json"
))
let
c11_headers
=
set_of_data_from_list
dir
"c11_headers.json"
in
and
c11_headers
=
Json
.(
to_set
(
parse
dir
"c11_headers.json"
))
let
glibc_idents
=
set_of_data_from_list
dir
"glibc_functions.json"
in
and
glibc_idents
=
Json
.(
to_set
(
parse
dir
"glibc_functions.json"
))
let
posix_idents
=
hashtable_of_ident_headers_and_e
xtensions
dir
"posix_identifiers.json"
in
and
posix_idents
=
Json
.(
to_table
HeadersAndE
xtensions
(
parse
dir
"posix_identifiers.json"
))
let
nonstandard_idents
=
set_of_data_from_assoc
dir
"nonstandard_identifiers.json"
in
and
nonstandard_idents
=
Json
.(
keys
(
parse
dir
"nonstandard_identifiers.json"
))
in
Hashtbl
.
iter
(
fun
id
headers
->
Hashtbl
.
iter
(
fun
id
headers
->
if
not
(
Extlib
.
string_prefix
"__"
id
)
&&
if
not
(
Extlib
.
string_prefix
"__"
id
)
&&
not
(
Extlib
.
string_prefix
"Frama_C"
id
)
&&
not
(
Extlib
.
string_prefix
"Frama_C"
id
)
&&
...
...
This diff is collapsed.
Click to expand it.
tests/libc/oracle/fc_libc.4.res.oracle
+
5
−
5
View file @
ff9f5326
[kernel] Parsing tests/libc/fc_libc.c (with preprocessing)
[kernel] Parsing tests/libc/fc_libc.c (with preprocessing)
[kernel]
p
arsing c11_functions.json
[kernel]
P
arsing c11_functions.json
[kernel]
p
arsing c11_headers.json
[kernel]
P
arsing c11_headers.json
[kernel]
p
arsing glibc_functions.json
[kernel]
P
arsing glibc_functions.json
[kernel]
p
arsing posix_identifiers.json
[kernel]
P
arsing posix_identifiers.json
[kernel]
p
arsing nonstandard_identifiers.json
[kernel]
P
arsing nonstandard_identifiers.json
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