CristalCaveGem » LustreC

let pp_var_decl fmt v = pp_print_string fmt v.var_id

let pp_true fmt () = pp_print_string fmt "\\true"

let pp_cast pp_ty pp fmt (ty, x) = fprintf fmt "(%a) %a" pp_ty ty pp x

let find_machine f = List.find (fun m -> m.mname.node_id = f)

let instances machines m =

  in

let pp_separated pp_self pp_mem pp_ptr fmt (self, mem, paths, ptrs) =

  fprintf

    self

    pp_mem

    mem

    paths

    (pp_comma_list ~pp_prologue:pp_print_comma pp_ptr)

    ptrs

         ~pp_epilogue:pp_print_cut

         ~pp_open_box:pp_open_vbox0

         (pp_memory_pack_def m))

let pp_transition_def m fmt t =

  let name = t.tname.node_id in

          (name, mem, self)

          (pp_ensures

             (pp_memory_pack_aux

                pp_ptr

                pp_print_string))

          (name, mem, self)

  let pp_step_spec fmt machines self mem m =

    let name = m.mname.node_id in

    let insts = instances machines m in

    in

    let inputs = m.mstep.step_inputs in

    let outputs = m.mstep.step_outputs in

             %a@,\

             %a@,\

             %a@,\

             %a"

            (pp_if_outputs (pp_requires (pp_valid pp_var_decl)))

            outputs

            (pp_requires pp_mem_valid')

            (name, self)

            (pp_requires (pp_separated' self mem))

            (pp_requires (pp_memory_pack_aux pp_ptr pp_print_string))

            (name, mem, self)

            (pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string))

            c

            (pp_assigns pp_ptr_decl)

            outputs

            (pp_assigns pp_reset_flag')

            [ self ]

            (pp_assigns (pp_reset_flag_chain self))

            (pp_assigns pp_reset_flag')

            [ mem ]

            (pp_assigns (pp_reset_flag_chain ~indirect:false mem))

      fmt

      ()

  let pp_main_loop_invariants main_mem machines fmt m =

    let name = m.mname.node_id in

    pp_acsl_cut

      (fun fmt () ->

        fprintf

    mpformula = sanitize_formula mp.mpformula

  }

let sanitize_spec s =

  { s with

  (* Step instructions *)

  s : instr_t list;

  (* Memory pack spec *)

  (* Transition spec *)

  t :

    (var_decl list

  let outputs_pi = Lustre_live.inter_live_i_with id (i - 1) outputs in

  let locals_i = Lustre_live.inter_live_i_with id i locals in

  let outputs_i = Lustre_live.inter_live_i_with id i outputs in

  let pred_t ctx a =

    ( inputs @ locals_i @ outputs_i,

      ctx.m,

        {

          inst with

          instr_spec =

            else [ mk_memory_pack ~i id ])

            @ [

                mk_transition

    let ctx =

      ctl

        (MStep ([ var_x ], inst, [ c1; c2 ]))

        (mk_transition ~inst false (node_name td) [ vdecl_to_val var_x ])

        { ctx with j = IMap.add inst (td, []) ctx.j }

    in

    let e = translate_expr e in

    ctl

      (MStateAssign (var_x, e))

      (mk_state_assign_tr var_x e)

      { ctx with m = ISet.add x ctx.m }

  | [ x ], Expr_fby (e1, e2) when env.is_local x ->

    let ctx =

      ctl

        (MStateAssign (var_x, e2))

        (mk_state_assign_tr var_x e2)

        { ctx with m = ISet.add x ctx.m }

    in

    let stateless = Stateless.check_node node_f in

    let inst = if stateless then None else Some i in

    let mp =

    in

    let ctx =

      ctl

    try

      let var_x = env.get_var x in

      let instr, spec = translate_act (var_x, eq.eq_rhs) in

    with Not_found ->

      Format.eprintf "ERROR: node %s, eq %a@." id Printers.pp_node_eq eq;

      raise Not_found)

  (* Build the machine *)

  let mmap = IMap.bindings ctx.j in

  let mmemory_packs =

    memory_pack_0 nd

         (List.rev ctx.mp)

  in

  let mtransitions =

    transition_0 nd

      | Some (Contract spec) ->

        pp_mspec m fmt spec)

    (pp_memory_packs m)

    (pp_transitions m)

    m.mspec.mtransitions

    (pp_print_list Printers.pp_expr_annot)

          ];

        step_asserts = [];

      };

    mannot = [];

    msch = None;

    mis_contract = false;

        step_instrs = [];

        step_asserts = [];

      };

    mannot = [];

    msch = None;

    mis_contract = false;

type machine_spec = {

  mnode_spec : mc_contract_t node_spec_t option;

  mtransitions : mc_transition_t list;

}

type machine_t = {