CristalCaveGem » LustreC

let pp_at_pre pp_v fmt v = pp_at pp_v fmt (v, "Pre")

  let pp_contract fmt machines _self mem m =

    let pp_vars ?pp_eol = pp_comma_list ?pp_eol (pp_c_var_read m) in

    match contract_of machines m with

    | Some c, Some m_c ->

      fprintf fmt "%a%a"

        (pp_acsl_line'_cut

           (pp_ghost

              (fun fmt () ->

                 fprintf

                   fmt

                   "%a(%a%a);"

                   pp_machine_step_name

                   m_c.mname.node_id

                   (pp_vars ~pp_eol:pp_print_comma)

                   m_c.mstep.step_inputs

                   (pp_comma_list (pp_c_var_write m))

                   m_c.mstep.step_outputs)))

        ()

        (pp_acsl_cut

           (pp_print_option

              (fun fmt -> function

                 | Kinduction k ->

                   let l = List.init k (fun n -> n + 1) in

                   let pp_mem_in = pp_at_pre pp_ptr in

                   let pp_mem_out = pp_ptr in

                   pp_assert

                     (pp_and

                        (pp_and_l

                           (fun fmt n ->

                              (if n = k then

                                 pp_k_induction_inductive_case

                               else

                                 pp_k_induction_base_case)

                                m

                                pp_mem_in

                                pp_mem_out

                                pp_vars

                                fmt

                                (n, mem, mem)))

                        (pp_transition_aux m_c pp_print_string pp_print_string (pp_c_var_read m)))

                     fmt

                     (l, (m_c.mname.node_id,

                          m_c.mstep.step_inputs @ m_c.mstep.step_outputs,

                          "", ""))))) c.mc_proof

        | _, _ -> ()