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
83f9f710
Commit
83f9f710
authored
2 years ago
by
Virgile Prevosto
Browse files
Options
Downloads
Patches
Plain Diff
[tests] check logic parser takes into account comments in parsing rules
parent
ed4f5130
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_internals/parsing/tests/check_logic_parser.ml
+51
-9
51 additions, 9 deletions
src/kernel_internals/parsing/tests/check_logic_parser.ml
with
51 additions
and
9 deletions
src/kernel_internals/parsing/tests/check_logic_parser.ml
+
51
−
9
View file @
83f9f710
...
...
@@ -28,7 +28,30 @@ let tokens = ref Strings.empty
let
wildcards
=
ref
Strings
.
empty
type
state
=
Throw
|
Wildcard
type
state
=
Throw
|
Wildcard
|
Comment
let
remove_comment
in_comm
s
=
let
b
=
Buffer
.
create
5
in
let
token
(
in_comm
,
prev
)
c
=
if
in_comm
then
begin
match
prev
,
c
with
|
Some
'
*
'
,
'
/
'
->
false
,
None
|
_
->
true
,
Some
c
end
else
begin
match
prev
,
c
with
|
Some
'
/
'
,
'
*
'
->
true
,
None
|
Some
c1
,
c2
->
Buffer
.
add_char
b
c1
;
false
,
Some
c2
|
_
->
false
,
Some
c
end
in
let
(
in_comm
,
last
)
=
Seq
.
fold_left
token
(
in_comm
,
None
)
(
String
.
to_seq
s
)
in
if
not
in_comm
then
begin
match
last
with
|
Some
c
->
Buffer
.
add_char
b
c
|
None
->
()
end
;
in_comm
,
Buffer
.
contents
b
let
is_token_line
s
=
String
.
length
s
>=
6
&&
String
.
sub
s
0
6
=
"%token"
...
...
@@ -52,6 +75,7 @@ let add_tokens s =
let
wildcard_rules
=
[
"bs_keyword"
;
"wildcard"
;
"keyword"
;
"c_keyword"
;
"non_logic_keyword"
;
"acsl_c_keyword"
;
"is_ext_spec"
;
"is_acsl_typename"
;
"is_acsl_spec"
;
"is_acsl_decl_or_code_annot"
;
"is_acsl_other"
;
"post_cond"
;
"identifier_or_typename"
...
...
@@ -91,23 +115,41 @@ let add_wildcards s =
if
s
<>
""
then
try
add_wildcard
s
with
Scanf
.
Scan_failure
_
->
()
with
Scanf
.
Scan_failure
_
|
End_of_file
->
()
let
()
=
try
let
state
=
ref
Throw
in
let
state
=
Stack
.
create
()
in
Stack
.
push
Throw
state
;
while
true
do
let
s
=
input_line
file
in
let
in_comm
,
s
=
remove_comment
(
Stack
.
top
state
=
Comment
)
s
in
(* if we exit from comment, return to previous state and analyze line *)
if
not
in_comm
&&
Stack
.
top
state
=
Comment
then
begin
ignore
(
Stack
.
pop
state
);
end
;
if
is_token_line
s
then
add_tokens
s
else
if
!
state
=
Throw
then
begin
else
if
Stack
.
top
state
=
Throw
then
begin
if
is_wildcard_rule
s
then
begin
state
:=
Wildcard
;
add_wildcards
s
Stack
.
clear
state
;
Stack
.
push
Wildcard
state
;
add_wildcards
s
;
end
end
else
if
Stack
.
top
state
=
Wildcard
then
begin
if
is_other_rule
s
then
begin
Stack
.
clear
state
;
Stack
.
push
Throw
state
;
end
else
begin
add_wildcards
s
;
end
;
end
;
(* if we have started an unfinished comment,
pass in comment mode for the next line. *)
if
in_comm
&&
Stack
.
top
state
<>
Comment
then
begin
Stack
.
push
Comment
state
;
end
else
(* state is Wildcard *)
if
is_other_rule
s
then
state
:=
Throw
else
add_wildcards
s
done
with
End_of_file
->
()
...
...
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