Revision 66359a5e
Added by Pierre-Loïc Garoche about 7 years ago
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
[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