c_backend_spec.ml

(********************************************************************)
(*                                                                  *)
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
(*                                                                  *)
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
(*  under the terms of the GNU Lesser General Public License        *)
(*  version 2.1.                                                    *)
(*                                                                  *)
(********************************************************************)
open Utils
open Format
open Lustre_types
open Machine_code_types
open C_backend_common
open Corelang
open Spec_types
open Machine_code_common
module Mpfr = Lustrec_mpfr

(**************************************************************************)
(*     Printing spec for c *)

(**************************************************************************)

let pp_acsl_basic_type_desc t_desc =
  if Types.is_bool_type t_desc then
    (* if !Options.cpp then "bool" else "_Bool" *)
    "_Bool"
  else if Types.is_int_type t_desc then
    (* !Options.int_type *)
    if t_desc.tid = -1 then "int" else "integer"
  else if Types.is_real_type t_desc then
    if !Options.mpfr then Mpfr.mpfr_t else !Options.real_type
  else assert false
(* Not a basic C type. Do not handle arrays or pointers *)

let pp_acsl pp fmt = fprintf fmt "@[<v>/*%@ @[<v>%a@]@,*/@]" pp

let pp_acsl_cut pp fmt = fprintf fmt "%a@," (pp_acsl pp)

let pp_acsl_line pp fmt = fprintf fmt "//%@ @[<h>%a@]" pp

let pp_acsl_line' ?(ghost = false) pp fmt x =
  let op = if ghost then "" else "*" in
  let cl = if ghost then "@" else "*" in
  fprintf fmt "/%s%@ @[<h>%a@] %s/" op pp x cl

let pp_acsl_line'_cut pp fmt = fprintf fmt "%a@," (pp_acsl_line' pp)

let pp_requires pp fmt = fprintf fmt "requires %a;" pp

let pp_ensures pp fmt = fprintf fmt "ensures %a;" pp

let pp_assumes pp fmt = fprintf fmt "assumes %a;" pp

let pp_terminates pp fmt = fprintf fmt "terminates %a;" pp

let pp_assigns pp =
  pp_comma_list
    ~pp_prologue:(fun fmt () -> pp_print_string fmt "assigns ")
    ~pp_epilogue:pp_print_semicolon'
    pp

let pp_ghost pp fmt = fprintf fmt "ghost %a" pp

let pp_assert pp fmt = fprintf fmt "assert %a;" pp

let pp_loop_invariant pp fmt = fprintf fmt "loop invariant %a;" pp