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
f6f01899
Commit
f6f01899
authored
4 years ago
by
Lionel Blatter
Committed by
Virgile Prevosto
4 years ago
Browse files
Options
Downloads
Patches
Plain Diff
Review of short printer for acsl_extensions.
Fix typos in comments. Fix ill-named variable.
parent
488ce255
No related branches found
Branches containing commit
No related tags found
Tags containing commit
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
+8
-11
8 additions, 11 deletions
src/kernel_services/ast_queries/acsl_extension.ml
with
8 additions
and
11 deletions
src/kernel_services/ast_queries/acsl_extension.ml
+
8
−
11
View file @
f6f01899
...
...
@@ -70,10 +70,7 @@ let default_printer printer fmt = function
|
Ext_annot
(
_
,
an
)
->
Pretty_utils
.
pp_list
~
pre
:
"@[<v 0>"
~
suf
:
"@]@
\n
"
~
sep
:
"@
\n
"
printer
#
extended
fmt
an
let
default_short_printer
name
printer
fmt
=
function
|
Ext_id
_
|
Ext_terms
_
|
Ext_preds
_
->
Format
.
fprintf
fmt
"%s"
name
|
Ext_annot
(
id
,
an
)
->
Format
.
fprintf
fmt
"%s@ {@
\n
%a@]@
\n
}"
id
(
Pretty_utils
.
pp_list
~
sep
:
"@
\n
"
printer
#
extended
)
an
let
default_short_printer
name
_printer
fmt
_ext_kind
=
Format
.
fprintf
fmt
"%s"
name
let
make
name
category
...
...
@@ -96,17 +93,17 @@ let make_block
{
preprocessor
;
typer
;
status
}
,
{
category
;
visitor
;
printer
;
short_printer
}
module
Extensions
=
struct
(*hash table for category, visitor, printer and short_priner of extensions*)
(*hash table for category, visitor, printer and short_prin
t
er of extensions*)
let
ext_tbl
=
Hashtbl
.
create
5
(*hash table for status, preprocessor and typer of single extensions*)
let
ext_s
ta
_tbl
=
Hashtbl
.
create
5
let
ext_s
ingle
_tbl
=
Hashtbl
.
create
5
(*hash table for status, preprocessor and
visito
r of block extensions*)
(*hash table for status, preprocessor and
type
r of block extensions*)
let
ext_block_tbl
=
Hashtbl
.
create
5
let
find_single
name
:
extension_single
=
try
Hashtbl
.
find
ext_s
ta
_tbl
name
with
Not_found
->
try
Hashtbl
.
find
ext_s
ingle
_tbl
name
with
Not_found
->
Kernel
.
fatal
~
current
:
true
"unsupported clause of name '%s'"
name
let
find_common
name
:
extension_common
=
...
...
@@ -136,7 +133,7 @@ module Extensions = struct
name
else
begin
Hashtbl
.
add
ext_s
ta
_tbl
name
info1
;
Hashtbl
.
add
ext_s
ingle
_tbl
name
info1
;
Hashtbl
.
add
ext_tbl
name
info2
end
...
...
@@ -258,7 +255,7 @@ let deprecated_replace name ext =
short_printer
=
ext
.
printer
;
}
in
Hashtbl
.
add
Extensions
.
ext_s
ta
_tbl
name
info1
;
Hashtbl
.
add
Extensions
.
ext_s
ingle
_tbl
name
info1
;
Hashtbl
.
add
Extensions
.
ext_tbl
name
info2
let
strong_cat
=
Hashtbl
.
create
5
...
...
@@ -275,7 +272,7 @@ let merge ((info1:extension_single),(info2:extension_common)) :extension =
short_printer
=
info2
.
printer
}
let
deprecated_find
?
(
strong
=
true
)
name
cat
op_name
=
match
Hashtbl
.
find_opt
Extensions
.
ext_s
ta
_tbl
name
with
match
Hashtbl
.
find_opt
Extensions
.
ext_s
ingle
_tbl
name
with
|
None
->
if
strong
then
Hashtbl
.
add
strong_cat
name
cat
;
merge
(
make
name
cat
default_typer
false
)
...
...
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