Project

General

Profile

Revision 66359a5e src/backends/Horn/horn_backend_printers.ml

View differences:

src/backends/Horn/horn_backend_printers.ml
96 96
   for the type integer (arrays).
97 97
*)
98 98
let rec pp_default_val fmt t =
99
  let t = Types.dynamic_type t in
100
  if Types.is_bool_type t  then fprintf fmt "true" else
101
  if Types.is_int_type t then fprintf fmt "0" else 
102
  if Types.is_real_type t then fprintf fmt "0" else 
99 103
  match (Types.dynamic_type t).Types.tdesc with
100
  | Types.Tint -> fprintf fmt "0"
101
  | Types.Treal -> fprintf fmt "0"
102
  | Types.Tbool -> fprintf fmt "true"
103 104
  | Types.Tarray(dim, l) -> (* TODO PL: this strange code has to be (heavily) checked *)
104 105
     let valt = Types.array_element_type t in
105 106
     fprintf fmt "((as const (Array Int %a)) %a)"

Also available in: Unified diff