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:

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; *)

Also available in: Unified diff