Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
POTTIER Francois
menhir
Commits
9ef1b9d8
Commit
9ef1b9d8
authored
Sep 25, 2015
by
POTTIER Francois
Browse files
Options
Browse Files
Download
Plain Diff
Merge branch 'coverage' into merr
parents
6ad597c0
0050c841
Changes
24
Expand all
Hide whitespace changes
Inline
Side-by-side
Showing
24 changed files
with
9117 additions
and
28 deletions
+9117
-28
bench/good/.gitignore
bench/good/.gitignore
+2
-0
bench/good/Makefile
bench/good/Makefile
+47
-2
bench/good/compcert_simplified.exp
bench/good/compcert_simplified.exp
+3
-0
bench/good/compcert_simplified.mly
bench/good/compcert_simplified.mly
+681
-0
bench/good/compcert_simplified.opp.exp
bench/good/compcert_simplified.opp.exp
+2195
-0
bench/good/coverage.sh
bench/good/coverage.sh
+0
-26
bench/good/framac-cparser.exp
bench/good/framac-cparser.exp
+117
-0
bench/good/framac-cparser.mly
bench/good/framac-cparser.mly
+1775
-0
bench/good/framac-cparser.opp.exp
bench/good/framac-cparser.opp.exp
+1901
-0
bench/good/framac-print_api-grammar.exp
bench/good/framac-print_api-grammar.exp
+0
-0
bench/good/framac-print_api-grammar.mly
bench/good/framac-print_api-grammar.mly
+41
-0
bench/good/framac-print_api-grammar.opp.exp
bench/good/framac-print_api-grammar.opp.exp
+36
-0
bench/good/ltlparser.exp
bench/good/ltlparser.exp
+24
-0
bench/good/ltlparser.mly
bench/good/ltlparser.mly
+185
-0
bench/good/ltlparser.opp.exp
bench/good/ltlparser.opp.exp
+173
-0
bench/good/promelaparser.exp
bench/good/promelaparser.exp
+4
-0
bench/good/promelaparser.mly
bench/good/promelaparser.mly
+233
-0
bench/good/promelaparser.opp.exp
bench/good/promelaparser.opp.exp
+227
-0
bench/good/promelaparser_withexps.exp
bench/good/promelaparser_withexps.exp
+28
-0
bench/good/promelaparser_withexps.mly
bench/good/promelaparser_withexps.mly
+300
-0
bench/good/promelaparser_withexps.opp.exp
bench/good/promelaparser_withexps.opp.exp
+314
-0
bench/good/yaparser.exp
bench/good/yaparser.exp
+53
-0
bench/good/yaparser.mly
bench/good/yaparser.mly
+361
-0
bench/good/yaparser.opp.exp
bench/good/yaparser.opp.exp
+417
-0
No files found.
bench/good/.gitignore
View file @
9ef1b9d8
...
...
@@ -6,3 +6,5 @@
*.conflicts
failures
warnings
*.log
lr.csv
bench/good/Makefile
View file @
9ef1b9d8
.PHONY
:
clean test expected
.PHONY
:
clean test expected
list
# Note that there is potential confusion between src/_stage1/menhir
# and src/_stage2/menhir. Here, we use the latter (built by "make
...
...
@@ -97,8 +97,53 @@ expected:
@
CREATE_EXPECTED
=
1
$(MAKE)
-s
test
@
echo
"Expected output re-generated."
clean
:
clean
:
:
rm
-f
*
~
rm
-f
*
.ml
*
.mli
*
.conflicts
*
.automaton
rm
-f
*
.out failures warnings
# ------------------------------------------------------------------------------
# Testing LRijkstra, that is, menhir --list-errors.
ifeq
($(shell hostname),teraram)
TIMEOUT
:=
1200
PARALLEL
:=
-j30
else
TIMEOUT
:=
2
PARALLEL
:=
-j4
endif
SINGLE
=
$(
shell
ls
*
.mly | egrep
-v
'.*-([1-9]
)
.mly'
)
%.log
:
%.mly
@
echo
"Now dealing with:
$<
"
|
tee
-a
$@
@
if
(
timeout
$(TIMEOUT)
$(MENHIR)
--list-errors
-la
2
--lalr
$<
)
>>
$@
2>&1
;
then
\
echo
"
$<
: success."
|
tee
-a
$@
;
\
else
\
echo
"
$<
: TIMEOUT (or failure)."
|
tee
-a
$@
;
\
fi
list
:
# Compile Menhir.
# make -C $(SRC) clean
make
-C
$(SRC)
bootstrap
# Remove any leftover output files.
rm
-f
*.log
lr.csv
# Print the header of lr.csv. (This should be kept in sync with LRijkstra.ml.)
echo
"grammar,terminals,nonterminals,size,states,trie,facts,edges,time,heap"
>
lr.csv
# Try every grammar. (Only the single-file grammars, that is.)
# This can proceed in parallel, for a reasonable number of processes.
# Each process appends one line of data to lr.csv when it finishes.
# Hopefully the final content of lr.csv will be a reasonable interleaving
# of these lines.
@
time
$(MAKE)
$(PARALLEL)
$(patsubst
%.mly,%.log,$(SINGLE))
# Finished.
@ echo "Number of grammars that could not be handled in $(TIMEOUT) seconds
:
"
@
grep
TIMEOUT
*
.log |
wc
-l
@
echo
"Number of grammars that were successfully handled:"
@
tail
-n
+2 lr.csv |
wc
-l
clean
::
rm
-f
*
.log
# rm -f lr.csv
bench/good/compcert_simplified.exp
0 → 100644
View file @
9ef1b9d8
Note: the nonterminal symbol option (from compcert_simplified.mly) is renamed compcert_simplified_option.
Warning: you are using the standard library and/or the %inline keyword. We
recommend switching on --infer in order to avoid obscure type error messages.
bench/good/compcert_simplified.mly
0 → 100644
View file @
9ef1b9d8
/*
*********************************************************************/
/*
*/
/*
The
Compcert
verified
compiler
*/
/*
*/
/*
Jacques
-
Henri
Jourdan
,
INRIA
Paris
-
Rocquencourt
*/
/*
*/
/*
Copyright
Institut
National
de
Recherche
en
Informatique
et
en
*/
/*
Automatique
.
All
rights
reserved
.
This
file
is
distributed
*/
/*
under
the
terms
of
the
GNU
General
Public
License
as
published
by
*/
/*
the
Free
Software
Foundation
,
either
version
2
of
the
License
,
or
*/
/*
(
at
your
option
)
any
later
version
.
This
file
is
also
distributed
*/
/*
under
the
terms
of
the
INRIA
Non
-
Commercial
License
Agreement
.
*/
/*
*/
/*
*********************************************************************/
%
{
open
Pre_parser_aux
let
set_id_type
(
_
,
r
,_
)
t
=
r
:=
t
let
declare_varname
(
i
,_,_
)
=
!
declare_varname
i
let
declare_typename
(
i
,_,_
)
=
!
declare_typename
i
%
}
%
token
<
string
*
Pre_parser_aux
.
identifier_type
ref
*
Cabs
.
cabsloc
>
VAR_NAME
TYPEDEF_NAME
%
token
<
Cabs
.
constant
*
Cabs
.
cabsloc
>
CONSTANT
%
token
<
bool
*
int64
list
*
Cabs
.
cabsloc
>
STRING_LITERAL
%
token
<
string
*
Cabs
.
cabsloc
>
PRAGMA
%
token
<
Cabs
.
cabsloc
>
SIZEOF
PTR
INC
DEC
LEFT
RIGHT
LEQ
GEQ
EQEQ
EQ
NEQ
LT
GT
ANDAND
BARBAR
PLUS
MINUS
STAR
TILDE
BANG
SLASH
PERCENT
HAT
BAR
QUESTION
COLON
AND
MUL_ASSIGN
DIV_ASSIGN
MOD_ASSIGN
ADD_ASSIGN
SUB_ASSIGN
LEFT_ASSIGN
RIGHT_ASSIGN
AND_ASSIGN
XOR_ASSIGN
OR_ASSIGN
LPAREN
RPAREN
LBRACK
RBRACK
LBRACE
RBRACE
DOT
COMMA
SEMICOLON
ELLIPSIS
TYPEDEF
EXTERN
STATIC
RESTRICT
AUTO
REGISTER
INLINE
CHAR
SHORT
INT
LONG
SIGNED
UNSIGNED
FLOAT
DOUBLE
UNDERSCORE_BOOL
CONST
VOLATILE
VOID
STRUCT
UNION
ENUM
CASE
DEFAULT
IF
ELSE
SWITCH
WHILE
DO
FOR
GOTO
CONTINUE
BREAK
RETURN
BUILTIN_VA_ARG
ALIGNOF
ATTRIBUTE
ALIGNAS
PACKED
ASM
%
token
EOF
(* These precedences declarations solve the conflict in the following declaration :
int f(int (a));
when a is a TYPEDEF_NAME. It is specified by 6.7.5.3 11.
*)
%
nonassoc
TYPEDEF_NAME
%
nonassoc
highPrec
%
start
<
unit
>
translation_unit_file
%%
(* Helpers *)
%
inline
option
(
X
)
:
|
/*
nothing
*/
{
None
}
|
x
=
X
{
Some
x
}
%
inline
fst
(
X
)
:
|
x
=
X
{
fst
x
}
general_identifier
:
|
i
=
VAR_NAME
|
i
=
TYPEDEF_NAME
{
i
}
string_literals_list
:
|
STRING_LITERAL
|
string_literals_list
STRING_LITERAL
{}
(* WARNING : because of the lookahead token, the context might
be pushed or popped one token after the position of this
non-terminal !
Pushing too late is not dangerous for us, because this does not
change the token stream. However, we have to make sure the
lookahead token present just after popping is not an identifier.
*)
push_context
:
(* empty *)
%
prec
highPrec
{
!
push_context
()
}
pop_context
:
(* empty *)
{
!
pop_context
()
}
in_context
(
nt
)
:
push_context
x
=
nt
pop_context
{
x
}
declare_varname
(
nt
)
:
i
=
nt
{
declare_varname
i
;
i
}
declare_typename
(
nt
)
:
i
=
nt
{
declare_typename
i
;
i
}
(* Actual grammar *)
primary_expression
:
|
i
=
VAR_NAME
{
set_id_type
i
VarId
}
|
CONSTANT
|
string_literals_list
|
LPAREN
expression
RPAREN
{}
postfix_expression
:
|
primary_expression
|
postfix_expression
LBRACK
expression
RBRACK
|
postfix_expression
LPAREN
argument_expression_list
?
RPAREN
{}
|
BUILTIN_VA_ARG
LPAREN
assignment_expression
COMMA
type_name
RPAREN
{}
|
postfix_expression
DOT
i
=
general_identifier
|
postfix_expression
PTR
i
=
general_identifier
{
set_id_type
i
OtherId
}
|
postfix_expression
INC
|
postfix_expression
DEC
|
LPAREN
type_name
RPAREN
LBRACE
initializer_list
COMMA
?
RBRACE
{}
argument_expression_list
:
|
assignment_expression
|
argument_expression_list
COMMA
assignment_expression
{}
unary_expression
:
|
postfix_expression
|
INC
unary_expression
|
DEC
unary_expression
|
unary_operator
cast_expression
|
SIZEOF
unary_expression
|
SIZEOF
LPAREN
type_name
RPAREN
|
ALIGNOF
unary_expression
|
ALIGNOF
LPAREN
type_name
RPAREN
{}
unary_operator
:
|
AND
|
STAR
|
PLUS
|
MINUS
|
TILDE
|
BANG
{}
cast_expression
:
|
unary_expression
|
LPAREN
type_name
RPAREN
cast_expression
{}
multiplicative_expression
:
|
cast_expression
|
multiplicative_expression
STAR
cast_expression
|
multiplicative_expression
SLASH
cast_expression
|
multiplicative_expression
PERCENT
cast_expression
{}
additive_expression
:
|
multiplicative_expression
|
additive_expression
PLUS
multiplicative_expression
|
additive_expression
MINUS
multiplicative_expression
{}
shift_expression
:
|
additive_expression
|
shift_expression
LEFT
additive_expression
|
shift_expression
RIGHT
additive_expression
{}
relational_expression
:
|
shift_expression
|
relational_expression
LT
shift_expression
|
relational_expression
GT
shift_expression
|
relational_expression
LEQ
shift_expression
|
relational_expression
GEQ
shift_expression
{}
equality_expression
:
|
relational_expression
|
equality_expression
EQEQ
relational_expression
|
equality_expression
NEQ
relational_expression
{}
and_expression
:
|
equality_expression
|
and_expression
AND
equality_expression
{}
exclusive_or_expression
:
|
and_expression
|
exclusive_or_expression
HAT
and_expression
{}
inclusive_or_expression
:
|
exclusive_or_expression
|
inclusive_or_expression
BAR
exclusive_or_expression
{}
logical_and_expression
:
|
inclusive_or_expression
|
logical_and_expression
ANDAND
inclusive_or_expression
{}
logical_or_expression
:
|
logical_and_expression
|
logical_or_expression
BARBAR
logical_and_expression
{}
conditional_expression
:
|
logical_or_expression
|
logical_or_expression
QUESTION
expression
COLON
conditional_expression
{}
assignment_expression
:
|
conditional_expression
|
unary_expression
assignment_operator
assignment_expression
{}
assignment_operator
:
|
EQ
|
MUL_ASSIGN
|
DIV_ASSIGN
|
MOD_ASSIGN
|
ADD_ASSIGN
|
SUB_ASSIGN
|
LEFT_ASSIGN
|
RIGHT_ASSIGN
|
AND_ASSIGN
|
XOR_ASSIGN
|
OR_ASSIGN
{}
expression
:
|
assignment_expression
|
expression
COMMA
assignment_expression
{}
constant_expression
:
|
conditional_expression
{}
declaration
:
|
declaration_specifiers
init_declarator_list
?
SEMICOLON
{}
|
declaration_specifiers_typedef
typedef_declarator_list
?
SEMICOLON
{}
declaration_specifiers_no_type
:
|
storage_class_specifier_no_typedef
declaration_specifiers_no_type
?
|
type_qualifier
declaration_specifiers_no_type
?
|
function_specifier
declaration_specifiers_no_type
?
{}
declaration_specifiers_no_typedef_name
:
|
storage_class_specifier_no_typedef
declaration_specifiers_no_typedef_name
?
|
type_qualifier
declaration_specifiers_no_typedef_name
?
|
function_specifier
declaration_specifiers_no_typedef_name
?
|
type_specifier_no_typedef_name
declaration_specifiers_no_typedef_name
?
{}
declaration_specifiers
:
|
declaration_specifiers_no_type
?
i
=
TYPEDEF_NAME
declaration_specifiers_no_type
?
{
set_id_type
i
TypedefId
}
|
declaration_specifiers_no_type
?
type_specifier_no_typedef_name
declaration_specifiers_no_typedef_name
?
{}
declaration_specifiers_typedef
:
|
declaration_specifiers_no_type
?
TYPEDEF
declaration_specifiers_no_type
?
i
=
TYPEDEF_NAME
declaration_specifiers_no_type
?
|
declaration_specifiers_no_type
?
i
=
TYPEDEF_NAME
declaration_specifiers_no_type
?
TYPEDEF
declaration_specifiers_no_type
?
{
set_id_type
i
TypedefId
}
|
declaration_specifiers_no_type
?
TYPEDEF
declaration_specifiers_no_type
?
type_specifier_no_typedef_name
declaration_specifiers_no_typedef_name
?
|
declaration_specifiers_no_type
?
type_specifier_no_typedef_name
declaration_specifiers_no_typedef_name
?
TYPEDEF
declaration_specifiers_no_typedef_name
?
{}
init_declarator_list
:
|
init_declarator
|
init_declarator_list
COMMA
init_declarator
{}
init_declarator
:
|
declare_varname
(
fst
(
declarator
))
|
declare_varname
(
fst
(
declarator
))
EQ
c_initializer
{
}
typedef_declarator_list
:
|
typedef_declarator
|
typedef_declarator_list
COMMA
typedef_declarator
{}
typedef_declarator
:
|
declare_typename
(
fst
(
declarator
))
{
}
storage_class_specifier_no_typedef
:
|
EXTERN
|
STATIC
|
AUTO
|
REGISTER
{}
type_specifier_no_typedef_name
:
|
VOID
|
CHAR
|
SHORT
|
INT
|
LONG
|
FLOAT
|
DOUBLE
|
SIGNED
|
UNSIGNED
|
UNDERSCORE_BOOL
|
struct_or_union_specifier
|
enum_specifier
{}
struct_or_union_specifier
:
|
struct_or_union
attribute_specifier_list
LBRACE
struct_declaration_list
RBRACE
{}
|
struct_or_union
attribute_specifier_list
i
=
general_identifier
LBRACE
struct_declaration_list
RBRACE
|
struct_or_union
attribute_specifier_list
i
=
general_identifier
{
set_id_type
i
OtherId
}
struct_or_union
:
|
STRUCT
|
UNION
{}
struct_declaration_list
:
|
(* empty *)
|
struct_declaration_list
struct_declaration
{}
struct_declaration
:
|
specifier_qualifier_list
struct_declarator_list
?
SEMICOLON
{}
specifier_qualifier_list
:
|
type_qualifier_list
?
i
=
TYPEDEF_NAME
type_qualifier_list
?
{
set_id_type
i
TypedefId
}
|
type_qualifier_list
?
type_specifier_no_typedef_name
specifier_qualifier_list_no_typedef_name
?
{}
specifier_qualifier_list_no_typedef_name
:
|
type_specifier_no_typedef_name
specifier_qualifier_list_no_typedef_name
?
|
type_qualifier
specifier_qualifier_list_no_typedef_name
?
{}
struct_declarator_list
:
|
struct_declarator
|
struct_declarator_list
COMMA
struct_declarator
{}
struct_declarator
:
|
declarator
|
declarator
?
COLON
constant_expression
{}
enum_specifier
:
|
ENUM
attribute_specifier_list
LBRACE
enumerator_list
COMMA
?
RBRACE
{}
|
ENUM
attribute_specifier_list
i
=
general_identifier
LBRACE
enumerator_list
COMMA
?
RBRACE
|
ENUM
attribute_specifier_list
i
=
general_identifier
{
set_id_type
i
OtherId
}
enumerator_list
:
|
declare_varname
(
enumerator
)
|
enumerator_list
COMMA
declare_varname
(
enumerator
)
{}
enumerator
:
|
i
=
enumeration_constant
|
i
=
enumeration_constant
EQ
constant_expression
{
i
}
enumeration_constant
:
|
i
=
general_identifier
{
set_id_type
i
VarId
;
i
}
type_qualifier
:
|
CONST
|
RESTRICT
|
VOLATILE
|
attribute_specifier
{}
attribute_specifier_list
:
|
/*
empty
*/
|
attribute_specifier_list
attribute_specifier
{}
attribute_specifier
:
|
ATTRIBUTE
LPAREN
LPAREN
gcc_attribute_list
RPAREN
RPAREN
|
PACKED
LPAREN
argument_expression_list
RPAREN
(* TODO: slove conflict *)
(* | PACKED *)
|
ALIGNAS
LPAREN
argument_expression_list
RPAREN
|
ALIGNAS
LPAREN
type_name
RPAREN
{}
gcc_attribute_list
:
|
gcc_attribute
|
gcc_attribute_list
COMMA
gcc_attribute
{}
gcc_attribute
:
|
/*
empty
*/
|
gcc_attribute_word
|
gcc_attribute_word
LPAREN
argument_expression_list
?
RPAREN
{}
|
gcc_attribute_word
LPAREN
i
=
TYPEDEF_NAME
COMMA
argument_expression_list
RPAREN
(* This is to emulate GCC's attribute syntax : we make this identifier
a var name identifier, so that the parser will see it as a variable
reference *)
{
set_id_type
i
VarId
}
gcc_attribute_word
:
|
i
=
general_identifier
{
set_id_type
i
OtherId
}
|
CONST
|
PACKED
{}
function_specifier
:
|
INLINE
{}
declarator
:
|
pointer
?
x
=
direct_declarator
attribute_specifier_list
{
x
}
direct_declarator
:
|
i
=
general_identifier
{
set_id_type
i
VarId
;
(
i
,
None
)
}
|
LPAREN
x
=
declarator
RPAREN
|
x
=
direct_declarator
LBRACK
type_qualifier_list
?
assignment_expression
?
RBRACK
{
x
}
|
x
=
direct_declarator
LPAREN
l
=
in_context
(
parameter_type_list
?
)
RPAREN
{
match
snd
x
with
|
None
->
(
fst
x
,
Some
(
match
l
with
None
->
[]
|
Some
l
->
l
))
|
Some
_
->
x
}
pointer
:
|
STAR
type_qualifier_list
?
|
STAR
type_qualifier_list
?
pointer
{}
type_qualifier_list
:
|
type_qualifier_list
?
type_qualifier
{}
parameter_type_list
:
|
l
=
parameter_list
|
l
=
parameter_list
COMMA
ELLIPSIS
{
l
}
parameter_list
:
|
i
=
parameter_declaration
{
[
i
]
}
|
l
=
parameter_list
COMMA
i
=
parameter_declaration
{
i
::
l
}
parameter_declaration
:
|
declaration_specifiers
id
=
declare_varname
(
fst
(
declarator
))
{
Some
id
}
|
declaration_specifiers
abstract_declarator
?
{
None
}
type_name
:
|
specifier_qualifier_list
abstract_declarator
?
{}
abstract_declarator
:
|
pointer
|
pointer
?
direct_abstract_declarator
{}
direct_abstract_declarator
:
|
LPAREN
abstract_declarator
RPAREN
|
direct_abstract_declarator
?
LBRACK
type_qualifier_list
?
assignment_expression
?
RBRACK
|
direct_abstract_declarator
?
LPAREN
in_context
(
parameter_type_list
?
)
RPAREN
{}
c_initializer
:
|
assignment_expression
|
LBRACE
initializer_list
COMMA
?
RBRACE
{}
initializer_list
:
|
designation
?
c_initializer
|
initializer_list
COMMA
designation
?
c_initializer
{}
designation
:
|
designator_list
EQ
{}
designator_list
:
|
designator_list
?
designator
{}
designator
:
|
LBRACK
constant_expression
RBRACK
{}
|
DOT
i
=
general_identifier
{
set_id_type
i
OtherId
}
statement_finish
:
|
labeled_statement
(
statement_finish
)
|
compound_statement
|
expression_statement
|
selection_statement_finish
|
iteration_statement
(
statement_finish
)
|
jump_statement
|
asm_statement
{}
statement_intern
:
|
labeled_statement
(
statement_intern
)
|
compound_statement
|
expression_statement
|
selection_statement_intern
|
iteration_statement
(
statement_intern
)
|
jump_statement
|
asm_statement
{}
labeled_statement
(
last_statement
)
:
|
i
=
general_identifier
COLON
last_statement
{
set_id_type
i
OtherId
}
|
CASE
constant_expression
COLON
last_statement
|
DEFAULT
COLON
last_statement
{}
compound_statement
:
|
LBRACE
in_context
(
block_item_list
?
)
RBRACE
{}