Revision 36454535
Added by Pierre-Loïc Garoche over 10 years ago
src/backends/C/c_backend_spec.ml | ||
---|---|---|
31 | 31 |
pp_acsl_type id.var_id fmt id.var_type |
32 | 32 |
|
33 | 33 |
|
34 |
let pp_econst fmt c = |
|
35 |
match c with |
|
36 |
| EConst_int i -> pp_print_int fmt i |
|
37 |
| EConst_real r -> pp_print_string fmt r |
|
38 |
| EConst_float r -> pp_print_float fmt r |
|
39 |
| EConst_bool b -> pp_print_bool fmt b |
|
40 |
| EConst_string s -> pp_print_string fmt ("\"" ^ s ^ "\"") |
|
41 |
|
|
42 | 34 |
let rec pp_eexpr is_output fmt eexpr = |
43 | 35 |
let pp_eexpr = pp_eexpr is_output in |
44 | 36 |
match eexpr.eexpr_desc with |
45 |
| EExpr_const c -> pp_econst fmt c |
|
37 |
| EExpr_const c -> Printers.pp_econst fmt c
|
|
46 | 38 |
| EExpr_ident id -> |
47 | 39 |
if is_output id then pp_print_string fmt ("*" ^ id) else pp_print_string fmt id |
48 | 40 |
| EExpr_tuple el -> Utils.fprintf_list ~sep:"," pp_eexpr fmt el |
Also available in: Unified diff
Merged horn_traces branch