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
488ce255
Commit
488ce255
authored
4 years ago
by
Lionel Blatter
Committed by
Virgile Prevosto
4 years ago
Browse files
Options
Downloads
Patches
Plain Diff
Fix ill-named types and the order of types
parent
412e8a1f
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
src/kernel_services/ast_queries/acsl_extension.ml
+21
-21
21 additions, 21 deletions
src/kernel_services/ast_queries/acsl_extension.ml
with
21 additions
and
21 deletions
src/kernel_services/ast_queries/acsl_extension.ml
+
21
−
21
View file @
488ce255
...
@@ -37,22 +37,22 @@ type extension_visitor =
...
@@ -37,22 +37,22 @@ type extension_visitor =
type
extension_printer
=
type
extension_printer
=
Printer_api
.
extensible_printer_type
->
Format
.
formatter
->
Printer_api
.
extensible_printer_type
->
Format
.
formatter
->
acsl_extension_kind
->
unit
acsl_extension_kind
->
unit
type
extension_s
tandard
=
{
type
extension_s
ingle
=
{
preprocessor
:
extension_preprocessor
;
preprocessor
:
extension_preprocessor
;
typer
:
extension_typer
;
typer
:
extension_typer
;
status
:
bool
;
status
:
bool
;
}
}
type
extension_commun
=
{
category
:
ext_category
;
visitor
:
extension_visitor
;
printer
:
extension_printer
;
short_printer
:
extension_printer
;
}
type
extension_block
=
{
type
extension_block
=
{
preprocessor
:
extension_preprocessor_block
;
preprocessor
:
extension_preprocessor_block
;
typer
:
extension_typer_block
;
typer
:
extension_typer_block
;
status
:
bool
;
status
:
bool
;
}
}
type
extension_common
=
{
category
:
ext_category
;
visitor
:
extension_visitor
;
printer
:
extension_printer
;
short_printer
:
extension_printer
;
}
type
extension
=
{
type
extension
=
{
preprocessor
:
extension_preprocessor
;
preprocessor
:
extension_preprocessor
;
typer
:
extension_typer
;
typer
:
extension_typer
;
...
@@ -82,7 +82,7 @@ let make
...
@@ -82,7 +82,7 @@ let make
?
(
visitor
=
fun
_
_
->
Cil
.
DoChildren
)
?
(
visitor
=
fun
_
_
->
Cil
.
DoChildren
)
?
(
printer
=
default_printer
)
?
(
printer
=
default_printer
)
?
(
short_printer
=
default_short_printer
name
)
?
(
short_printer
=
default_short_printer
name
)
status
:
extension_s
tandard
*
extension_comm
u
n
=
status
:
extension_s
ingle
*
extension_comm
o
n
=
{
preprocessor
;
typer
;
status
}
,
{
category
;
visitor
;
printer
;
short_printer
}
{
preprocessor
;
typer
;
status
}
,
{
category
;
visitor
;
printer
;
short_printer
}
let
make_block
let
make_block
...
@@ -92,24 +92,24 @@ let make_block
...
@@ -92,24 +92,24 @@ let make_block
?
(
visitor
=
fun
_
_
->
Cil
.
DoChildren
)
?
(
visitor
=
fun
_
_
->
Cil
.
DoChildren
)
?
(
printer
=
default_printer
)
?
(
printer
=
default_printer
)
?
(
short_printer
=
default_short_printer
name
)
?
(
short_printer
=
default_short_printer
name
)
status
:
extension_block
*
extension_comm
u
n
=
status
:
extension_block
*
extension_comm
o
n
=
{
preprocessor
;
typer
;
status
}
,
{
category
;
visitor
;
printer
;
short_printer
}
{
preprocessor
;
typer
;
status
}
,
{
category
;
visitor
;
printer
;
short_printer
}
module
Extensions
=
struct
module
Extensions
=
struct
(*hash table for category, visitor, printer and short_priner of extensions*)
(*hash table for category, visitor, printer and short_priner of extensions*)
let
ext_tbl
=
Hashtbl
.
create
5
let
ext_tbl
=
Hashtbl
.
create
5
(*hash table for status, preprocessor and typer of s
tandard
extensions*)
(*hash table for status, preprocessor and typer of s
ingle
extensions*)
let
ext_sta_tbl
=
Hashtbl
.
create
5
let
ext_sta_tbl
=
Hashtbl
.
create
5
(*hash table for status, preprocessor and visitor of block extensions*)
(*hash table for status, preprocessor and visitor of block extensions*)
let
ext_block_tbl
=
Hashtbl
.
create
5
let
ext_block_tbl
=
Hashtbl
.
create
5
let
find_s
tandard
name
:
extension_s
tandard
=
let
find_s
ingle
name
:
extension_s
ingle
=
try
Hashtbl
.
find
ext_sta_tbl
name
with
Not_found
->
try
Hashtbl
.
find
ext_sta_tbl
name
with
Not_found
->
Kernel
.
fatal
~
current
:
true
"unsupported clause of name '%s'"
name
Kernel
.
fatal
~
current
:
true
"unsupported clause of name '%s'"
name
let
find_comm
u
n
name
:
extension_comm
u
n
=
let
find_comm
o
n
name
:
extension_comm
o
n
=
try
Hashtbl
.
find
ext_tbl
name
with
Not_found
->
try
Hashtbl
.
find
ext_tbl
name
with
Not_found
->
Kernel
.
fatal
~
current
:
true
"unsupported clause of name '%s'"
name
Kernel
.
fatal
~
current
:
true
"unsupported clause of name '%s'"
name
...
@@ -155,12 +155,12 @@ module Extensions = struct
...
@@ -155,12 +155,12 @@ module Extensions = struct
Hashtbl
.
add
ext_tbl
name
info2
Hashtbl
.
add
ext_tbl
name
info2
end
end
let
preprocess
name
=
(
find_s
tandard
name
)
.
preprocessor
let
preprocess
name
=
(
find_s
ingle
name
)
.
preprocessor
let
preprocess_block
name
=
(
find_block
name
)
.
preprocessor
let
preprocess_block
name
=
(
find_block
name
)
.
preprocessor
let
typing
name
typing_context
loc
es
=
let
typing
name
typing_context
loc
es
=
let
ext_info
=
find_s
tandard
name
in
let
ext_info
=
find_s
ingle
name
in
let
status
=
ext_info
.
status
in
let
status
=
ext_info
.
status
in
let
typer
=
ext_info
.
typer
in
let
typer
=
ext_info
.
typer
in
let
normal_error
=
ref
false
in
let
normal_error
=
ref
false
in
...
@@ -191,10 +191,10 @@ module Extensions = struct
...
@@ -191,10 +191,10 @@ module Extensions = struct
Kernel
.
fatal
"Typechecking ACSL extension %s raised exception %s"
Kernel
.
fatal
"Typechecking ACSL extension %s raised exception %s"
name
(
Printexc
.
to_string
exn
)
name
(
Printexc
.
to_string
exn
)
let
visit
name
=
(
find_comm
u
n
name
)
.
visitor
let
visit
name
=
(
find_comm
o
n
name
)
.
visitor
let
print
name
printer
fmt
kind
=
let
print
name
printer
fmt
kind
=
let
pp
=
(
find_comm
u
n
name
)
.
printer
printer
in
let
pp
=
(
find_comm
o
n
name
)
.
printer
printer
in
match
kind
with
match
kind
with
|
Ext_annot
(
id
,_
)
->
|
Ext_annot
(
id
,_
)
->
Format
.
fprintf
fmt
"@[<v 2>@[%s %s {@]@
\n
%a}@]"
name
id
pp
kind
Format
.
fprintf
fmt
"@[<v 2>@[%s %s {@]@
\n
%a}@]"
name
id
pp
kind
...
@@ -202,7 +202,7 @@ module Extensions = struct
...
@@ -202,7 +202,7 @@ module Extensions = struct
Format
.
fprintf
fmt
"@[<hov 2>%s %a;@]"
name
pp
kind
Format
.
fprintf
fmt
"@[<hov 2>%s %a;@]"
name
pp
kind
let
short_print
name
printer
fmt
kind
=
let
short_print
name
printer
fmt
kind
=
let
pp
=
(
find_comm
u
n
name
)
.
short_printer
in
let
pp
=
(
find_comm
o
n
name
)
.
short_printer
in
Format
.
fprintf
fmt
"%a"
(
pp
printer
)
kind
Format
.
fprintf
fmt
"%a"
(
pp
printer
)
kind
end
end
...
@@ -245,13 +245,13 @@ let () =
...
@@ -245,13 +245,13 @@ let () =
(* For Deprecation: *)
(* For Deprecation: *)
let
deprecated_replace
name
ext
=
let
deprecated_replace
name
ext
=
let
info1
:
extension_s
tandard
=
{
let
info1
:
extension_s
ingle
=
{
preprocessor
=
ext
.
preprocessor
;
preprocessor
=
ext
.
preprocessor
;
typer
=
ext
.
typer
;
typer
=
ext
.
typer
;
status
=
ext
.
status
;
status
=
ext
.
status
;
}
}
in
in
let
info2
:
extension_comm
u
n
=
{
let
info2
:
extension_comm
o
n
=
{
category
=
ext
.
category
;
category
=
ext
.
category
;
visitor
=
ext
.
visitor
;
visitor
=
ext
.
visitor
;
printer
=
ext
.
printer
;
printer
=
ext
.
printer
;
...
@@ -265,7 +265,7 @@ let strong_cat = Hashtbl.create 5
...
@@ -265,7 +265,7 @@ let strong_cat = Hashtbl.create 5
let
default_typer
_typing_context
_loc
_l
=
assert
false
let
default_typer
_typing_context
_loc
_l
=
assert
false
let
merge
((
info1
:
extension_s
tandard
)
,
(
info2
:
extension_comm
u
n
))
:
extension
=
let
merge
((
info1
:
extension_s
ingle
)
,
(
info2
:
extension_comm
o
n
))
:
extension
=
{
preprocessor
=
info1
.
preprocessor
;
{
preprocessor
=
info1
.
preprocessor
;
typer
=
info1
.
typer
;
typer
=
info1
.
typer
;
status
=
info1
.
status
;
status
=
info1
.
status
;
...
@@ -280,7 +280,7 @@ let deprecated_find ?(strong=true) name cat op_name =
...
@@ -280,7 +280,7 @@ let deprecated_find ?(strong=true) name cat op_name =
if
strong
then
Hashtbl
.
add
strong_cat
name
cat
;
if
strong
then
Hashtbl
.
add
strong_cat
name
cat
;
merge
(
make
name
cat
default_typer
false
)
merge
(
make
name
cat
default_typer
false
)
|
Some
ext1
->
|
Some
ext1
->
let
ext2
=
Extensions
.
find_comm
u
n
name
in
let
ext2
=
Extensions
.
find_comm
o
n
name
in
if
strong
&&
Hashtbl
.
mem
strong_cat
name
then
begin
if
strong
&&
Hashtbl
.
mem
strong_cat
name
then
begin
if
ext2
.
category
=
cat
then
merge
(
ext1
,
ext2
)
if
ext2
.
category
=
cat
then
merge
(
ext1
,
ext2
)
else
else
...
...
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