Revision dccec723
Added by LĂ©lio Brun over 3 years ago
lustrec.opam | ||
---|---|---|
25 | 25 |
] |
26 | 26 |
depopts: ["z3"] |
27 | 27 |
build: [ |
28 |
["dune" "subst" "--root" "."] {dev}
|
|
28 |
["dune" "subst"] {dev} |
|
29 | 29 |
[ |
30 | 30 |
"dune" |
31 | 31 |
"build" |
... | ... | |
33 | 33 |
name |
34 | 34 |
"-j" |
35 | 35 |
jobs |
36 |
"--promote-install-files" |
|
37 |
"false" |
|
36 |
"--promote-install-files=false" |
|
38 | 37 |
"@install" |
39 | 38 |
"@runtest" {with-test} |
40 | 39 |
"@doc" {with-doc} |
src/backends/Ada/ada_backend.ml | ||
---|---|---|
86 | 86 |
l) -> assert false | Expr_appl call -> assert false *) |
87 | 87 |
in |
88 | 88 |
match m.mspec.mnode_spec with |
89 |
| Some (NodeSpec (ident, _)) ->
|
|
89 |
| Some (NodeSpec ident) ->
|
|
90 | 90 |
let machine_spec = find_submachine_from_ident ident machines in |
91 | 91 |
let guarantees = |
92 | 92 |
match machine_spec.mspec.mnode_spec with |
src/backends/C/c_backend_spec.ml | ||
---|---|---|
195 | 195 |
pp_var_decl |
196 | 196 |
|
197 | 197 |
let pp_forall pp_l pp_r fmt (l, r) = |
198 |
fprintf fmt "@[<v 2>\\forall %a;@,%a@]" pp_l l pp_r r
|
|
198 |
fprintf fmt "@[<v 2>\\forall @[<hov>%a@];@,%a@]" pp_l l pp_r r
|
|
199 | 199 |
|
200 | 200 |
let pp_exists pp_l pp_r fmt (l, r) = |
201 | 201 |
fprintf fmt "@[<v 2>\\exists %a;@,%a@]" pp_l l pp_r r |
... | ... | |
240 | 240 |
let pp_initialization pp_mem fmt (name, mem) = |
241 | 241 |
fprintf fmt "%s_initialization(%a)" name pp_mem mem |
242 | 242 |
|
243 |
let pp_init pp_mem fmt (name, mem) = |
|
244 |
fprintf fmt "%s_init(%a)" name pp_mem mem |
|
245 |
|
|
243 | 246 |
let pp_initialization' = pp_initialization pp_print_string |
244 | 247 |
|
245 | 248 |
let pp_local m = |
... | ... | |
628 | 631 |
let pp_lemma pp_l pp_r fmt (l, r) = |
629 | 632 |
fprintf fmt "@[<v 2>lemma %a:@,%a;@]" pp_l l pp_r r |
630 | 633 |
|
634 |
let pp_axiomatic pp_l pp_r fmt (l, r) = |
|
635 |
fprintf fmt "@[<v 2>axiomatic %a {@,%a@]@;}" pp_l l pp_r r |
|
636 |
|
|
637 |
let pp_axiom pp_l pp_r fmt (l, r) = |
|
638 |
fprintf fmt "@[<v 2>axiom %a:@,%a;@]" pp_l l pp_r r |
|
639 |
|
|
631 | 640 |
let pp_mem_valid_def fmt m = |
632 | 641 |
if not (fst (get_stateless_status m)) then |
633 | 642 |
let name = m.mname.node_id in |
... | ... | |
991 | 1000 |
fmt |
992 | 1001 |
() |
993 | 1002 |
|
994 |
let pp_node_spec m fmt = function |
|
995 |
| Contract c |
|
996 |
| NodeSpec (_, Some c) -> |
|
997 |
PrintSpec.pp_spec PrintSpec.TransitionMode m fmt |
|
998 |
(Spec_common.red (Imply (c.mc_pre, c.mc_post))) |
|
999 |
| NodeSpec (f, None) -> |
|
1000 |
pp_print_string fmt f |
|
1003 |
let spec_from_contract c = |
|
1004 |
Spec_common.red (Imply (c.mc_pre, c.mc_post)) |
|
1005 |
|
|
1006 |
let pp_contract m fmt c = |
|
1007 |
PrintSpec.pp_spec PrintSpec.TransitionMode m fmt (spec_from_contract c) |
|
1008 |
|
|
1009 |
let contract_of machines m = |
|
1010 |
match m.mspec.mnode_spec with |
|
1011 |
| Some spec -> |
|
1012 |
begin match spec with |
|
1013 |
| Contract c -> |
|
1014 |
Some c, None |
|
1015 |
| NodeSpec f -> |
|
1016 |
let m_f = find_machine f machines in |
|
1017 |
begin match m_f.mspec.mnode_spec with |
|
1018 |
| Some (Contract c) -> |
|
1019 |
Some c, Some m_f |
|
1020 |
| _ -> |
|
1021 |
None, None |
|
1022 |
end |
|
1023 |
end |
|
1024 |
| None -> |
|
1025 |
None, None |
|
1026 |
|
|
1027 |
let pp_init_def fmt m = |
|
1028 |
let name = m.mname.node_id in |
|
1029 |
let mem = mk_mem m in |
|
1030 |
pp_predicate |
|
1031 |
(pp_init (pp_machine_decl' ~ghost:true)) |
|
1032 |
(pp_and pp_initialization' (pp_reset_flag' ~indirect:false)) |
|
1033 |
fmt |
|
1034 |
((name, (name, mem)), ((name, mem), mem)) |
|
1035 |
|
|
1036 |
let rename n x = sprintf "%s_%d" x n |
|
1037 |
|
|
1038 |
let rename_var_decl n vd = { vd with var_id = rename n vd.var_id } |
|
1039 |
|
|
1040 |
let rec rename_value n v = |
|
1041 |
{ v with value_desc = |
|
1042 |
match v.value_desc with |
|
1043 |
| Machine_code_types.Var v -> Machine_code_types.Var (rename_var_decl n v) |
|
1044 |
| Fun (f, vs) -> Fun (f, List.map (rename_value n) vs) |
|
1045 |
| Array vs -> Array (List.map (rename_value n) vs) |
|
1046 |
| Access (v1, v2) -> Access (rename_value n v1, rename_value n v2) |
|
1047 |
| Power (v1, v2) -> Power (rename_value n v1, rename_value n v2) |
|
1048 |
| v -> v |
|
1049 |
} |
|
1050 |
|
|
1051 |
let rename_expression: type a. int -> (value_t, a) expression_t -> (value_t, a) expression_t = |
|
1052 |
fun n -> function |
|
1053 |
| Val v -> Val (rename_value n v) |
|
1054 |
| Var v -> Var (rename_var_decl n v) |
|
1055 |
| e -> e |
|
1056 |
|
|
1057 |
let rename_predicate n = function |
|
1058 |
| Transition (f, inst, i, es, r, mf, mif) -> |
|
1059 |
Transition (f, inst, i, List.map (rename_expression n) es, r, mf, mif) |
|
1060 |
| p -> p |
|
1061 |
|
|
1062 |
let rec rename_formula n = function |
|
1063 |
| Equal (e1, e2) -> Equal (rename_expression n e1, rename_expression n e2) |
|
1064 |
| And fs -> And (List.map (rename_formula n) fs) |
|
1065 |
| Or fs -> Or (List.map (rename_formula n) fs) |
|
1066 |
| Imply (f1, f2) -> Imply (rename_formula n f1, rename_formula n f2) |
|
1067 |
| Exists (xs, f) -> Exists (List.map (rename_var_decl n) xs, rename_formula n f) |
|
1068 |
| Forall (xs, f) -> Forall (List.map (rename_var_decl n) xs, rename_formula n f) |
|
1069 |
| Ternary (e, t, f) -> Ternary (rename_expression n e, rename_formula n t, rename_formula n f) |
|
1070 |
| Predicate p -> Predicate (rename_predicate n p) |
|
1071 |
| ExistsMem (x, f1, f2) -> ExistsMem (rename n x, rename_formula n f1, rename_formula n f2) |
|
1072 |
| Value v -> Value (rename_value n v) |
|
1073 |
| f -> f |
|
1074 |
|
|
1075 |
|
|
1076 |
let rename_contract n c = |
|
1077 |
{ c with |
|
1078 |
mc_pre = rename_formula n c.mc_pre; |
|
1079 |
mc_post = rename_formula n c.mc_post; } |
|
1080 |
|
|
1081 |
let but_last l = |
|
1082 |
List.(rev (tl (rev l))) |
|
1083 |
|
|
1084 |
let pp_k_induction_case case m pp_mem_in pp_mem_out pp_vars fmt (n, mem_in, mem_out) = |
|
1085 |
let name = m.mname.node_id in |
|
1086 |
let inputs = m.mstep.step_inputs in |
|
1087 |
let outputs = m.mstep.step_outputs in |
|
1088 |
fprintf fmt "%s_%s_%d(@[<hov>%a,@;%a,@;%a@])" |
|
1089 |
name |
|
1090 |
case |
|
1091 |
n |
|
1092 |
pp_mem_in |
|
1093 |
mem_in |
|
1094 |
pp_vars |
|
1095 |
(inputs @ outputs) |
|
1096 |
pp_mem_out |
|
1097 |
mem_out |
|
1098 |
|
|
1099 |
let pp_k_induction_base_case m = |
|
1100 |
pp_k_induction_case "base" m |
|
1101 |
|
|
1102 |
let pp_k_induction_inductive_case m = |
|
1103 |
pp_k_induction_case "inductive" m |
|
1104 |
|
|
1105 |
let pp_base_cases m fmt (c, m_c, k) = |
|
1106 |
let name = m.mname.node_id in |
|
1107 |
let mem = mk_mem m in |
|
1108 |
let inputs = m.mstep.step_inputs in |
|
1109 |
let outputs = m.mstep.step_outputs in |
|
1110 |
let l = List.init (k - 1) (fun n -> n + 1) in |
|
1111 |
pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:pp_print_cutcut |
|
1112 |
(fun fmt n -> |
|
1113 |
let l = List.init (n + 1) (fun n -> n) in |
|
1114 |
let l' = List.init n (fun n -> n) in |
|
1115 |
let pp = |
|
1116 |
pp_implies |
|
1117 |
(pp_and |
|
1118 |
(pp_and_l (fun fmt -> function |
|
1119 |
| 0 -> |
|
1120 |
pp_init pp_print_string fmt (name, rename 0 mem) |
|
1121 |
| n -> |
|
1122 |
pp_transition_aux m pp_print_string pp_print_string pp_var_decl |
|
1123 |
fmt |
|
1124 |
(name, |
|
1125 |
List.map (rename_var_decl n) (inputs @ outputs), |
|
1126 |
rename (n - 1) mem, |
|
1127 |
rename n mem))) |
|
1128 |
(pp_transition_aux m_c pp_print_string pp_print_string pp_var_decl)) |
|
1129 |
(pp_contract m) |
|
1130 |
in |
|
1131 |
pp_predicate |
|
1132 |
(pp_k_induction_base_case |
|
1133 |
m |
|
1134 |
(pp_machine_decl' ~ghost:true) |
|
1135 |
(pp_machine_decl' ~ghost:true) |
|
1136 |
(fun fmt xs -> pp_locals m fmt (List.map (rename_var_decl n) xs))) |
|
1137 |
(pp_forall (pp_locals m) |
|
1138 |
(if n > 1 then |
|
1139 |
pp_forall |
|
1140 |
(fun fmt l -> fprintf fmt "%a@,%a" |
|
1141 |
(pp_machine_decl ~ghost:true |
|
1142 |
(pp_comma_list ~pp_eol:pp_print_comma |
|
1143 |
(fun fmt n -> pp_print_string fmt (rename n mem)))) |
|
1144 |
(name, but_last l) |
|
1145 |
(pp_locals m) |
|
1146 |
(List.flatten |
|
1147 |
(List.map (fun n -> |
|
1148 |
List.map (rename_var_decl n) (inputs @ outputs)) |
|
1149 |
(List.tl l)))) |
|
1150 |
pp |
|
1151 |
else |
|
1152 |
fun fmt (_, x) -> pp fmt x)) |
|
1153 |
fmt |
|
1154 |
((n, (name, rename (n - 1) mem), (name, rename n mem)), |
|
1155 |
(List.map (rename_var_decl n) m_c.mstep.step_outputs, |
|
1156 |
(l', ((l, |
|
1157 |
(m_c.mname.node_id, |
|
1158 |
List.map (rename_var_decl n) (m_c.mstep.step_inputs @ m_c.mstep.step_outputs), |
|
1159 |
"", "")), |
|
1160 |
rename_contract n c))))) |
|
1161 |
fmt |
|
1162 |
l |
|
1163 |
|
|
1164 |
let pp_inductive_case m fmt (c, m_c, k) = |
|
1165 |
let name = m.mname.node_id in |
|
1166 |
let mem = mk_mem m in |
|
1167 |
let inputs = m.mstep.step_inputs in |
|
1168 |
let outputs = m.mstep.step_outputs in |
|
1169 |
let l = List.init k (fun n -> n + 1) in |
|
1170 |
let pp = |
|
1171 |
pp_implies |
|
1172 |
(pp_and_l (fun fmt n -> |
|
1173 |
pp_and |
|
1174 |
(pp_and |
|
1175 |
(pp_transition_aux m pp_print_string pp_print_string pp_var_decl) |
|
1176 |
(pp_transition_aux m_c pp_print_string pp_print_string pp_var_decl)) |
|
1177 |
(pp_contract m) |
|
1178 |
fmt |
|
1179 |
(((name, |
|
1180 |
List.map (rename_var_decl n) (inputs @ outputs), |
|
1181 |
rename (n - 1) mem, |
|
1182 |
rename n mem), |
|
1183 |
(m_c.mname.node_id, |
|
1184 |
List.map (rename_var_decl n) (m_c.mstep.step_inputs @ m_c.mstep.step_outputs), |
|
1185 |
"", "")), |
|
1186 |
rename_contract n c))) |
|
1187 |
(pp_contract m) |
|
1188 |
in |
|
1189 |
pp_predicate |
|
1190 |
(pp_k_induction_inductive_case |
|
1191 |
m |
|
1192 |
(pp_machine_decl' ~ghost:true) |
|
1193 |
(pp_machine_decl' ~ghost:true) |
|
1194 |
(fun fmt xs -> pp_locals m fmt (List.map (rename_var_decl k) xs))) |
|
1195 |
(pp_forall (pp_locals m) |
|
1196 |
(if k > 1 then |
|
1197 |
pp_forall |
|
1198 |
(fun fmt l -> fprintf fmt "%a@,%a" |
|
1199 |
(pp_machine_decl ~ghost:true |
|
1200 |
(pp_comma_list ~pp_eol:pp_print_comma |
|
1201 |
(fun fmt n -> pp_print_string fmt (rename (n - 1) mem)))) |
|
1202 |
(name, but_last l) |
|
1203 |
(pp_locals m) |
|
1204 |
(List.flatten |
|
1205 |
(List.map (fun n -> |
|
1206 |
List.map (rename_var_decl (n - 1)) (inputs @ outputs)) |
|
1207 |
(List.tl l)))) |
|
1208 |
pp |
|
1209 |
else |
|
1210 |
fun fmt (_, x) -> pp fmt x)) |
|
1211 |
fmt |
|
1212 |
((k, (name, rename (k - 1) mem), (name, rename k mem)), |
|
1213 |
(List.(flatten (List.map (fun n -> List.map (rename_var_decl n) m_c.mstep.step_outputs) l)), |
|
1214 |
(l, (l, rename_contract k c)))) |
|
1215 |
|
|
1216 |
let pp_k_induction_lemmas m fmt k = |
|
1217 |
let name = m.mname.node_id in |
|
1218 |
let mem_in = mk_mem_in m in |
|
1219 |
let mem_out = mk_mem_out m in |
|
1220 |
let inputs = m.mstep.step_inputs in |
|
1221 |
let outputs = m.mstep.step_outputs in |
|
1222 |
let l = List.init k (fun n -> n + 1) in |
|
1223 |
pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:pp_print_cutcut |
|
1224 |
(fun fmt n -> |
|
1225 |
pp_lemma |
|
1226 |
(fun fmt n -> fprintf fmt "%s_k_induction_%d" name n) |
|
1227 |
(pp_forall |
|
1228 |
(fun fmt () -> fprintf fmt "%a,@;%a" |
|
1229 |
(pp_machine_decl ~ghost:true (pp_comma_list pp_print_string)) |
|
1230 |
(name, [mem_in; mem_out]) |
|
1231 |
(pp_locals m) |
|
1232 |
(inputs @ outputs)) |
|
1233 |
((if n = k then |
|
1234 |
pp_k_induction_inductive_case |
|
1235 |
else |
|
1236 |
pp_k_induction_base_case) |
|
1237 |
m |
|
1238 |
pp_print_string |
|
1239 |
pp_print_string |
|
1240 |
(pp_comma_list pp_var_decl))) |
|
1241 |
fmt |
|
1242 |
(n, ((), (n, mem_in, mem_out)))) |
|
1243 |
fmt |
|
1244 |
l |
|
1245 |
|
|
1246 |
let pp_k_induction_axiom m fmt (c, m_c, k) = |
|
1247 |
let name = m.mname.node_id in |
|
1248 |
let mem_in = mk_mem_in m in |
|
1249 |
let mem_out = mk_mem_out m in |
|
1250 |
let inputs = m.mstep.step_inputs in |
|
1251 |
let outputs = m.mstep.step_outputs in |
|
1252 |
let l = List.init k (fun n -> n + 1) in |
|
1253 |
pp_axiomatic |
|
1254 |
(fun fmt () -> fprintf fmt "%s_k_Induction" name) |
|
1255 |
(pp_axiom |
|
1256 |
(fun fmt () -> fprintf fmt "%s_k_induction" name) |
|
1257 |
(pp_forall |
|
1258 |
(pp_locals m) |
|
1259 |
(pp_forall |
|
1260 |
(fun fmt () -> fprintf fmt "%a,@;%a" |
|
1261 |
(pp_machine_decl ~ghost:true (pp_comma_list pp_print_string)) |
|
1262 |
(name, [mem_in; mem_out]) |
|
1263 |
(pp_locals m) |
|
1264 |
(inputs @ outputs)) |
|
1265 |
(pp_implies |
|
1266 |
(pp_and |
|
1267 |
(pp_and_l |
|
1268 |
(fun fmt n -> |
|
1269 |
(if n = k then |
|
1270 |
pp_k_induction_inductive_case |
|
1271 |
else |
|
1272 |
pp_k_induction_base_case) |
|
1273 |
m |
|
1274 |
pp_print_string |
|
1275 |
pp_print_string |
|
1276 |
(pp_comma_list pp_var_decl) |
|
1277 |
fmt |
|
1278 |
(n, mem_in, mem_out))) |
|
1279 |
(pp_transition_aux m_c pp_print_string pp_print_string pp_var_decl)) |
|
1280 |
(pp_contract m))))) |
|
1281 |
fmt |
|
1282 |
((), |
|
1283 |
((), |
|
1284 |
(m_c.mstep.step_outputs, |
|
1285 |
((), |
|
1286 |
(((l, |
|
1287 |
(m_c.mname.node_id, |
|
1288 |
m_c.mstep.step_inputs @ m_c.mstep.step_outputs, |
|
1289 |
"", "")), c)))))) |
|
1290 |
|
|
1291 |
|
|
1292 |
let pp_k_induction m fmt (_, _, k as c_m_k) = |
|
1293 |
pp_acsl_cut |
|
1294 |
(fun fmt () -> fprintf fmt "%a@,@,%a@,@,%a@,@,%a@,@,%a" |
|
1295 |
pp_init_def m |
|
1296 |
(pp_base_cases m) c_m_k |
|
1297 |
(pp_inductive_case m) c_m_k |
|
1298 |
(pp_k_induction_lemmas m) k |
|
1299 |
(pp_k_induction_axiom m) c_m_k) |
|
1300 |
fmt |
|
1301 |
() |
|
1302 |
|
|
1303 |
let pp_proof_annotation m m_c fmt c = |
|
1304 |
let pp m_c fmt = function |
|
1305 |
| Kinduction k -> |
|
1306 |
pp_k_induction m fmt (c, m_c, k) |
|
1307 |
in |
|
1308 |
match m_c with |
|
1309 |
| Some m_c -> |
|
1310 |
pp_print_option (pp m_c) fmt c.mc_proof |
|
1311 |
| None -> () |
|
1001 | 1312 |
|
1002 | 1313 |
let pp_step_spec fmt machines self mem m = |
1003 | 1314 |
let name = m.mname.node_id in |
... | ... | |
1014 | 1325 |
let pp_if_outputs pp = |
1015 | 1326 |
if outputs = [] then pp_print_nothing else pp |
1016 | 1327 |
in |
1017 |
let spec = m.mspec.mnode_spec in
|
|
1328 |
let c, m_c = contract_of machines m in
|
|
1018 | 1329 |
(* (\* prevent printing an ensures clause with contract name *\) |
1019 | 1330 |
* let spec = |
1020 | 1331 |
* match m.mspec.mnode_spec with |
... | ... | |
1022 | 1333 |
* | s -> s |
1023 | 1334 |
* in *) |
1024 | 1335 |
let pp_spec = pp_print_option |
1025 |
(if m.mis_contract then pp_print_nothing else pp_ensures (pp_node_spec m)) in |
|
1336 |
(if m.mis_contract then pp_print_nothing else pp_ensures (pp_contract m)) in |
|
1337 |
let pp_spec_vars, pp_assigns_spec_vars = |
|
1338 |
match m.mspec.mnode_spec with |
|
1339 |
| Some (NodeSpec f) -> |
|
1340 |
let m_f = find_machine f machines in |
|
1341 |
pp_acsl_cut |
|
1342 |
(pp_ghost |
|
1343 |
(fun fmt () -> |
|
1344 |
fprintf |
|
1345 |
fmt |
|
1346 |
"@;<0 2>@[<v>%a@]" |
|
1347 |
(pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:pp_print_semicolon |
|
1348 |
~pp_eol:pp_print_semicolon (pp_c_decl_local_var m)) |
|
1349 |
m_f.mstep.step_outputs)), |
|
1350 |
fun fmt () -> pp_assigns pp_var_decl fmt m_f.mstep.step_outputs |
|
1351 |
| _ -> pp_print_nothing, pp_print_nothing |
|
1352 |
in |
|
1353 |
pp_print_option (pp_proof_annotation m m_c) fmt c; |
|
1354 |
pp_spec_vars fmt (); |
|
1026 | 1355 |
pp_acsl_cut |
1027 | 1356 |
~ghost:m.mis_contract |
1028 | 1357 |
(fun fmt () -> |
1029 | 1358 |
if fst (get_stateless_status m) then |
1030 | 1359 |
fprintf |
1031 | 1360 |
fmt |
1032 |
"%a@,%a@,%a@,%a@,%a" |
|
1361 |
"%a@,%a@,%a@,%a@,%a@,%a"
|
|
1033 | 1362 |
(pp_if_outputs (pp_requires (pp_valid pp_var_decl))) |
1034 | 1363 |
outputs |
1035 | 1364 |
(pp_if_outputs (pp_requires pp_separated'')) |
1036 | 1365 |
outputs |
1366 |
pp_assigns_spec_vars () |
|
1037 | 1367 |
(pp_assigns pp_ptr_decl) |
1038 | 1368 |
outputs |
1039 | 1369 |
(pp_ensures (pp_transition_aux' m)) |
1040 | 1370 |
(name, inputs @ outputs, "", "") |
1041 | 1371 |
pp_spec |
1042 |
spec
|
|
1372 |
c |
|
1043 | 1373 |
else |
1044 | 1374 |
fprintf |
1045 | 1375 |
fmt |
1046 |
"%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a" |
|
1376 |
"%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a"
|
|
1047 | 1377 |
(pp_if_outputs (pp_requires (pp_valid pp_var_decl))) |
1048 | 1378 |
outputs |
1049 | 1379 |
(pp_requires pp_mem_valid') |
... | ... | |
1059 | 1389 |
(if is_output m v then pp_ptr_decl else pp_var_decl) fmt v))) |
1060 | 1390 |
(name, inputs @ outputs, mem, mem) |
1061 | 1391 |
pp_spec |
1062 |
spec |
|
1392 |
c |
|
1393 |
pp_assigns_spec_vars () |
|
1063 | 1394 |
(pp_assigns pp_ptr_decl) |
1064 | 1395 |
outputs |
1065 | 1396 |
(pp_assigns (pp_reg self)) |
... | ... | |
1131 | 1462 |
|
1132 | 1463 |
let pp_contract fmt machines _self m = |
1133 | 1464 |
match m.mspec.mnode_spec with |
1134 |
| Some (NodeSpec (f, _)) ->
|
|
1465 |
| Some (NodeSpec f) ->
|
|
1135 | 1466 |
let m_f = find_machine f machines in |
1136 |
pp_acsl_cut |
|
1467 |
pp_acsl_line'_cut
|
|
1137 | 1468 |
(pp_ghost |
1138 | 1469 |
(fun fmt () -> |
1139 | 1470 |
fprintf |
1140 | 1471 |
fmt |
1141 |
"@;<0 2>@[<v>%a%a(%a%a);@]" |
|
1142 |
(pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:pp_print_semicolon ~pp_eol:pp_print_semicolon (pp_c_decl_local_var m)) |
|
1143 |
m_f.mstep.step_outputs |
|
1472 |
"%a(%a%a);" |
|
1144 | 1473 |
pp_machine_step_name |
1145 | 1474 |
m_f.mname.node_id |
1146 | 1475 |
(pp_comma_list ~pp_eol:pp_print_comma (pp_c_var_read m)) |
src/backends/EMF/EMF_backend.ml | ||
---|---|---|
489 | 489 |
(* TODO *) |
490 | 490 |
(* assert (c.locals = [] && c.consts = [] && c.stmts = [] && c.imports = []); *) |
491 | 491 |
fprintf fmt "\"spec\": %a,@ " pp_emf_spec c |
492 |
| Some (NodeSpec (id, _)) -> fprintf fmt "\"contract\": \"%s\",@ " id);
|
|
492 |
| Some (NodeSpec id) -> fprintf fmt "\"contract\": \"%s\",@ " id);
|
|
493 | 493 |
fprintf fmt "\"annots\": {@[<v 0> %a@]@ }" |
494 | 494 |
(pp_emf_annots_list (ref 0)) |
495 | 495 |
m.mannot; |
... | ... | |
519 | 519 |
(match ind.nodei_spec with |
520 | 520 |
| None -> fprintf fmt "@ " |
521 | 521 |
| Some (Contract _) -> assert false (* should have been processed *) |
522 |
| Some (NodeSpec (id, _)) -> fprintf fmt ",@ \"coco_contract\": %s" id);
|
|
522 |
| Some (NodeSpec id) -> fprintf fmt ",@ \"coco_contract\": %s" id);
|
|
523 | 523 |
fprintf fmt "@]@ }" |
524 | 524 |
(* XXX: UNUSED *) |
525 | 525 |
(* with Unhandled msg -> |
src/causality.ml | ||
---|---|---|
475 | 475 |
match nd.node_spec with |
476 | 476 |
| None -> |
477 | 477 |
[] |
478 |
| Some (NodeSpec (id, _)) ->
|
|
478 |
| Some (NodeSpec id) ->
|
|
479 | 479 |
[ id ] |
480 | 480 |
| Some (Contract c) -> |
481 | 481 |
get_contract_calls (fun _ -> true) c |
src/compiler_common.ml | ||
---|---|---|
330 | 330 |
c.spec_loc |
331 | 331 |
top.top_decl_owner |
332 | 332 |
top.top_decl_itf |
333 |
(Node nd), |
|
334 |
c |
|
333 |
(Node nd) |
|
335 | 334 |
(* { nd with |
336 | 335 |
* node_dec_stateless = stateless; |
337 | 336 |
* node_stateless = Some stateless; |
... | ... | |
373 | 372 |
| Some (Contract _) -> |
374 | 373 |
(* A contract: processing it *) |
375 | 374 |
(* we bind a fresh node *) |
376 |
let new_nd, new_c = process_contract_new_node accu_contracts prog top in
|
|
375 |
let new_nd = process_contract_new_node accu_contracts prog top in |
|
377 | 376 |
(* Format.eprintf "Creating new contract node %s@." (node_name |
378 | 377 |
new_nd); *) |
379 | 378 |
let nd = |
380 |
{ nd with node_spec = Some (NodeSpec (node_name new_nd, Some new_c)) }
|
|
379 |
{ nd with node_spec = Some (NodeSpec (node_name new_nd)) } |
|
381 | 380 |
in |
382 | 381 |
( new_nd :: accu_contracts, |
383 | 382 |
{ top with top_decl_desc = Node nd } :: accu_nodes )) |
... | ... | |
392 | 391 |
| Some (Contract _) -> |
393 | 392 |
(* A contract: processing it *) |
394 | 393 |
(* we bind a fresh node *) |
395 |
let new_nd, new_c = process_contract_new_node accu_contracts prog top in
|
|
394 |
let new_nd = process_contract_new_node accu_contracts prog top in |
|
396 | 395 |
let ind = |
397 |
{ ind with nodei_spec = Some (NodeSpec (node_name new_nd, Some new_c)) }
|
|
396 |
{ ind with nodei_spec = Some (NodeSpec (node_name new_nd)) } |
|
398 | 397 |
in |
399 | 398 |
( new_nd :: accu_contracts, |
400 | 399 |
{ top with top_decl_desc = ImportedNode ind } :: accu_nodes )) |
src/corelang.ml | ||
---|---|---|
193 | 193 |
modes = []; |
194 | 194 |
imports = []; |
195 | 195 |
spec_loc = Location.dummy; |
196 |
proof = None |
|
196 | 197 |
} |
197 | 198 |
|
198 | 199 |
(* For const declaration we do as for regular lustre node. But for local flows |
... | ... | |
213 | 214 |
|
214 | 215 |
let eexpr_add_name eexpr eexpr_name = { eexpr with eexpr_name } |
215 | 216 |
|
216 |
let mk_contract_guarantees name eexpr = |
|
217 |
let mk_contract_guarantees name eexpr proof =
|
|
217 | 218 |
{ |
218 | 219 |
empty_contract with |
219 | 220 |
guarantees = [ eexpr_add_name eexpr name ]; |
220 | 221 |
spec_loc = eexpr.eexpr_loc; |
222 |
proof |
|
221 | 223 |
} |
222 | 224 |
|
223 | 225 |
let mk_contract_assume name eexpr = |
... | ... | |
242 | 244 |
spec_loc = loc; |
243 | 245 |
} |
244 | 246 |
|
247 |
let merge_proofs p1 p2 = |
|
248 |
let merge_proofs p1 p2 = match p1, p2 with |
|
249 |
| Kinduction k1, Kinduction k2 -> |
|
250 |
Kinduction (max k1 k2) |
|
251 |
in |
|
252 |
match p1, p2 with |
|
253 |
| Some p1, Some p2 -> Some (merge_proofs p1 p2) |
|
254 |
| Some p, None | None, Some p -> Some p |
|
255 |
| None, None -> None |
|
256 |
|
|
245 | 257 |
let merge_contracts ann1 ann2 = |
246 | 258 |
(* keeping the first item loc *) |
247 | 259 |
{ |
... | ... | |
253 | 265 |
modes = ann1.modes @ ann2.modes; |
254 | 266 |
imports = ann1.imports @ ann2.imports; |
255 | 267 |
spec_loc = ann1.spec_loc; |
268 |
proof = merge_proofs ann1.proof ann2.proof |
|
256 | 269 |
} |
257 | 270 |
|
258 | 271 |
let mkeexpr loc expr = |
... | ... | |
1105 | 1118 |
option_map |
1106 | 1119 |
(fun s -> |
1107 | 1120 |
match s with |
1108 |
| NodeSpec (id, oc) ->
|
|
1109 |
NodeSpec (f_node id, option_map (rename_contract f_var f_node) oc)
|
|
1121 |
| NodeSpec id ->
|
|
1122 |
NodeSpec (f_node id) |
|
1110 | 1123 |
| Contract c -> |
1111 | 1124 |
Contract (rename_contract f_var f_node c)) |
1112 | 1125 |
nd.node_spec |
src/corelang.mli | ||
---|---|---|
271 | 271 |
val mk_contract_var : |
272 | 272 |
ident -> bool -> type_dec option -> expr -> Location.t -> contract_desc |
273 | 273 |
|
274 |
val mk_contract_guarantees : string option -> eexpr -> contract_desc |
|
274 |
val mk_contract_guarantees : string option -> eexpr -> proof_annotation option -> contract_desc
|
|
275 | 275 |
|
276 | 276 |
val mk_contract_assume : string option -> eexpr -> contract_desc |
277 | 277 |
|
src/lustre_types.ml | ||
---|---|---|
151 | 151 |
hand_loc : Location.t; |
152 | 152 |
} |
153 | 153 |
|
154 |
type proof_annotation = Kinduction of int |
|
155 |
|
|
154 | 156 |
type contract_desc = { |
155 | 157 |
consts : var_decl list; |
156 | 158 |
locals : var_decl list; |
... | ... | |
160 | 162 |
modes : contract_mode list; |
161 | 163 |
imports : contract_import list; |
162 | 164 |
spec_loc : Location.t; |
165 |
proof : proof_annotation option |
|
163 | 166 |
} |
164 | 167 |
|
165 |
type 'a node_spec_t = Contract of 'a | NodeSpec of ident * 'a option
|
|
168 |
type 'a node_spec_t = Contract of 'a | NodeSpec of ident |
|
166 | 169 |
|
167 | 170 |
type node_desc = { |
168 | 171 |
node_id : ident; |
src/lustre_types.mli | ||
---|---|---|
140 | 140 |
hand_loc : Location.t; |
141 | 141 |
} |
142 | 142 |
|
143 |
type proof_annotation = Kinduction of int |
|
144 |
|
|
143 | 145 |
type contract_desc = { |
144 | 146 |
consts : var_decl list; |
145 | 147 |
locals : var_decl list; |
... | ... | |
149 | 151 |
modes : contract_mode list; |
150 | 152 |
imports : contract_import list; |
151 | 153 |
spec_loc : Location.t; |
154 |
proof : proof_annotation option |
|
152 | 155 |
} |
153 | 156 |
|
154 |
type 'a node_spec_t = Contract of 'a | NodeSpec of ident * 'a option
|
|
157 |
type 'a node_spec_t = Contract of 'a | NodeSpec of ident |
|
155 | 158 |
|
156 | 159 |
type node_desc = { |
157 | 160 |
node_id : ident; |
src/machine_code.ml | ||
---|---|---|
43 | 43 |
is_local = (fun id -> List.exists (fun v -> v.var_id = id) locals); |
44 | 44 |
get_var = |
45 | 45 |
(fun id -> |
46 |
try List.find (fun v -> v.var_id = id) all |
|
47 |
with Not_found -> |
|
46 |
try List.find (fun v -> v.var_id = id) all
|
|
47 |
with Not_found ->
|
|
48 | 48 |
(* Format.eprintf "Impossible to find variable %s in set %a@.@?" * id |
49 | 49 |
* VSet.pp all; *) |
50 | 50 |
raise Not_found); |
... | ... | |
373 | 373 |
else mkinstr (MSetReset inst) :: ctx.si); |
374 | 374 |
} |
375 | 375 |
| [ x ], _ -> |
376 |
begin try |
|
376 | 377 |
let var_x = env.get_var x in |
377 | 378 |
let instr, spec = translate_act (var_x, eq.eq_rhs) in |
378 | 379 |
control_on_clock eq.eq_rhs.expr_clock instr True spec ctx |
380 |
with Not_found -> |
|
381 |
Format.eprintf "ERROR: node %s, eq %a@." id Printers.pp_node_eq eq ; |
|
382 |
raise Not_found |
|
383 |
end |
|
379 | 384 |
| _ -> |
380 | 385 |
Format.eprintf |
381 | 386 |
"internal error: Machine_code.translate_eq %a@?" |
... | ... | |
484 | 489 |
tname = nd; |
485 | 490 |
tindex = Some 0; |
486 | 491 |
tvars = nd.node_inputs; |
487 |
tformula = True;
|
|
492 |
tformula = if fst (get_stateless_status_node nd) then True else StateVarPack ResetFlag;
|
|
488 | 493 |
tmem_footprint = ISet.empty; |
489 | 494 |
tinst_footprint = IMap.empty; |
490 | 495 |
} |
... | ... | |
508 | 513 |
} |
509 | 514 |
|
510 | 515 |
let translate_eexpr env e = |
516 |
try |
|
511 | 517 |
List.fold_right (fun (qt, xs) f -> match qt with |
512 | 518 |
| Lustre_types.Exists -> Exists (xs, f) |
513 | 519 |
| Lustre_types.Forall -> Forall (xs, f)) |
514 | 520 |
e.eexpr_quantifiers |
515 | 521 |
(Value (translate_expr env e.eexpr_qfexpr)) |
522 |
with |
|
523 |
NormalizationError -> |
|
524 |
Format.eprintf |
|
525 |
"Normalization error: %a@." |
|
526 |
Printers.pp_eexpr |
|
527 |
e; |
|
528 |
raise NormalizationError |
|
529 |
|
|
516 | 530 |
|
517 | 531 |
let translate_contract env c = { |
518 | 532 |
mc_pre = And (List.map (translate_eexpr env) c.Lustre_types.assume); |
519 |
mc_post = And (List.map (translate_eexpr env) c.Lustre_types.guarantees) |
|
533 |
mc_post = And (List.map (translate_eexpr env) c.Lustre_types.guarantees); |
|
534 |
mc_proof = c.proof |
|
520 | 535 |
} |
521 | 536 |
|
522 | 537 |
let translate_spec env = function |
523 | 538 |
| Contract c -> |
524 | 539 |
Contract (translate_contract env c) |
525 |
| NodeSpec (s, c) ->
|
|
526 |
NodeSpec (s, option_map (translate_contract env) c)
|
|
540 |
| NodeSpec s ->
|
|
541 |
NodeSpec s
|
|
527 | 542 |
|
528 | 543 |
let translate_decl nd sch = |
529 | 544 |
(* Format.eprintf "Translating node %s@." nd.node_id; *) |
src/machine_code_common.ml | ||
---|---|---|
339 | 339 |
match m.mspec.mnode_spec with |
340 | 340 |
| None -> |
341 | 341 |
() |
342 |
| Some (NodeSpec (id, c)) -> |
|
343 |
fprintf fmt "cocospec: %s@;%a" id |
|
344 |
(pp_print_option (pp_mspec m)) c |
|
342 |
| Some (NodeSpec id) -> |
|
343 |
fprintf fmt "cocospec: %s" id |
|
345 | 344 |
| Some (Contract spec) -> |
346 | 345 |
pp_mspec m fmt spec) |
347 | 346 |
(pp_memory_packs m) |
src/machine_code_types.mli | ||
---|---|---|
60 | 60 |
type mc_contract_t = { |
61 | 61 |
mc_pre: mc_formula_t; |
62 | 62 |
mc_post: mc_formula_t; |
63 |
mc_proof: proof_annotation option |
|
63 | 64 |
} |
64 | 65 |
|
65 | 66 |
type machine_spec = { |
src/normalization.ml | ||
---|---|---|
753 | 753 |
Careful: we do not normalize annotations, since they can have the form |
754 | 754 |
x = (a, b, c) *) |
755 | 755 |
match node.node_spec with |
756 |
| None | Some (NodeSpec _) -> node.node_spec, [], [], eqs |
|
756 |
| None | Some (NodeSpec _) -> |
|
757 |
node.node_spec, [], [], eqs |
|
757 | 758 |
| Some (Contract s) -> |
758 |
let new_locals, new_outs, new_stmts, s' =
|
|
759 |
normalize_spec node.node_id
|
|
760 |
(node.node_inputs, node.node_outputs, node.node_locals)
|
|
761 |
s
|
|
762 |
in
|
|
763 |
(* Format.eprintf "Normalization bounded new locals: %a@." Printers.pp_vars new_locals;
|
|
764 |
* Format.eprintf "Normalization bounded stmts: %a@." Printers.pp_node_eqs new_stmts; *)
|
|
765 |
Some (Contract s'), new_locals, new_outs, new_stmts @ eqs
|
|
759 |
let new_locals, new_outs, new_stmts, s' = |
|
760 |
normalize_spec node.node_id |
|
761 |
(node.node_inputs, node.node_outputs, node.node_locals) |
|
762 |
s |
|
763 |
in |
|
764 |
(* Format.eprintf "Normalization bounded new locals: %a@." Printers.pp_vars new_locals; |
|
765 |
* Format.eprintf "Normalization bounded stmts: %a@." Printers.pp_node_eqs new_stmts; *) |
|
766 |
Some (Contract s'), new_locals, new_outs, new_stmts @ eqs |
|
766 | 767 |
in |
767 | 768 |
let defs, vars = |
768 | 769 |
List.fold_left (normalize_eq norm_ctx) ([], new_vars @ orig_vars) eqs |
src/parsers/lexerLustreSpec.mll | ||
---|---|---|
93 | 93 |
"forall", FORALL; |
94 | 94 |
"c_code", CCODE; |
95 | 95 |
"matlab", MATLAB; |
96 |
"by", BY |
|
96 | 97 |
] |
97 | 98 |
|
98 | 99 |
} |
... | ... | |
113 | 114 |
{REAL (Real.create (l^r) (String.length r + -1 * int_of_string exp) s)} |
114 | 115 |
| '-'? ['0'-'9']+ |
115 | 116 |
{INT (int_of_string (Lexing.lexeme lexbuf)) } |
117 |
| (['0'-'9']+) as i '-' "induction" |
|
118 |
{KINDUCTION (int_of_string i)} |
|
116 | 119 |
(* | '/' (['_' 'A'-'Z' 'a'-'z'] ['A'-'Z' 'a'-'z' '_' '0'-'9']* '/')+ as s |
117 | 120 |
{IDENT s} |
118 | 121 |
*) |
src/parsers/parser_lustre.messages | ||
---|---|---|
1 | 1 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR LET ANNOT XOR |
2 | 2 |
## |
3 |
## Ends in an error in state: 527.
|
|
3 |
## Ends in an error in state: 532.
|
|
4 | 4 |
## |
5 | 5 |
## stmt_list -> ANNOT . stmt_list [ TEL ] |
6 | 6 |
## |
... | ... | |
9 | 9 |
## |
10 | 10 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR LET ASSERT UIDENT SCOL XOR |
11 | 11 |
## |
12 |
## Ends in an error in state: 537.
|
|
12 |
## Ends in an error in state: 542.
|
|
13 | 13 |
## |
14 | 14 |
## stmt_list -> assert_ . stmt_list [ TEL ] |
15 | 15 |
## |
... | ... | |
18 | 18 |
## |
19 | 19 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR LET XOR |
20 | 20 |
## |
21 |
## Ends in an error in state: 501.
|
|
21 |
## Ends in an error in state: 506.
|
|
22 | 22 |
## |
23 | 23 |
## top_decl -> state_annot node_ident_decl LPAR var_decl_list(vdecl) RPAR RETURNS LPAR var_decl_list(vdecl) RPAR option(SCOL) nodespecs loption(preceded(VAR,var_decl_list(local_vdecl))) LET . stmt_list TEL [ NODESPEC NODE FUNCTION EOF CONST ] |
24 | 24 |
## |
... | ... | |
27 | 27 |
## |
28 | 28 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR LET AUTOMATON IDENT STATE UIDENT COL LET XOR |
29 | 29 |
## |
30 |
## Ends in an error in state: 523.
|
|
30 |
## Ends in an error in state: 528.
|
|
31 | 31 |
## |
32 | 32 |
## handler -> STATE UIDENT COL list(unless) loption(preceded(VAR,var_decl_list(local_vdecl))) LET . stmt_list TEL list(until) [ UIDENT TEL STATE LPAR IDENT AUTOMATON ASSERT ANNOT ] |
33 | 33 |
## |
... | ... | |
36 | 36 |
## |
37 | 37 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR LET UIDENT EQ FALSE SCOL XOR |
38 | 38 |
## |
39 |
## Ends in an error in state: 533.
|
|
39 |
## Ends in an error in state: 538.
|
|
40 | 40 |
## |
41 | 41 |
## stmt_list -> eq . stmt_list [ TEL ] |
42 | 42 |
## |
... | ... | |
48 | 48 |
|
49 | 49 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR LET ASSERT XOR |
50 | 50 |
## |
51 |
## Ends in an error in state: 524.
|
|
51 |
## Ends in an error in state: 529.
|
|
52 | 52 |
## |
53 | 53 |
## assert_ -> ASSERT . expr SCOL [ UIDENT TEL LPAR IDENT AUTOMATON ASSERT ANNOT ] |
54 | 54 |
## |
... | ... | |
61 | 61 |
|
62 | 62 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR LET AUTOMATON IDENT STATE UIDENT COL LET TEL UNTIL UIDENT RESTART UIDENT XOR |
63 | 63 |
## |
64 |
## Ends in an error in state: 547.
|
|
64 |
## Ends in an error in state: 552.
|
|
65 | 65 |
## |
66 | 66 |
## list(until) -> until . list(until) [ UIDENT TEL STATE LPAR IDENT AUTOMATON ASSERT ANNOT ] |
67 | 67 |
## |
... | ... | |
70 | 70 |
## |
71 | 71 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR LET AUTOMATON IDENT STATE UIDENT COL LET TEL XOR |
72 | 72 |
## |
73 |
## Ends in an error in state: 540.
|
|
73 |
## Ends in an error in state: 545.
|
|
74 | 74 |
## |
75 | 75 |
## handler -> STATE UIDENT COL list(unless) loption(preceded(VAR,var_decl_list(local_vdecl))) LET stmt_list TEL . list(until) [ UIDENT TEL STATE LPAR IDENT AUTOMATON ASSERT ANNOT ] |
76 | 76 |
## |
... | ... | |
83 | 83 |
|
84 | 84 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR LET AUTOMATON IDENT STATE UIDENT COL LET TEL UNTIL UIDENT RESTART XOR |
85 | 85 |
## |
86 |
## Ends in an error in state: 545.
|
|
86 |
## Ends in an error in state: 550.
|
|
87 | 87 |
## |
88 | 88 |
## until -> UNTIL expr RESTART . UIDENT [ UNTIL UIDENT TEL STATE LPAR IDENT AUTOMATON ASSERT ANNOT ] |
89 | 89 |
## |
... | ... | |
92 | 92 |
## |
93 | 93 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR LET AUTOMATON IDENT STATE UIDENT COL LET TEL UNTIL UIDENT RESUME XOR |
94 | 94 |
## |
95 |
## Ends in an error in state: 543.
|
|
95 |
## Ends in an error in state: 548.
|
|
96 | 96 |
## |
97 | 97 |
## until -> UNTIL expr RESUME . UIDENT [ UNTIL UIDENT TEL STATE LPAR IDENT AUTOMATON ASSERT ANNOT ] |
98 | 98 |
## |
... | ... | |
101 | 101 |
## |
102 | 102 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR LET AUTOMATON IDENT STATE XOR |
103 | 103 |
## |
104 |
## Ends in an error in state: 510.
|
|
104 |
## Ends in an error in state: 515.
|
|
105 | 105 |
## |
106 | 106 |
## handler -> STATE . UIDENT COL list(unless) loption(preceded(VAR,var_decl_list(local_vdecl))) LET stmt_list TEL list(until) [ UIDENT TEL STATE LPAR IDENT AUTOMATON ASSERT ANNOT ] |
107 | 107 |
## |
... | ... | |
110 | 110 |
## |
111 | 111 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR LET AUTOMATON IDENT STATE UIDENT COL UNLESS UIDENT RESTART XOR |
112 | 112 |
## |
113 |
## Ends in an error in state: 517.
|
|
113 |
## Ends in an error in state: 522.
|
|
114 | 114 |
## |
115 | 115 |
## unless -> UNLESS expr RESTART . UIDENT [ VAR UNLESS LET ] |
116 | 116 |
## |
... | ... | |
119 | 119 |
## |
120 | 120 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR LET AUTOMATON IDENT STATE UIDENT COL UNLESS UIDENT RESUME XOR |
121 | 121 |
## |
122 |
## Ends in an error in state: 515.
|
|
122 |
## Ends in an error in state: 520.
|
|
123 | 123 |
## |
124 | 124 |
## unless -> UNLESS expr RESUME . UIDENT [ VAR UNLESS LET ] |
125 | 125 |
## |
... | ... | |
128 | 128 |
## |
129 | 129 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR LET AUTOMATON IDENT STATE UIDENT XOR |
130 | 130 |
## |
131 |
## Ends in an error in state: 511.
|
|
131 |
## Ends in an error in state: 516.
|
|
132 | 132 |
## |
133 | 133 |
## handler -> STATE UIDENT . COL list(unless) loption(preceded(VAR,var_decl_list(local_vdecl))) LET stmt_list TEL list(until) [ UIDENT TEL STATE LPAR IDENT AUTOMATON ASSERT ANNOT ] |
134 | 134 |
## |
... | ... | |
140 | 140 |
|
141 | 141 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR LET AUTOMATON IDENT STATE UIDENT COL LET TEL UNTIL XOR |
142 | 142 |
## |
143 |
## Ends in an error in state: 541.
|
|
143 |
## Ends in an error in state: 546.
|
|
144 | 144 |
## |
145 | 145 |
## until -> UNTIL . expr RESTART UIDENT [ UNTIL UIDENT TEL STATE LPAR IDENT AUTOMATON ASSERT ANNOT ] |
146 | 146 |
## until -> UNTIL . expr RESUME UIDENT [ UNTIL UIDENT TEL STATE LPAR IDENT AUTOMATON ASSERT ANNOT ] |
... | ... | |
154 | 154 |
|
155 | 155 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR LET AUTOMATON IDENT STATE UIDENT COL UNLESS UIDENT RESTART UIDENT XOR |
156 | 156 |
## |
157 |
## Ends in an error in state: 519.
|
|
157 |
## Ends in an error in state: 524.
|
|
158 | 158 |
## |
159 | 159 |
## list(unless) -> unless . list(unless) [ VAR LET ] |
160 | 160 |
## |
... | ... | |
167 | 167 |
|
168 | 168 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR LET AUTOMATON IDENT STATE UIDENT COL UNLESS XOR |
169 | 169 |
## |
170 |
## Ends in an error in state: 513.
|
|
170 |
## Ends in an error in state: 518.
|
|
171 | 171 |
## |
172 | 172 |
## unless -> UNLESS . expr RESTART UIDENT [ VAR UNLESS LET ] |
173 | 173 |
## unless -> UNLESS . expr RESUME UIDENT [ VAR UNLESS LET ] |
... | ... | |
181 | 181 |
|
182 | 182 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR LET AUTOMATON IDENT STATE UIDENT COL XOR |
183 | 183 |
## |
184 |
## Ends in an error in state: 512.
|
|
184 |
## Ends in an error in state: 517.
|
|
185 | 185 |
## |
186 | 186 |
## handler -> STATE UIDENT COL . list(unless) loption(preceded(VAR,var_decl_list(local_vdecl))) LET stmt_list TEL list(until) [ UIDENT TEL STATE LPAR IDENT AUTOMATON ASSERT ANNOT ] |
187 | 187 |
## |
... | ... | |
194 | 194 |
|
195 | 195 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR LET AUTOMATON IDENT XOR |
196 | 196 |
## |
197 |
## Ends in an error in state: 509.
|
|
197 |
## Ends in an error in state: 514.
|
|
198 | 198 |
## |
199 | 199 |
## automaton -> AUTOMATON type_ident . list(handler) [ UIDENT TEL LPAR IDENT AUTOMATON ASSERT ANNOT ] |
200 | 200 |
## |
... | ... | |
203 | 203 |
## |
204 | 204 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR LET AUTOMATON XOR |
205 | 205 |
## |
206 |
## Ends in an error in state: 508.
|
|
206 |
## Ends in an error in state: 513.
|
|
207 | 207 |
## |
208 | 208 |
## automaton -> AUTOMATON . type_ident list(handler) [ UIDENT TEL LPAR IDENT AUTOMATON ASSERT ANNOT ] |
209 | 209 |
## |
... | ... | |
215 | 215 |
|
216 | 216 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR LET LPAR UIDENT RPAR EQ XOR |
217 | 217 |
## |
218 |
## Ends in an error in state: 505.
|
|
218 |
## Ends in an error in state: 510.
|
|
219 | 219 |
## |
220 | 220 |
## eq -> LPAR separated_nonempty_list(COMMA,vdecl_ident) RPAR EQ . expr SCOL [ UIDENT TEL LPAR IDENT AUTOMATON ASSERT ANNOT ] |
221 | 221 |
## |
... | ... | |
224 | 224 |
## |
225 | 225 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR LET UIDENT EQ XOR |
226 | 226 |
## |
227 |
## Ends in an error in state: 530.
|
|
227 |
## Ends in an error in state: 535.
|
|
228 | 228 |
## |
229 | 229 |
## eq -> separated_nonempty_list(COMMA,vdecl_ident) EQ . expr SCOL [ UIDENT TEL LPAR IDENT AUTOMATON ASSERT ANNOT ] |
230 | 230 |
## |
... | ... | |
237 | 237 |
|
238 | 238 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR LET LPAR UIDENT RPAR XOR |
239 | 239 |
## |
240 |
## Ends in an error in state: 504.
|
|
240 |
## Ends in an error in state: 509.
|
|
241 | 241 |
## |
242 | 242 |
## eq -> LPAR separated_nonempty_list(COMMA,vdecl_ident) RPAR . EQ expr SCOL [ UIDENT TEL LPAR IDENT AUTOMATON ASSERT ANNOT ] |
243 | 243 |
## |
... | ... | |
246 | 246 |
## |
247 | 247 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR LET UIDENT SCOL |
248 | 248 |
## |
249 |
## Ends in an error in state: 529.
|
|
249 |
## Ends in an error in state: 534.
|
|
250 | 250 |
## |
251 | 251 |
## eq -> separated_nonempty_list(COMMA,vdecl_ident) . EQ expr SCOL [ UIDENT TEL LPAR IDENT AUTOMATON ASSERT ANNOT ] |
252 | 252 |
## |
... | ... | |
265 | 265 |
|
266 | 266 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR LET LPAR UIDENT SCOL |
267 | 267 |
## |
268 |
## Ends in an error in state: 503.
|
|
268 |
## Ends in an error in state: 508.
|
|
269 | 269 |
## |
270 | 270 |
## eq -> LPAR separated_nonempty_list(COMMA,vdecl_ident) . RPAR EQ expr SCOL [ UIDENT TEL LPAR IDENT AUTOMATON ASSERT ANNOT ] |
271 | 271 |
## |
... | ... | |
280 | 280 |
## |
281 | 281 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR LET LPAR XOR |
282 | 282 |
## |
283 |
## Ends in an error in state: 502.
|
|
283 |
## Ends in an error in state: 507.
|
|
284 | 284 |
## |
285 | 285 |
## eq -> LPAR . separated_nonempty_list(COMMA,vdecl_ident) RPAR EQ expr SCOL [ UIDENT TEL LPAR IDENT AUTOMATON ASSERT ANNOT ] |
286 | 286 |
## |
... | ... | |
293 | 293 |
|
294 | 294 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR NODESPEC FUNCTION |
295 | 295 |
## |
296 |
## Ends in an error in state: 485.
|
|
296 |
## Ends in an error in state: 490.
|
|
297 | 297 |
## |
298 | 298 |
## top_decl -> state_annot node_ident_decl LPAR var_decl_list(vdecl) RPAR RETURNS LPAR var_decl_list(vdecl) RPAR option(SCOL) nodespecs . loption(preceded(VAR,var_decl_list(local_vdecl))) LET stmt_list TEL [ NODESPEC NODE FUNCTION EOF CONST ] |
299 | 299 |
## |
... | ... | |
306 | 306 |
## may provide an INCOMPLETE view of the future (what was expected next). |
307 | 307 |
## In state 118, spurious reduction of production nodespec_list -> |
308 | 308 |
## In state 119, spurious reduction of production nodespec_list -> NODESPEC nodespec_list |
309 |
## In state 420, spurious reduction of production nodespecs -> nodespec_list
|
|
309 |
## In state 425, spurious reduction of production nodespecs -> nodespec_list
|
|
310 | 310 |
## |
311 | 311 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR XOR |
312 | 312 |
## |
313 |
## Ends in an error in state: 483.
|
|
313 |
## Ends in an error in state: 488.
|
|
314 | 314 |
## |
315 | 315 |
## top_decl -> state_annot node_ident_decl LPAR var_decl_list(vdecl) RPAR RETURNS LPAR var_decl_list(vdecl) RPAR . option(SCOL) nodespecs loption(preceded(VAR,var_decl_list(local_vdecl))) LET stmt_list TEL [ NODESPEC NODE FUNCTION EOF CONST ] |
316 | 316 |
## |
... | ... | |
319 | 319 |
## |
320 | 320 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR SCOL LCUR |
321 | 321 |
## |
322 |
## Ends in an error in state: 484.
|
|
322 |
## Ends in an error in state: 489.
|
|
323 | 323 |
## |
324 | 324 |
## top_decl -> state_annot node_ident_decl LPAR var_decl_list(vdecl) RPAR RETURNS LPAR var_decl_list(vdecl) RPAR option(SCOL) . nodespecs loption(preceded(VAR,var_decl_list(local_vdecl))) LET stmt_list TEL [ NODESPEC NODE FUNCTION EOF CONST ] |
325 | 325 |
## |
... | ... | |
331 | 331 |
|
332 | 332 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR VAR CONST UIDENT COL IDENT WHENNOT |
333 | 333 |
## |
334 |
## Ends in an error in state: 489.
|
|
334 |
## Ends in an error in state: 494.
|
|
335 | 335 |
## |
336 | 336 |
## local_vdecl -> CONST vdecl_ident option(preceded(COL,typeconst)) . EQ expr [ SCOL LET ] |
337 | 337 |
## |
... | ... | |
348 | 348 |
## |
349 | 349 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR VAR CONST UIDENT EQ XOR |
350 | 350 |
## |
351 |
## Ends in an error in state: 490.
|
|
351 |
## Ends in an error in state: 495.
|
|
352 | 352 |
## |
353 | 353 |
## local_vdecl -> CONST vdecl_ident option(preceded(COL,typeconst)) EQ . expr [ SCOL LET ] |
354 | 354 |
## |
... | ... | |
357 | 357 |
## |
358 | 358 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR VAR CONST UIDENT XOR |
359 | 359 |
## |
360 |
## Ends in an error in state: 488.
|
|
360 |
## Ends in an error in state: 493.
|
|
361 | 361 |
## |
362 | 362 |
## local_vdecl -> CONST vdecl_ident . option(preceded(COL,typeconst)) EQ expr [ SCOL LET ] |
363 | 363 |
## |
... | ... | |
370 | 370 |
|
371 | 371 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR VAR CONST XOR |
372 | 372 |
## |
373 |
## Ends in an error in state: 487.
|
|
373 |
## Ends in an error in state: 492.
|
|
374 | 374 |
## |
375 | 375 |
## local_vdecl -> CONST . vdecl_ident option(preceded(COL,typeconst)) EQ expr [ SCOL LET ] |
376 | 376 |
## |
... | ... | |
383 | 383 |
|
384 | 384 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR VAR UIDENT COL IDENT WHENNOT IDENT RPAR |
385 | 385 |
## |
386 |
## Ends in an error in state: 497.
|
|
386 |
## Ends in an error in state: 502.
|
|
387 | 387 |
## |
388 | 388 |
## var_decl_list(local_vdecl) -> local_vdecl . [ LET ] |
389 | 389 |
## var_decl_list(local_vdecl) -> local_vdecl . SCOL [ LET ] |
... | ... | |
398 | 398 |
## may provide an INCOMPLETE view of the future (what was expected next). |
399 | 399 |
## In state 150, spurious reduction of production nonempty_list(when_cond) -> when_cond |
400 | 400 |
## In state 153, spurious reduction of production option(clock) -> nonempty_list(when_cond) |
401 |
## In state 496, spurious reduction of production local_vdecl -> separated_nonempty_list(COMMA,vdecl_ident) COL typeconst option(clock)
|
|
401 |
## In state 501, spurious reduction of production local_vdecl -> separated_nonempty_list(COMMA,vdecl_ident) COL typeconst option(clock)
|
|
402 | 402 |
## |
403 | 403 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR VAR UIDENT COL TREAL RPAR |
404 | 404 |
## |
405 |
## Ends in an error in state: 495.
|
|
405 |
## Ends in an error in state: 500.
|
|
406 | 406 |
## |
407 | 407 |
## local_vdecl -> separated_nonempty_list(COMMA,vdecl_ident) COL typeconst . option(clock) [ SCOL LET ] |
408 | 408 |
## |
... | ... | |
417 | 417 |
## |
418 | 418 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR VAR UIDENT RPAR |
419 | 419 |
## |
420 |
## Ends in an error in state: 493.
|
|
420 |
## Ends in an error in state: 498.
|
|
421 | 421 |
## |
422 | 422 |
## local_vdecl -> separated_nonempty_list(COMMA,vdecl_ident) . [ SCOL LET ] |
423 | 423 |
## local_vdecl -> separated_nonempty_list(COMMA,vdecl_ident) . COL typeconst option(clock) [ SCOL LET ] |
... | ... | |
433 | 433 |
## |
434 | 434 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR VAR UIDENT SCOL XOR |
435 | 435 |
## |
436 |
## Ends in an error in state: 498.
|
|
436 |
## Ends in an error in state: 503.
|
|
437 | 437 |
## |
438 | 438 |
## var_decl_list(local_vdecl) -> local_vdecl SCOL . [ LET ] |
439 | 439 |
## var_decl_list(local_vdecl) -> local_vdecl SCOL . var_decl_list(local_vdecl) [ LET ] |
... | ... | |
443 | 443 |
## |
444 | 444 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR VAR XOR |
445 | 445 |
## |
446 |
## Ends in an error in state: 486.
|
|
446 |
## Ends in an error in state: 491.
|
|
447 | 447 |
## |
448 | 448 |
## loption(preceded(VAR,var_decl_list(local_vdecl))) -> VAR . var_decl_list(local_vdecl) [ LET ] |
449 | 449 |
## |
... | ... | |
456 | 456 |
|
457 | 457 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR CONST IDENT RPAR VAR UIDENT COL XOR |
458 | 458 |
## |
459 |
## Ends in an error in state: 494.
|
|
459 |
## Ends in an error in state: 499.
|
|
460 | 460 |
## |
461 | 461 |
## local_vdecl -> separated_nonempty_list(COMMA,vdecl_ident) COL . typeconst option(clock) [ SCOL LET ] |
462 | 462 |
## |
... | ... | |
506 | 506 |
|
507 | 507 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS LPAR XOR |
508 | 508 |
## |
509 |
## Ends in an error in state: 481.
|
|
509 |
## Ends in an error in state: 486.
|
|
510 | 510 |
## |
511 | 511 |
## top_decl -> state_annot node_ident_decl LPAR var_decl_list(vdecl) RPAR RETURNS LPAR . var_decl_list(vdecl) RPAR option(SCOL) nodespecs loption(preceded(VAR,var_decl_list(local_vdecl))) LET stmt_list TEL [ NODESPEC NODE FUNCTION EOF CONST ] |
512 | 512 |
## |
... | ... | |
515 | 515 |
## |
516 | 516 |
prog: NODE UIDENT LPAR XOR |
517 | 517 |
## |
518 |
## Ends in an error in state: 477.
|
|
518 |
## Ends in an error in state: 482.
|
|
519 | 519 |
## |
520 | 520 |
## top_decl -> state_annot node_ident_decl LPAR . var_decl_list(vdecl) RPAR RETURNS LPAR var_decl_list(vdecl) RPAR option(SCOL) nodespecs loption(preceded(VAR,var_decl_list(local_vdecl))) LET stmt_list TEL [ NODESPEC NODE FUNCTION EOF CONST ] |
521 | 521 |
## |
... | ... | |
575 | 575 |
|
576 | 576 |
prog: NODE UIDENT LPAR CONST IDENT RPAR XOR |
577 | 577 |
## |
578 |
## Ends in an error in state: 479.
|
|
578 |
## Ends in an error in state: 484.
|
|
579 | 579 |
## |
580 | 580 |
## top_decl -> state_annot node_ident_decl LPAR var_decl_list(vdecl) RPAR . RETURNS LPAR var_decl_list(vdecl) RPAR option(SCOL) nodespecs loption(preceded(VAR,var_decl_list(local_vdecl))) LET stmt_list TEL [ NODESPEC NODE FUNCTION EOF CONST ] |
581 | 581 |
## |
... | ... | |
593 | 593 |
## |
594 | 594 |
prog: NODE UIDENT LPAR CONST IDENT RPAR RETURNS XOR |
595 | 595 |
## |
596 |
## Ends in an error in state: 480.
|
|
596 |
## Ends in an error in state: 485.
|
|
597 | 597 |
## |
598 | 598 |
## top_decl -> state_annot node_ident_decl LPAR var_decl_list(vdecl) RPAR RETURNS . LPAR var_decl_list(vdecl) RPAR option(SCOL) nodespecs loption(preceded(VAR,var_decl_list(local_vdecl))) LET stmt_list TEL [ NODESPEC NODE FUNCTION EOF CONST ] |
599 | 599 |
## |
... | ... | |
611 | 611 |
## |
612 | 612 |
header: NODE UIDENT LPAR CONST IDENT RPAR RETURNS XOR |
613 | 613 |
## |
614 |
## Ends in an error in state: 408.
|
|
614 |
## Ends in an error in state: 413.
|
|
615 | 615 |
## |
616 | 616 |
## top_decl_header -> nodespecs state_annot node_ident_decl LPAR var_decl_list(vdecl) RPAR RETURNS . LPAR var_decl_list(vdecl) RPAR option(preceded(PROTOTYPE,node_ident)) list(preceded(LIB,module_ident)) SCOL [ NODESPEC NODE FUNCTION EOF CONTRACT CONST ] |
617 | 617 |
## |
... | ... | |
620 | 620 |
## |
621 | 621 |
header: NODE UIDENT LPAR CONST IDENT RPAR XOR |
622 | 622 |
## |
623 |
## Ends in an error in state: 407.
|
|
623 |
## Ends in an error in state: 412.
|
|
624 | 624 |
## |
625 | 625 |
## top_decl_header -> nodespecs state_annot node_ident_decl LPAR var_decl_list(vdecl) RPAR . RETURNS LPAR var_decl_list(vdecl) RPAR option(preceded(PROTOTYPE,node_ident)) list(preceded(LIB,module_ident)) SCOL [ NODESPEC NODE FUNCTION EOF CONTRACT CONST ] |
626 | 626 |
## |
... | ... | |
633 | 633 |
|
634 | 634 |
prog: NODE UIDENT XOR |
635 | 635 |
## |
636 |
## Ends in an error in state: 476.
|
|
636 |
## Ends in an error in state: 481.
|
|
637 | 637 |
## |
638 | 638 |
## top_decl -> state_annot node_ident_decl . LPAR var_decl_list(vdecl) RPAR RETURNS LPAR var_decl_list(vdecl) RPAR option(SCOL) nodespecs loption(preceded(VAR,var_decl_list(local_vdecl))) LET stmt_list TEL [ NODESPEC NODE FUNCTION EOF CONST ] |
639 | 639 |
## |
... | ... | |
651 | 651 |
## |
652 | 652 |
header: NODE UIDENT XOR |
653 | 653 |
## |
654 |
## Ends in an error in state: 404.
|
|
654 |
## Ends in an error in state: 409.
|
|
655 | 655 |
## |
656 | 656 |
## top_decl_header -> nodespecs state_annot node_ident_decl . LPAR var_decl_list(vdecl) RPAR RETURNS LPAR var_decl_list(vdecl) RPAR option(preceded(PROTOTYPE,node_ident)) list(preceded(LIB,module_ident)) SCOL [ NODESPEC NODE FUNCTION EOF CONTRACT CONST ] |
657 | 657 |
## |
... | ... | |
664 | 664 |
|
665 | 665 |
prog: NODE XOR |
666 | 666 |
## |
667 |
## Ends in an error in state: 475.
|
|
667 |
## Ends in an error in state: 480.
|
|
668 | 668 |
## |
669 | 669 |
## top_decl -> state_annot . node_ident_decl LPAR var_decl_list(vdecl) RPAR RETURNS LPAR var_decl_list(vdecl) RPAR option(SCOL) nodespecs loption(preceded(VAR,var_decl_list(local_vdecl))) LET stmt_list TEL [ NODESPEC NODE FUNCTION EOF CONST ] |
670 | 670 |
## |
... | ... | |
673 | 673 |
## |
674 | 674 |
header: NODE XOR |
675 | 675 |
## |
676 |
## Ends in an error in state: 403.
|
|
676 |
## Ends in an error in state: 408.
|
|
677 | 677 |
## |
678 | 678 |
## top_decl_header -> nodespecs state_annot . node_ident_decl LPAR var_decl_list(vdecl) RPAR RETURNS LPAR var_decl_list(vdecl) RPAR option(preceded(PROTOTYPE,node_ident)) list(preceded(LIB,module_ident)) SCOL [ NODESPEC NODE FUNCTION EOF CONTRACT CONST ] |
679 | 679 |
## |
... | ... | |
685 | 685 |
|
686 | 686 |
prog: NODESPEC XOR |
687 | 687 |
## |
688 |
## Ends in an error in state: 474.
|
|
688 |
## Ends in an error in state: 479.
|
|
689 | 689 |
## |
690 | 690 |
## list(top_decl) -> top_decl . list(top_decl) [ EOF ] |
691 | 691 |
## |
... | ... | |
694 | 694 |
## |
695 | 695 |
prog: OPEN LT IDENT GT CONTRACT |
696 | 696 |
## |
697 |
## Ends in an error in state: 469.
|
|
697 |
## Ends in an error in state: 474.
|
|
698 | 698 |
## |
699 | 699 |
## prog -> prefix . list(top_decl) EOF [ # ] |
700 | 700 |
## |
... | ... | |
710 | 710 |
## |
711 | 711 |
prog: XOR |
712 | 712 |
## |
713 |
## Ends in an error in state: 467.
|
|
713 |
## Ends in an error in state: 472.
|
|
714 | 714 |
## |
715 | 715 |
## prog' -> . prog [ # ] |
716 | 716 |
## |
... | ... | |
719 | 719 |
## |
720 | 720 |
header: CONST UIDENT EQ FALSE SCOL XOR |
721 | 721 |
## |
722 |
## Ends in an error in state: 398.
|
|
722 |
## Ends in an error in state: 403.
|
|
723 | 723 |
## |
724 | 724 |
## list(top_decl_header) -> top_decl_header . list(top_decl_header) [ EOF ] |
725 | 725 |
## |
... | ... | |
728 | 728 |
## |
729 | 729 |
header: NODESPEC VAR |
730 | 730 |
## |
731 |
## Ends in an error in state: 400.
|
|
731 |
## Ends in an error in state: 405.
|
|
732 | 732 |
## |
733 | 733 |
## top_decl_header -> nodespecs . state_annot node_ident_decl LPAR var_decl_list(vdecl) RPAR RETURNS LPAR var_decl_list(vdecl) RPAR option(preceded(PROTOTYPE,node_ident)) list(preceded(LIB,module_ident)) SCOL [ NODESPEC NODE FUNCTION EOF CONTRACT CONST ] |
734 | 734 |
## |
... | ... | |
741 | 741 |
## may provide an INCOMPLETE view of the future (what was expected next). |
742 | 742 |
## In state 118, spurious reduction of production nodespec_list -> |
743 | 743 |
## In state 119, spurious reduction of production nodespec_list -> NODESPEC nodespec_list |
744 |
## In state 420, spurious reduction of production nodespecs -> nodespec_list
|
|
744 |
## In state 425, spurious reduction of production nodespecs -> nodespec_list
|
|
745 | 745 |
## |
746 | 746 |
header: NODESPEC XOR |
747 | 747 |
## |
... | ... | |
775 | 775 |
|
776 | 776 |
lustre_spec: ASSUME STRING UIDENT SCOL XOR |
777 | 777 |
## |
778 |
## Ends in an error in state: 334.
|
|
778 |
## Ends in an error in state: 338.
|
|
779 | 779 |
## |
780 | 780 |
## contract_content -> ASSUME STRING qexpr SCOL . contract_content [ TEL EOF ] |
781 | 781 |
## |
... | ... | |
784 | 784 |
## |
785 | 785 |
lustre_spec: ASSUME UIDENT SCOL XOR |
786 | 786 |
## |
787 |
## Ends in an error in state: 337.
|
|
787 |
## Ends in an error in state: 341.
|
|
788 | 788 |
## |
789 | 789 |
## contract_content -> ASSUME qexpr SCOL . contract_content [ TEL EOF ] |
790 | 790 |
## |
... | ... | |
794 | 794 |
|
795 | 795 |
Contract content expected. |
796 | 796 |
|
797 |
lustre_spec: ASSUME STRING UIDENT BY |
|
798 |
## |
|
799 |
## Ends in an error in state: 337. |
|
800 |
## |
|
801 |
## contract_content -> ASSUME STRING qexpr . SCOL contract_content [ TEL EOF ] |
|
802 |
## |
|
803 |
## The known suffix of the stack is as follows: |
|
804 |
## ASSUME STRING qexpr |
|
805 |
## |
|
806 |
## WARNING: This example involves spurious reductions. |
|
807 |
## This implies that, although the LR(1) items shown above provide an |
|
808 |
## accurate view of the past (what has been recognized so far), they |
|
809 |
## may provide an INCOMPLETE view of the future (what was expected next). |
|
810 |
## In state 168, spurious reduction of production expr -> UIDENT |
|
811 |
## In state 292, spurious reduction of production qexpr -> expr |
|
812 |
## |
|
813 |
lustre_spec: ASSUME UIDENT BY |
|
814 |
## |
|
815 |
## Ends in an error in state: 340. |
|
816 |
## |
|
817 |
## contract_content -> ASSUME qexpr . SCOL contract_content [ TEL EOF ] |
|
818 |
## |
|
819 |
## The known suffix of the stack is as follows: |
|
820 |
## ASSUME qexpr |
|
821 |
## |
|
822 |
## WARNING: This example involves spurious reductions. |
|
823 |
## This implies that, although the LR(1) items shown above provide an |
|
824 |
## accurate view of the past (what has been recognized so far), they |
|
825 |
## may provide an INCOMPLETE view of the future (what was expected next). |
|
826 |
## In state 168, spurious reduction of production expr -> UIDENT |
|
827 |
## In state 292, spurious reduction of production qexpr -> expr |
|
828 |
## |
|
797 | 829 |
lustre_spec: ASSUME STRING VAR |
798 | 830 |
## |
799 |
## Ends in an error in state: 332.
|
|
831 |
## Ends in an error in state: 336.
|
|
800 | 832 |
## |
801 | 833 |
## contract_content -> ASSUME STRING . qexpr SCOL contract_content [ TEL EOF ] |
802 | 834 |
## expr -> STRING . [ XOR WHENNOT WHEN SCOL POWER PLUS OR NEQ MULT MOD MINUS LTE LT LBRACKET IMPL GTE GT FBY EQ DIV BARBAR ARROW AND AMPERAMPER ] |
... | ... | |
806 | 838 |
## |
807 | 839 |
lustre_spec: ASSUME XOR |
808 | 840 |
## |
809 |
## Ends in an error in state: 331.
|
|
841 |
## Ends in an error in state: 335.
|
|
810 | 842 |
## |
811 | 843 |
## contract_content -> ASSUME . qexpr SCOL contract_content [ TEL EOF ] |
812 | 844 |
## contract_content -> ASSUME . STRING qexpr SCOL contract_content [ TEL EOF ] |
... | ... | |
820 | 852 |
|
821 | 853 |
lustre_spec: CONST IDENT COL TREAL WHENNOT |
822 | 854 |
## |
823 |
## Ends in an error in state: 327.
|
|
855 |
## Ends in an error in state: 331.
|
|
824 | 856 |
## |
825 | 857 |
## contract_content -> CONST IDENT option(preceded(COL,typeconst)) . EQ expr SCOL contract_content [ TEL EOF ] |
826 | 858 |
## |
... | ... | |
836 | 868 |
## |
837 | 869 |
lustre_spec: CONST IDENT XOR |
838 | 870 |
## |
839 |
## Ends in an error in state: 326.
|
|
871 |
## Ends in an error in state: 330.
|
|
840 | 872 |
## |
841 | 873 |
## contract_content -> CONST IDENT . option(preceded(COL,typeconst)) EQ expr SCOL contract_content [ TEL EOF ] |
842 | 874 |
## |
... | ... | |
845 | 877 |
## |
846 | 878 |
lustre_spec: CONST IDENT EQ XOR |
847 | 879 |
## |
848 |
## Ends in an error in state: 328.
|
|
880 |
## Ends in an error in state: 332.
|
|
849 | 881 |
## |
850 | 882 |
## contract_content -> CONST IDENT option(preceded(COL,typeconst)) EQ . expr SCOL contract_content [ TEL EOF ] |
851 | 883 |
## |
... | ... | |
858 | 890 |
|
859 | 891 |
lustre_spec: CONST XOR |
860 | 892 |
## |
861 |
## Ends in an error in state: 325.
|
|
893 |
## Ends in an error in state: 329.
|
|
862 | 894 |
## |
863 | 895 |
## contract_content -> CONST . IDENT option(preceded(COL,typeconst)) EQ expr SCOL contract_content [ TEL EOF ] |
864 | 896 |
## |
... | ... | |
871 | 903 |
|
872 | 904 |
lustre_spec: CONTRACT UIDENT LPAR CONST UIDENT RPAR RETURNS LPAR CONST IDENT RPAR LET TEL XOR |
873 | 905 |
## |
874 |
## Ends in an error in state: 459.
|
|
906 |
## Ends in an error in state: 464.
|
|
875 | 907 |
## |
876 | 908 |
## nonempty_list(top_contract) -> top_contract . [ EOF ] |
877 | 909 |
## nonempty_list(top_contract) -> top_contract . nonempty_list(top_contract) [ EOF ] |
... | ... | |
883 | 915 |
Node contracts must be separated by `;`s. |
884 | 916 |
|
885 | 917 |
lustre_spec: CONTRACT XOR |
918 |
## |
|
919 |
## Ends in an error in state: 463. |
|
920 |
## |
|
921 |
## option(CONTRACT) -> CONTRACT . [ VAR MODE IMPORT GUARANTEES EOF CONST ASSUME ] |
|
922 |
## top_contract -> CONTRACT . node_ident_decl LPAR var_decl_list(vdecl) RPAR RETURNS LPAR var_decl_list(vdecl) RPAR option(SCOL) LET contract_content TEL [ EOF CONTRACT ] |
|
923 |
## |
|
886 | 924 |
## The known suffix of the stack is as follows: |
887 | 925 |
## CONTRACT |
888 | 926 |
## |
... | ... | |
919 | 957 |
## |
920 | 958 |
lustre_spec: GUARANTEES STRING UIDENT SCOL XOR |
921 | 959 |
## |
922 |
## Ends in an error in state: 324.
|
|
960 |
## Ends in an error in state: 328.
|
|
923 | 961 |
## |
924 |
## contract_content -> GUARANTEES STRING qexpr SCOL . contract_content [ TEL EOF ] |
|
962 |
## contract_content -> GUARANTEES STRING qexpr option(proof_annotation) SCOL . contract_content [ TEL EOF ]
|
|
925 | 963 |
## |
926 | 964 |
## The known suffix of the stack is as follows: |
927 |
## GUARANTEES STRING qexpr SCOL |
|
965 |
## GUARANTEES STRING qexpr option(proof_annotation) SCOL
|
|
928 | 966 |
## |
929 | 967 |
lustre_spec: GUARANTEES UIDENT SCOL XOR |
930 | 968 |
## |
931 |
## Ends in an error in state: 342. |
|
969 |
## Ends in an error in state: 347. |
Also available in: Unified diff
a version that almost work for the k-inuctive two_counters example