Project

General

Profile

« Previous | Next » 

Revision 1b57e111

Added by Teme Kahsai almost 8 years ago

adding sfunction support

View differences:

src/parserLustreSpec.mly
52 52 
%token PRE ARROW
53 53 
%token EOF
54 54 
%token REQUIRES ENSURES OBSERVER
55 
%token INVARIANT BEHAVIOR ASSUMES
55 
%token INVARIANT BEHAVIOR ASSUMES CCODE MATLAB
56 56 
%token EXISTS FORALL
57 57 

  		




  58
  58
  
    
%nonassoc prec_exists prec_forall


  		




  ......




  295
  295
  
    
| IDENT COL expr SCOL lustre_annot_list { ([$1],$3)::$5 }


  		




  296
  296
  
    
| INVARIANT COL expr SCOL lustre_annot_list{ (["invariant"],$3)::$5 }


  		




  297
  297
  
    
| OBSERVER COL expr SCOL lustre_annot_list { (["observer"],$3)::$5 }


  		




  
  298
  
    
| CCODE COL const lustre_annot_list{ (["c_code"],$3)::$5 }


  		




  
  299
  
    
| MATLAB COL const lustre_annot_list{ (["matlab"],$3)::$5 }


  		




  298
  300
  
    

  		




  299
  301
  
    
kwd:


  		




  300
  302
  
    
DIV { [] }


  		












Also available in:  Unified diff