Commit 51879623 authored by Patrick Baudin's avatar Patrick Baudin
Browse files

Merge branch 'fix/test/parsing' into 'master'

Fix test checking wildcard rules of ACSL parser

See merge request frama-c/frama-c!3878
parents 65bbf41d 3b4867a5
...@@ -14,6 +14,7 @@ mk_tests { ...@@ -14,6 +14,7 @@ mk_tests {
@tests/saveload/ptests \ @tests/saveload/ptests \
@tests/spec/ptests \ @tests/spec/ptests \
@tests/syntax/ptests \ @tests/syntax/ptests \
@tests/test/ptests @tests/test/ptests \
@src/kernel_internals/parsing/tests/ptests
''; '';
} }
...@@ -1145,7 +1145,13 @@ contract: ...@@ -1145,7 +1145,13 @@ contract:
// use that to detect potentially missing ';' at end of clause // use that to detect potentially missing ';' at end of clause
clause_kw: clause_kw:
| ADMIT_REQUIRES { "admit requires" } | ADMIT_REQUIRES { "admit requires" }
| ADMIT_INVARIANT { "admit invariant" }
| ADMIT_LEMMA { "admit lemma" }
| ADMIT_LOOP { "admit loop" }
| CHECK_REQUIRES { "check requires" } | CHECK_REQUIRES { "check requires" }
| CHECK_INVARIANT { "check invariant" }
| CHECK_LEMMA { "check lemma" }
| CHECK_LOOP { "check loop" }
| REQUIRES { "requires" } | REQUIRES { "requires" }
| ASSUMES {"assumes"} | ASSUMES {"assumes"}
| ASSIGNS { "assigns" } | ASSIGNS { "assigns" }
...@@ -1495,6 +1501,8 @@ beg_pragma_or_code_annotation: ...@@ -1495,6 +1501,8 @@ beg_pragma_or_code_annotation:
| INVARIANT {} | INVARIANT {}
| CHECK_INVARIANT {} | CHECK_INVARIANT {}
| ADMIT_INVARIANT {} | ADMIT_INVARIANT {}
| CHECK_LOOP {}
| ADMIT_LOOP {}
| EXT_CODE_ANNOT {} | EXT_CODE_ANNOT {}
; ;
...@@ -1871,7 +1879,7 @@ identifier_or_typename: /* allowed as C field names */ ...@@ -1871,7 +1879,7 @@ identifier_or_typename: /* allowed as C field names */
| is_acsl_typename { $1 } | is_acsl_typename { $1 }
| TYPENAME { $1 } /* followed by the same list than 'identifier' */ | TYPENAME { $1 } /* followed by the same list than 'identifier' */
| IDENTIFIER { $1 } | IDENTIFIER { $1 }
/* token list used inside ascl clauses: */ /* token list used inside acsl clauses: */
| BEHAVIORS { "behaviors" } | BEHAVIORS { "behaviors" }
| LABEL { "label" } | LABEL { "label" }
| READS { "reads" } | READS { "reads" }
...@@ -1880,7 +1888,7 @@ identifier_or_typename: /* allowed as C field names */ ...@@ -1880,7 +1888,7 @@ identifier_or_typename: /* allowed as C field names */
identifier: /* part included into 'identifier_or_typename', but duplicated to avoid parsing conflicts */ identifier: /* part included into 'identifier_or_typename', but duplicated to avoid parsing conflicts */
| IDENTIFIER { $1 } | IDENTIFIER { $1 }
/* token list used inside ascl clauses: */ /* token list used inside acsl clauses: */
| BEHAVIORS { "behaviors" } | BEHAVIORS { "behaviors" }
| LABEL { "label" } | LABEL { "label" }
| READS { "reads" } | READS { "reads" }
...@@ -1975,8 +1983,14 @@ is_acsl_decl_or_code_annot: ...@@ -1975,8 +1983,14 @@ is_acsl_decl_or_code_annot:
| IMPACT { "impact" } | IMPACT { "impact" }
| INDUCTIVE { "inductive" } | INDUCTIVE { "inductive" }
| INVARIANT { "invariant" } | INVARIANT { "invariant" }
| ADMIT_INVARIANT { "admit invariant" }
| CHECK_INVARIANT { "check invariant" }
| LEMMA { "lemma" } | LEMMA { "lemma" }
| ADMIT_LEMMA { "admit lemma" }
| CHECK_LEMMA { "check lemma" }
| LOOP { "loop" } | LOOP { "loop" }
| ADMIT_LOOP { "admit loop" }
| CHECK_LOOP { "check loop" }
| PRAGMA { "pragma" } | PRAGMA { "pragma" }
| PREDICATE { "predicate" } | PREDICATE { "predicate" }
| SLICE { "slice" } | SLICE { "slice" }
......
...@@ -28,7 +28,30 @@ let tokens = ref Strings.empty ...@@ -28,7 +28,30 @@ let tokens = ref Strings.empty
let wildcards = 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" let is_token_line s = String.length s >= 6 && String.sub s 0 6 = "%token"
...@@ -52,6 +75,7 @@ let add_tokens s = ...@@ -52,6 +75,7 @@ let add_tokens s =
let wildcard_rules = let wildcard_rules =
[ "bs_keyword"; "wildcard"; "keyword"; "c_keyword"; [ "bs_keyword"; "wildcard"; "keyword"; "c_keyword";
"non_logic_keyword"; "acsl_c_keyword"; "is_ext_spec"; "non_logic_keyword"; "acsl_c_keyword"; "is_ext_spec";
"is_acsl_typename";
"is_acsl_spec"; "is_acsl_decl_or_code_annot"; "is_acsl_spec"; "is_acsl_decl_or_code_annot";
"is_acsl_other"; "post_cond"; "is_acsl_other"; "post_cond";
"identifier_or_typename" "identifier_or_typename"
...@@ -91,23 +115,41 @@ let add_wildcards s = ...@@ -91,23 +115,41 @@ let add_wildcards s =
if s <> "" then if s <> "" then
try try
add_wildcard s add_wildcard s
with Scanf.Scan_failure _ -> () with Scanf.Scan_failure _ | End_of_file -> ()
let () = let () =
try try
let state = ref Throw in let state = Stack.create () in
Stack.push Throw state;
while true do while true do
let s = input_line file in 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 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 if is_wildcard_rule s then begin
state:=Wildcard; Stack.clear state;
add_wildcards s 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 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 end
else (* state is Wildcard *)
if is_other_rule s then state:=Throw
else add_wildcards s
done done
with End_of_file -> () with End_of_file -> ()
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment