Project

General

Profile

« Previous | Next » 

Revision dccec723

Added by LĂ©lio Brun over 3 years ago

a version that almost work for the k-inuctive two_counters example

View differences:

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.
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff