Skip to content

M
menhir
Commit bf483577 authored by POTTIER Francois's avatar POTTIER Francois
Browse files
Options

More sample grammars, from Frama-C.

parent 711e4589
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 6189 additions and 0 deletions
bench/good/framac-cparser.exp 0 → 100644
View file @ bf483577
File "framac-cparser.mly", line 389, characters 54-60:
Warning: the token ADDROF is unused.
File "framac-cparser.mly", line 357, characters 36-50:
Warning: the token ATTRIBUTE_USED is unused.
File "framac-cparser.mly", line 358, characters 7-22:
Warning: the token BUILTIN_VA_LIST is unused.
File "framac-cparser.mly", line 389, characters 42-46:
Warning: the token CAST is unused.
File "framac-cparser.mly", line 319, characters 59-64:
Warning: the token INT32 is unused.
File "framac-cparser.mly", line 389, characters 0-6:
Warning: the precedence level assigned to ADDROF is never useful.
File "framac-cparser.mly", line 389, characters 0-6:
Warning: the precedence level assigned to ALIGNOF is never useful.
File "framac-cparser.mly", line 383, characters 0-5:
Warning: the precedence level assigned to AND is never useful.
File "framac-cparser.mly", line 380, characters 0-5:
Warning: the precedence level assigned to AND_AND is never useful.
File "framac-cparser.mly", line 376, characters 0-6:
Warning: the precedence level assigned to AND_EQ is never useful.
File "framac-cparser.mly", line 391, characters 0-5:
Warning: the precedence level assigned to ARROW is never useful.
File "framac-cparser.mly", line 389, characters 0-6:
Warning: the precedence level assigned to CAST is never useful.
File "framac-cparser.mly", line 382, characters 0-5:
Warning: the precedence level assigned to CIRC is never useful.
File "framac-cparser.mly", line 376, characters 0-6:
Warning: the precedence level assigned to CIRC_EQ is never useful.
File "framac-cparser.mly", line 375, characters 0-5:
Warning: the precedence level assigned to COMMA is never useful.
File "framac-cparser.mly", line 388, characters 0-5:
Warning: the precedence level assigned to CONST is never useful.
File "framac-cparser.mly", line 391, characters 0-5:
Warning: the precedence level assigned to DOT is never useful.
File "framac-cparser.mly", line 376, characters 0-6:
Warning: the precedence level assigned to EQ is never useful.
File "framac-cparser.mly", line 384, characters 0-5:
Warning: the precedence level assigned to EQ_EQ is never useful.
File "framac-cparser.mly", line 389, characters 0-6:
Warning: the precedence level assigned to EXCLAM is never useful.
File "framac-cparser.mly", line 384, characters 0-5:
Warning: the precedence level assigned to EXCLAM_EQ is never useful.
File "framac-cparser.mly", line 385, characters 0-5:
Warning: the precedence level assigned to INF is never useful.
File "framac-cparser.mly", line 385, characters 0-5:
Warning: the precedence level assigned to INF_EQ is never useful.
File "framac-cparser.mly", line 386, characters 0-5:
Warning: the precedence level assigned to INF_INF is never useful.
File "framac-cparser.mly", line 376, characters 0-6:
Warning: the precedence level assigned to INF_INF_EQ is never useful.
File "framac-cparser.mly", line 391, characters 0-5:
Warning: the precedence level assigned to LBRACE is never useful.
File "framac-cparser.mly", line 390, characters 0-5:
Warning: the precedence level assigned to LBRACKET is never useful.
File "framac-cparser.mly", line 387, characters 0-5:
Warning: the precedence level assigned to MINUS is never useful.
File "framac-cparser.mly", line 376, characters 0-6:
Warning: the precedence level assigned to MINUS_EQ is never useful.
File "framac-cparser.mly", line 389, characters 0-6:
Warning: the precedence level assigned to MINUS_MINUS is never useful.
File "framac-cparser.mly", line 388, characters 0-5:
Warning: the precedence level assigned to PERCENT is never useful.
File "framac-cparser.mly", line 376, characters 0-6:
Warning: the precedence level assigned to PERCENT_EQ is never useful.
File "framac-cparser.mly", line 381, characters 0-5:
Warning: the precedence level assigned to PIPE is never useful.
File "framac-cparser.mly", line 376, characters 0-6:
Warning: the precedence level assigned to PIPE_EQ is never useful.
File "framac-cparser.mly", line 379, characters 0-5:
Warning: the precedence level assigned to PIPE_PIPE is never useful.
File "framac-cparser.mly", line 387, characters 0-5:
Warning: the precedence level assigned to PLUS is never useful.
File "framac-cparser.mly", line 376, characters 0-6:
Warning: the precedence level assigned to PLUS_EQ is never useful.
File "framac-cparser.mly", line 389, characters 0-6:
Warning: the precedence level assigned to PLUS_PLUS is never useful.
File "framac-cparser.mly", line 378, characters 0-6:
Warning: the precedence level assigned to QUEST is never useful.
File "framac-cparser.mly", line 388, characters 0-5:
Warning: the precedence level assigned to RESTRICT is never useful.
File "framac-cparser.mly", line 389, characters 0-6:
Warning: the precedence level assigned to SIZEOF is never useful.
File "framac-cparser.mly", line 388, characters 0-5:
Warning: the precedence level assigned to SLASH is never useful.
File "framac-cparser.mly", line 376, characters 0-6:
Warning: the precedence level assigned to SLASH_EQ is never useful.
File "framac-cparser.mly", line 388, characters 0-5:
Warning: the precedence level assigned to STAR is never useful.
File "framac-cparser.mly", line 376, characters 0-6:
Warning: the precedence level assigned to STAR_EQ is never useful.
File "framac-cparser.mly", line 385, characters 0-5:
Warning: the precedence level assigned to SUP is never useful.
File "framac-cparser.mly", line 385, characters 0-5:
Warning: the precedence level assigned to SUP_EQ is never useful.
File "framac-cparser.mly", line 386, characters 0-5:
Warning: the precedence level assigned to SUP_SUP is never useful.
File "framac-cparser.mly", line 376, characters 0-6:
Warning: the precedence level assigned to SUP_SUP_EQ is never useful.
File "framac-cparser.mly", line 389, characters 0-6:
Warning: the precedence level assigned to TILDE is never useful.
File "framac-cparser.mly", line 388, characters 0-5:
Warning: the precedence level assigned to VOLATILE is never useful.
File "framac-cparser.mly", line 464, characters 56-61:
Warning: this %prec declaration is never useful.
Warning: one state has shift/reduce conflicts.
Warning: one shift/reduce conflict was arbitrarily resolved.
File "framac-cparser.mly", line 1304, characters 2-28:
Warning: production direct_old_proto_decl -> direct_decl LPAREN RPAREN is never reduced.
File "framac-cparser.mly", line 1443, characters 2-26:
Warning: production function_def_start -> IDENT LPAREN RPAREN is never reduced.
File "framac-cparser.mly", line 509, characters 2-37:
Warning: production global -> IDENT LPAREN RPAREN SEMICOLON is never reduced.
File "framac-cparser.mly", line 1548, characters 4-24:
Warning: production var_attr -> IDENT COLON CST_INT is never reduced.
File "framac-cparser.mly", line 1549, characters 4-29:
Warning: production var_attr -> NAMED_TYPE COLON CST_INT is never reduced.
Warning: in total, 5 productions are never reduced.
bench/good/framac-cparser.mly 0 → 100644
View file @ bf483577
This diff is collapsed.
bench/good/framac-cparser.opp.exp 0 → 100644
View file @ bf483577
This diff is collapsed.
bench/good/framac-print_api-grammar.mly 0 → 100644
View file @ bf483577
/**************************************************************************/
/* */
/* This file is part of Frama-C. */
/* */
/* Copyright (C) 2007-2015 */
/* CEA (Commissariat à l'énergie atomique et aux énergies */
/* alternatives) */
/* */
/* you can redistribute it and/or modify it under the terms of the GNU */
/* Lesser General Public License as published by the Free Software */
/* Foundation, version 2.1. */
/* */
/* It is distributed in the hope that it will be useful, */
/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
/* GNU Lesser General Public License for more details. */
/* */
/* See the GNU Lesser General Public License version 2.1 */
/* for more details (enclosed in the file licenses/LGPLv2.1). */
/* */
/**************************************************************************/
%{
%}
%token <string> WORD
%token LPAR
%token RPAR
%token COMMA
%token EOF
%start main
%type <string> main
%%
main:
type_string EOF { $1 }
word: WORD { $1 }
type_string: word { $1 }
| type_string word { "'a "^$2 }
| LPAR type_string COMMA type_string RPAR word { "('a,'b) "^$6 }
| LPAR type_string COMMA type_string COMMA type_string RPAR word { "('a,'b,'c) "^$8 }
| LPAR type_string COMMA type_string COMMA type_string COMMA type_string RPAR word { "('a,'b,'c,'d) "^$10 }
bench/good/framac-print_api-grammar.opp.exp 0 → 100644
View file @ bf483577
%{
%}
%start main
%token <string> WORD
%token RPAR
%token LPAR
%token EOF
%token COMMA
%type <string> main
%%
main:
| _1 = type_string _2 = EOF
{ ( _1 )}
word:
| _1 = WORD
{ ( _1 )}
type_string:
| _1 = word
{ ( _1 )}
| _1 = type_string _2 = word
{ ( "'a "^_2 )}
| _1 = LPAR _2 = type_string _3 = COMMA _4 = type_string _5 = RPAR _6 = word
{ ( "('a,'b) "^_6 )}
| _1 = LPAR _2 = type_string _3 = COMMA _4 = type_string _5 = COMMA _6 = type_string _7 = RPAR _8 = word
{ ( "('a,'b,'c) "^_8 )}
| _1 = LPAR _2 = type_string _3 = COMMA _4 = type_string _5 = COMMA _6 = type_string _7 = COMMA _8 = type_string _9 = RPAR _10 = word
{ ( "('a,'b,'c,'d) "^_10 )}
%%
bench/good/ltlparser.exp 0 → 100644
View file @ bf483577
File "ltlparser.mly", line 64, characters 0-6:
Warning: the precedence level assigned to LTL_DIV is never useful.
File "ltlparser.mly", line 58, characters 0-6:
Warning: the precedence level assigned to LTL_EQ is never useful.
File "ltlparser.mly", line 58, characters 0-6:
Warning: the precedence level assigned to LTL_GE is never useful.
File "ltlparser.mly", line 58, characters 0-6:
Warning: the precedence level assigned to LTL_GT is never useful.
File "ltlparser.mly", line 58, characters 0-6:
Warning: the precedence level assigned to LTL_LE is never useful.
File "ltlparser.mly", line 58, characters 0-6:
Warning: the precedence level assigned to LTL_LT is never useful.
File "ltlparser.mly", line 64, characters 0-6:
Warning: the precedence level assigned to LTL_MINUS is never useful.
File "ltlparser.mly", line 64, characters 0-6:
Warning: the precedence level assigned to LTL_MODULO is never useful.
File "ltlparser.mly", line 58, characters 0-6:
Warning: the precedence level assigned to LTL_NEQ is never useful.
File "ltlparser.mly", line 64, characters 0-6:
Warning: the precedence level assigned to LTL_PLUS is never useful.
File "ltlparser.mly", line 64, characters 0-6:
Warning: the precedence level assigned to LTL_STAR is never useful.
Warning: 5 states have shift/reduce conflicts.
Warning: 7 shift/reduce conflicts were arbitrarily resolved.
bench/good/ltlparser.mly 0 → 100644
View file @ bf483577
/**************************************************************************/
/* */
/* This file is part of Aorai plug-in of Frama-C. */
/* */
/* Copyright (C) 2007-2015 */
/* CEA (Commissariat à l'énergie atomique et aux énergies */
/* alternatives) */
/* INRIA (Institut National de Recherche en Informatique et en */
/* Automatique) */
/* INSA (Institut National des Sciences Appliquees) */
/* */
/* you can redistribute it and/or modify it under the terms of the GNU */
/* Lesser General Public License as published by the Free Software */
/* Foundation, version 2.1. */
/* */
/* It is distributed in the hope that it will be useful, */
/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
/* GNU Lesser General Public License for more details. */
/* */
/* See the GNU Lesser General Public License version 2.1 */
/* for more details (enclosed in the file licenses/LGPLv2.1). */
/* */
/**************************************************************************/
/* $Id: ltlparser.mly,v 1.3 2009-02-13 07:59:29 uid562 Exp $ */
/* Originated from http://www.ltl2dstar.de/down/ltl2dstar-0.4.2.zip */
%{
open Promelaast
open Logic_ptree
let observed_expressions=Hashtbl.create 97
let ident_count=ref 0
let get_fresh_ident () =
ident_count:=!ident_count+1;
("buchfreshident"^(string_of_int !ident_count))
%}
%token LTL_TRUE LTL_FALSE LTL_LPAREN LTL_RPAREN
/* Logic operators */
%token LTL_OR LTL_IMPLIES LTL_LEFT_RIGHT_ARROW
%token LTL_AND
%token LTL_NOT
%token LTL_GLOBALLY LTL_FATALLY LTL_UNTIL LTL_RELEASE LTL_NEXT
%right LTL_OR LTL_IMPLIES LTL_LEFT_RIGHT_ARROW
%right LTL_AND
%nonassoc LTL_NOT
%right LTL_GLOBALLY LTL_FATALLY LTL_UNTIL LTL_RELEASE LTL_NEXT
/* Logic relations */
%token LTL_EQ LTL_LT LTL_GT LTL_LE LTL_GE LTL_NEQ
%right LTL_EQ LTL_LT LTL_GT LTL_LE LTL_GE LTL_NEQ
/* Arithmetic relations */
%token LTL_PLUS LTL_MINUS
%token LTL_DIV LTL_STAR LTL_MODULO
%right LTL_PLUS LTL_MINUS LTL_DIV LTL_STAR LTL_MODULO
/* Access */
%token LTL_RIGHT_ARROW LTL_DOT LTL_LEFT_SQUARE LTL_RIGHT_SQUARE LTL_ADRESSE
%token LTL_CALL LTL_RETURN LTL_CALL_OR_RETURN
/* Variables and constants */
%token <string> LTL_INT
%token <string> LTL_LABEL
/* Others */
%token EOF
%type <(Ltlast.formula * (string, (Logic_ptree.relation * Promelaast.expression * Promelaast.expression)) Hashtbl.t)> ltl
%start ltl
%%
ltl
: formula EOF {($1,observed_expressions)}
;
formula
: LTL_TRUE
{Ltlast.LTrue}
| LTL_FALSE
{Ltlast.LFalse}
| LTL_LPAREN formula LTL_RPAREN
{ $2 }
| LTL_GLOBALLY formula
{ Ltlast.LGlobally($2) }
| LTL_FATALLY formula
{ Ltlast.LFatally($2) }
| formula LTL_UNTIL formula
{ Ltlast.LUntil($1,$3) }
| formula LTL_RELEASE formula
{ Ltlast.LRelease($1,$3) }
| LTL_NEXT formula
{ Ltlast.LNext($2) }
| formula LTL_OR formula
{ Ltlast.LOr($1,$3) }
| formula LTL_AND formula
{ Ltlast.LAnd($1,$3) }
| LTL_NOT formula
{ Ltlast.LNot($2) }
| formula LTL_IMPLIES formula
{ Ltlast.LImplies($1,$3) }
| formula LTL_LEFT_RIGHT_ARROW formula
{ Ltlast.LIff($1,$3) }
| LTL_CALL LTL_LPAREN LTL_LABEL LTL_RPAREN
{ Ltlast.LCall($3)}
| LTL_RETURN LTL_LPAREN LTL_LABEL LTL_RPAREN
{ Ltlast.LReturn($3)}
| LTL_CALL_OR_RETURN LTL_LPAREN LTL_LABEL LTL_RPAREN
{ Ltlast.LCallOrReturn($3)}
/* returns a string identifer associated, through observed_expressions table, to the represented expression */
| logic_relation
{
let id = get_fresh_ident () in
Hashtbl.add observed_expressions id $1;
Ltlast.LIdent(id)
}
;
logic_relation
: arith_relation LTL_EQ arith_relation { Eq, $1 , $3}
| arith_relation LTL_LT arith_relation { Lt, $1, $3 }
| arith_relation LTL_GT arith_relation { Gt, $1, $3 }
| arith_relation LTL_LE arith_relation { Le, $1, $3 }
| arith_relation LTL_GE arith_relation { Ge, $1, $3 }
| arith_relation LTL_NEQ arith_relation { Neq, $1, $3 }
| arith_relation { Neq, $1, PCst (IntConstant "0") }
;
arith_relation
: arith_relation_mul LTL_PLUS arith_relation { PBinop(Badd,$1,$3) }
| arith_relation_mul LTL_MINUS arith_relation { PBinop(Bsub,$1,$3) }
| arith_relation_mul { $1 }
;
arith_relation_mul
: arith_relation_mul LTL_DIV access_or_const { PBinop(Bdiv,$1,$3) }
| arith_relation_mul LTL_STAR access_or_const { PBinop(Bmul,$1,$3) }
| arith_relation_mul LTL_MODULO access_or_const { PBinop(Bmod,$1,$3)}
| access_or_const { $1 }
;
/* returns a Lval exp or a Const exp*/
access_or_const
: LTL_INT { PCst (IntConstant $1) }
| LTL_MINUS LTL_INT { PUnop (Uminus,PCst (IntConstant $2)) }
| access { $1 }
| LTL_LPAREN arith_relation LTL_RPAREN { $2 }
;
/* returns a lval */
access
: access LTL_RIGHT_ARROW LTL_LABEL { PField (PUnop(Ustar,$1),$3) }
| access LTL_DOT LTL_LABEL { PField($1,$3) }
| access_array {$1}
access_array
: access_array LTL_LEFT_SQUARE access_or_const LTL_RIGHT_SQUARE
{ PArrget($1,$3) }
| access_leaf {$1}
access_leaf
: LTL_ADRESSE access { PUnop (Uamp,$2) }
| LTL_STAR access { PUnop (Ustar, $2 ) }
| LTL_LABEL { PVar $1 }
| LTL_LPAREN access LTL_RPAREN { $2 }
;
bench/good/ltlparser.opp.exp 0 → 100644
View file @ bf483577
%{
open Promelaast
open Logic_ptree
let observed_expressions=Hashtbl.create 97
let ident_count=ref 0
let get_fresh_ident () =
ident_count:=!ident_count+1;
("buchfreshident"^(string_of_int !ident_count))
%}
%start ltl
%token LTL_TRUE
%token LTL_RPAREN
%token LTL_RIGHT_SQUARE
%token LTL_RIGHT_ARROW
%token LTL_RETURN
%token LTL_LPAREN
%token LTL_LEFT_SQUARE
%token <string> LTL_LABEL
%token <string> LTL_INT
%token LTL_FALSE
%token LTL_DOT
%token LTL_CALL_OR_RETURN
%token LTL_CALL
%token LTL_ADRESSE
%token EOF
%token LTL_OR
%token LTL_LEFT_RIGHT_ARROW
%token LTL_IMPLIES
%token LTL_AND
%token LTL_NOT
%token LTL_UNTIL
%token LTL_RELEASE
%token LTL_NEXT
%token LTL_GLOBALLY
%token LTL_FATALLY
%token LTL_NEQ
%token LTL_LT
%token LTL_LE
%token LTL_GT
%token LTL_GE
%token LTL_EQ
%token LTL_STAR
%token LTL_PLUS
%token LTL_MODULO
%token LTL_MINUS
%token LTL_DIV
%right LTL_OR LTL_LEFT_RIGHT_ARROW LTL_IMPLIES
%right LTL_AND
%nonassoc LTL_NOT
%right LTL_UNTIL LTL_RELEASE LTL_NEXT LTL_GLOBALLY LTL_FATALLY
%right LTL_NEQ LTL_LT LTL_LE LTL_GT LTL_GE LTL_EQ
%right LTL_STAR LTL_PLUS LTL_MODULO LTL_MINUS LTL_DIV
%type <(Ltlast.formula * (string, (Logic_ptree.relation * Promelaast.expression * Promelaast.expression)) Hashtbl.t)> ltl
%%
ltl:
| _1 = formula _2 = EOF
{ ((_1,observed_expressions))}
formula:
| _1 = LTL_TRUE
{ (Ltlast.LTrue)}
| _1 = LTL_FALSE
{ (Ltlast.LFalse)}
| _1 = LTL_LPAREN _2 = formula _3 = LTL_RPAREN
{ ( _2 )}
| _1 = LTL_GLOBALLY _2 = formula
{ ( Ltlast.LGlobally(_2) )}
| _1 = LTL_FATALLY _2 = formula
{ ( Ltlast.LFatally(_2) )}
| _1 = formula _2 = LTL_UNTIL _3 = formula
{ ( Ltlast.LUntil(_1,_3) )}
| _1 = formula _2 = LTL_RELEASE _3 = formula
{ ( Ltlast.LRelease(_1,_3) )}
| _1 = LTL_NEXT _2 = formula
{ ( Ltlast.LNext(_2) )}
| _1 = formula _2 = LTL_OR _3 = formula
{ ( Ltlast.LOr(_1,_3) )}
| _1 = formula _2 = LTL_AND _3 = formula
{ ( Ltlast.LAnd(_1,_3) )}
| _1 = LTL_NOT _2 = formula
{ ( Ltlast.LNot(_2) )}
| _1 = formula _2 = LTL_IMPLIES _3 = formula
{ ( Ltlast.LImplies(_1,_3) )}
| _1 = formula _2 = LTL_LEFT_RIGHT_ARROW _3 = formula
{ ( Ltlast.LIff(_1,_3) )}
| _1 = LTL_CALL _2 = LTL_LPAREN _3 = LTL_LABEL _4 = LTL_RPAREN
{ ( Ltlast.LCall(_3))}
| _1 = LTL_RETURN _2 = LTL_LPAREN _3 = LTL_LABEL _4 = LTL_RPAREN
{ ( Ltlast.LReturn(_3))}
| _1 = LTL_CALL_OR_RETURN _2 = LTL_LPAREN _3 = LTL_LABEL _4 = LTL_RPAREN
{ ( Ltlast.LCallOrReturn(_3))}
| _1 = logic_relation
{ (
let id = get_fresh_ident () in
Hashtbl.add observed_expressions id _1;
Ltlast.LIdent(id)
)}
logic_relation:
| _1 = arith_relation _2 = LTL_EQ _3 = arith_relation
{ ( Eq, _1 , _3)}
| _1 = arith_relation _2 = LTL_LT _3 = arith_relation
{ ( Lt, _1, _3 )}
| _1 = arith_relation _2 = LTL_GT _3 = arith_relation
{ ( Gt, _1, _3 )}
| _1 = arith_relation _2 = LTL_LE _3 = arith_relation
{ ( Le, _1, _3 )}
| _1 = arith_relation _2 = LTL_GE _3 = arith_relation
{ ( Ge, _1, _3 )}
| _1 = arith_relation _2 = LTL_NEQ _3 = arith_relation
{ ( Neq, _1, _3 )}
| _1 = arith_relation
{ ( Neq, _1, PCst (IntConstant "0") )}
arith_relation:
| _1 = arith_relation_mul _2 = LTL_PLUS _3 = arith_relation
{ ( PBinop(Badd,_1,_3) )}
| _1 = arith_relation_mul _2 = LTL_MINUS _3 = arith_relation
{ ( PBinop(Bsub,_1,_3) )}
| _1 = arith_relation_mul
{ ( _1 )}
arith_relation_mul:
| _1 = arith_relation_mul _2 = LTL_DIV _3 = access_or_const
{ ( PBinop(Bdiv,_1,_3) )}
| _1 = arith_relation_mul _2 = LTL_STAR _3 = access_or_const
{ ( PBinop(Bmul,_1,_3) )}
| _1 = arith_relation_mul _2 = LTL_MODULO _3 = access_or_const
{ ( PBinop(Bmod,_1,_3))}
| _1 = access_or_const
{ ( _1 )}
access_or_const:
| _1 = LTL_INT
{ ( PCst (IntConstant _1) )}
| _1 = LTL_MINUS _2 = LTL_INT
{ ( PUnop (Uminus,PCst (IntConstant _2)) )}
| _1 = access
{ ( _1 )}
| _1 = LTL_LPAREN _2 = arith_relation _3 = LTL_RPAREN
{ ( _2 )}
access:
| _1 = access _2 = LTL_RIGHT_ARROW _3 = LTL_LABEL
{ ( PField (PUnop(Ustar,_1),_3) )}
| _1 = access _2 = LTL_DOT _3 = LTL_LABEL
{ ( PField(_1,_3) )}
| _1 = access_array
{ (_1)}
access_array:
| _1 = access_array _2 = LTL_LEFT_SQUARE _3 = access_or_const _4 = LTL_RIGHT_SQUARE
{ ( PArrget(_1,_3) )}
| _1 = access_leaf
{ (_1)}
access_leaf:
| _1 = LTL_ADRESSE _2 = access
{ ( PUnop (Uamp,_2) )}
| _1 = LTL_STAR _2 = access
{ ( PUnop (Ustar, _2 ) )}
| _1 = LTL_LABEL
{ ( PVar _1 )}
| _1 = LTL_LPAREN _2 = access _3 = LTL_RPAREN
{ ( _2 )}
%%
bench/good/promelaparser.exp 0 → 100644
View file @ bf483577
File "promelaparser.mly", line 51, characters 0-9:
Warning: the precedence level assigned to PROMELA_FALSE is never useful.
File "promelaparser.mly", line 51, characters 0-9:
Warning: the precedence level assigned to PROMELA_TRUE is never useful.
bench/good/promelaparser.mly 0 → 100644
View file @ bf483577
/**************************************************************************/
/* */
/* This file is part of Aorai plug-in of Frama-C. */
/* */
/* Copyright (C) 2007-2015 */
/* CEA (Commissariat à l'énergie atomique et aux énergies */
/* alternatives) */
/* INRIA (Institut National de Recherche en Informatique et en */
/* Automatique) */
/* INSA (Institut National des Sciences Appliquees) */
/* */
/* you can redistribute it and/or modify it under the terms of the GNU */
/* Lesser General Public License as published by the Free Software */
/* Foundation, version 2.1. */
/* */
/* It is distributed in the hope that it will be useful, */
/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
/* GNU Lesser General Public License for more details. */
/* */
/* See the GNU Lesser General Public License version 2.1 */
/* for more details (enclosed in the file licenses/LGPLv2.1). */
/* */
/**************************************************************************/
/* $Id: promelaparser.mly,v 1.2 2008-10-02 13:33:29 uid588 Exp $ */
/* Originated from http://www.ltl2dstar.de/down/ltl2dstar-0.4.2.zip */
%{
open Promelaast
open Bool3
let observed_states=Hashtbl.create 1
let to_seq c =
[{ condition = Some c; nested = [];
min_rep = Some (PCst (Logic_ptree.IntConstant "1"));
max_rep = Some (PCst (Logic_ptree.IntConstant "1"));
}]
%}
%token PROMELA_OR
%token PROMELA_AND
%token PROMELA_NOT PROMELA_TRUE PROMELA_FALSE
%right PROMELA_OR
%right PROMELA_AND
%nonassoc PROMELA_NOT PROMELA_TRUE PROMELA_FALSE
%token PROMELA_NEVER PROMELA_IF PROMELA_FI PROMELA_GOTO PROMELA_SKIP
%token <string> PROMELA_LABEL
%token PROMELA_COLON PROMELA_SEMICOLON PROMELA_DOUBLE_COLON
%token PROMELA_LBRACE PROMELA_RBRACE PROMELA_LPAREN
%token PROMELA_RPAREN PROMELA_RIGHT_ARROW
%token <string> PROMELA_CALLOF PROMELA_RETURNOF PROMELA_CALLORRETURNOF
%token EOF
%type <Promelaast.parsed_automaton> promela
%start promela
%%
promela
: PROMELA_NEVER PROMELA_LBRACE states PROMELA_RBRACE EOF {
let states=
Hashtbl.fold (fun _ st l ->
if st.acceptation=Undefined || st.init=Undefined then
begin
Aorai_option.abort
"Error: the state %s is used but never defined" st.name;
end;
st::l
) observed_states []
in
(states , $3)
}
| PROMELA_NEVER PROMELA_LBRACE states PROMELA_SEMICOLON
PROMELA_RBRACE EOF {
let states=
Hashtbl.fold (fun _ st l ->
if st.acceptation=Undefined || st.init=Undefined then
begin
Aorai_option.abort
"Error: the state %s is used but never defined" st.name;
end;
st::l
) observed_states []
in
(states , $3) }
;
states
: states PROMELA_SEMICOLON state {
$1@$3
}
| state { $1 }
;
state
: state_labels state_body {
let (stl,trans)=$1 in
let (trl,force_final)=$2 in
if force_final then
begin
List.iter (fun s ->
try
(Hashtbl.find observed_states s.name).acceptation <- True
with
| Not_found -> assert false
(* This state has to be in the hashtable -- by construction *)
) stl
end;
if trl=[] then
trans
else
let tr_list=
List.fold_left (fun l1 (cr,stop_st) ->
List.fold_left (fun l2 st ->
{start=st;stop=stop_st;cross=Seq (to_seq cr);numt=(-1)}::l2
) l1 stl
) [] trl
in
(List.rev tr_list)@trans
}
;
state_labels
: label state_labels {
let (stl1,trl1)=$1 in
let (stl2,trl2)=$2 in
(stl1@stl2,trl1@trl2)
}
| label { $1 }
;
label
: PROMELA_LABEL PROMELA_COLON {