Project

General

Profile

Revision 4f26dcf5

View differences:

TODO.org
133 133

  
134 134
** Development
135 135
*** Done
136
- (ploc) retirer le parser Kind2 et revenir à celui de lustrec
136 137
*** To be done
137 138
**** Court terme
138

  
139
- (CG) etendre la syntaxe pour coller à la definition donnée ci-dessus
140
  - lexeur/parseur lustreSpec + document latex de grammaire
139 141
- repartir la branche acsl2018 qui contient la normalisation des eexpr
140 142
  - le refaire compiler
141 143
  - merger avec unstable 
142 144
- transformer cette normalisation pour partager les definitions locales de
143 145
  variables dans le noeud de spec, aka contract
144
- retirer le parser Kind21 et revenir à celui de lustrec
145
- (CG) etendre la syntaxe pour coller à la definition donnée ci-dessus
146
  - lexeur/parseur lustreSpec + document latex de grammaire
147 146

  
148 147
**** Apres
149 148
- developper dans les backends
src/corelang.ml
165 165
(*   Eexpr functions *)
166 166
(************************************************************)
167 167

  
168
let merge_node_annot ann1 ann2 =
168
let merge_contracts ann1 ann2 =
169 169
  { requires = ann1.requires @ ann2.requires;
170 170
    ensures = ann1.ensures @ ann2.ensures;
171 171
    behaviors = ann1.behaviors @ ann2.behaviors;
src/corelang.mli
156 156

  
157 157
(** Annotation expression related functions *)
158 158
val mkeexpr: Location.t ->  expr -> eexpr
159
val merge_node_annot: node_annot -> node_annot -> node_annot 
159
val merge_contracts:  contract_desc -> contract_desc -> contract_desc 
160 160
val extend_eexpr: (quantifier_type * var_decl list) list -> eexpr -> eexpr
161 161
val update_expr_annot: ident -> expr -> expr_annot -> expr
162 162
(* val mkpredef_call: Location.t -> ident -> eexpr list -> eexpr*)
src/lustre_types.ml
124 124
 {annots: (string list * eexpr) list;
125 125
  annot_loc: Location.t}
126 126

  
127
type node_annot = {
127
type contract_desc = {
128
(* TODO: 
129
   local variables 
130
   rename: assume/guarantee
131
           in behavior mode (id, requires/ensures)
132
   import contract
133
*)
134
  
128 135
  requires: eexpr list;
129 136
  ensures: eexpr list;
130 137
  behaviors: (string * eexpr list * eexpr list * Location.t) list;
......
173 180
     node_stmts: statement list;
174 181
     mutable node_dec_stateless: bool;
175 182
     mutable node_stateless: bool option;
176
     node_spec: node_annot option;
183
     node_spec: contract_desc option;
177 184
     node_annot: expr_annot list;
178 185
    }
179 186

  
......
184 191
     nodei_inputs: var_decl list;
185 192
     nodei_outputs: var_decl list;
186 193
     nodei_stateless: bool;
187
     nodei_spec: node_annot option;
194
     nodei_spec: contract_desc option;
188 195
     (* nodei_annot: expr_annot list; *)
189 196
     nodei_prototype: string option;
190 197
     nodei_in_lib: string list;
......
204 211
| Open of bool * string (* the boolean set to true denotes a local
205 212
			   lusi vs a lusi installed at system level *)
206 213
| TypeDef of typedef_desc
207

  
214
| Contract of contract_desc
215
    
208 216
type top_decl =
209 217
    {top_decl_desc: top_decl_desc;      (* description of the symbol *)
210 218
     top_decl_owner: Location.filename; (* the module where it is defined *)
src/machine_code_types.ml
51 51
  mstatic: var_decl list; (* static inputs only *)
52 52
  mconst: instr_t list; (* assignments of node constant locals *)
53 53
  mstep: step_t;
54
  mspec: node_annot option;
54
  mspec: contract_desc option;
55 55
  mannot: expr_annot list;
56 56
}
src/parser_lustre.mly
56 56
%token <Num.num * int * string> REAL
57 57

  
58 58
%token <string> STRING
59
%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME LAST
59
%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME 
60 60
%token ASSERT OPEN QUOTE FUNCTION
61 61
%token <string> IDENT
62 62
%token <string> UIDENT
63 63
%token TRUE FALSE
64 64
%token <Lustre_types.expr_annot> ANNOT
65
%token <Lustre_types.node_annot> NODESPEC
65
%token <Lustre_types.contract_desc> NODESPEC
66 66
%token LBRACKET RBRACKET LCUR RCUR LPAR RPAR SCOL COL COMMA COLCOL 
67 67
%token AMPERAMPER BARBAR NOT POWER
68 68
%token IF THEN ELSE
......
113 113
%type <Lustre_types.expr_annot> lustre_annot
114 114

  
115 115
%start lustre_spec
116
%type <Lustre_types.node_annot> lustre_spec
116
%type <Lustre_types.contract_desc> lustre_spec
117 117

  
118 118
%start signed_const
119 119
%type <Lustre_types.constant> signed_const
......
248 248
| NODESPEC nodespec_list { 
249 249
  (function 
250 250
  | None    -> (fun s1 -> Some s1) 
251
  | Some s2 -> (fun s1 -> Some (merge_node_annot s1 s2))) $2 $1 }
251
  | Some s2 -> (fun s1 -> Some (merge_contracts s1 s2))) $2 $1 }
252 252

  
253 253
typ_def_list:
254 254
    /* empty */             { (fun itf -> []) }

Also available in: Unified diff