Project

General

Profile

« Previous | Next » 

Revision 66359a5e

Added by Pierre-Loïc Garoche about 7 years ago

[general] large modification: added machine types, a second typing phase dealing with machine types (eg uint8)
typing was transformed as a functor and parametrized by basic types (int/real/bool)
it can also be applied multiple times on the same program

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