Project

General

Profile

Revision cefc3744 src/backends/C/c_backend_spec.ml

View differences:

src/backends/C/c_backend_spec.ml
3 3

  
4 4
(**************************************************************************)
5 5

  
6
let pp_acsl_type var fmt t =
7
  let rec aux t pp_suffix =
8
  match (Types.repr t).Types.tdesc with
9
  | Types.Tclock t'       -> aux t' pp_suffix
10
  | Types.Tbool           -> fprintf fmt "int %s%a" var pp_suffix ()
11
  | Types.Treal           -> fprintf fmt "real %s%a" var pp_suffix ()
12
  | Types.Tint            -> fprintf fmt "int %s%a" var pp_suffix ()
13
  | Types.Tarray (d, t')  ->
14
    let pp_suffix' fmt () = fprintf fmt "%a[%a]" pp_suffix () pp_c_dimension d in
15
    aux t' pp_suffix'
16
  (* | Types.Tstatic (_, t') -> fprintf fmt "const "; aux t' pp_suffix *)
17
  (* | Types.Tconst ty       -> fprintf fmt "%s %s" ty var *)
18
  (* | Types.Tarrow (_, _)   -> fprintf fmt "void (\*%s)()" var *)
19
  | _                     -> eprintf "internal error: pp_acsl_type %a@." Types.print_ty t; assert false
20
  in aux t (fun fmt () -> ())
21

  
22
let pp_acsl_var_decl fmt id =
23
  pp_acsl_type id.var_id fmt id.var_type
24

  
6 25

  
7 26
let pp_econst fmt c = 
8 27
  match c with

Also available in: Unified diff