Revision 4174a469
Added by Guillaume Davy over 8 years ago
| src/backends/C/c_backend_spec.ml | ||
|---|---|---|
| 354 | 354 |
| _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 |
| 355 | 355 |
| _ -> raise (Failure ("No ACSL printer for function " ^ i))
|
| 356 | 356 |
|
| 357 |
let pp_acsl_tag fmt t = |
|
| 358 |
pp_print_string fmt (if t = Corelang.tag_true then "\\true" else if t = Corelang.tag_false then "\\false" else t) |
|
| 359 |
let rec pp_acsl_const fmt c = |
|
| 360 |
match c with |
|
| 361 |
| Const_int i -> pp_print_int fmt i |
|
| 362 |
| Const_real r -> pp_print_string fmt r |
|
| 363 |
| Const_float r -> pp_print_float fmt r |
|
| 364 |
| Const_tag t -> pp_acsl_tag fmt t |
|
| 365 |
| Const_array ca -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " pp_c_const) ca
|
|
| 366 |
| Const_struct fl -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " (fun fmt (f, c) -> pp_c_const fmt c)) fl
|
|
| 367 |
| Const_string _ -> assert false (* string occurs in annotations not in C *) |
|
| 357 | 368 |
|
| 358 | 369 |
let rec pp_acsl_val ?(is_lhs=false) self pp_var fmt v = |
| 359 | 370 |
match v with |
| 360 |
| Cst c -> pp_c_const fmt c
|
|
| 371 |
| Cst c -> pp_acsl_const fmt c
|
|
| 361 | 372 |
| Array _ |
| 362 | 373 |
| Access _ -> assert false (* no arrays *) |
| 363 | 374 |
| Power (v, n) -> assert false |
| 364 | 375 |
| LocalVar v -> pp_var fmt v |
| 365 | 376 |
| StateVar v -> |
| 366 |
if Types.is_array_type v.var_type |
|
| 377 |
(match (Types.repr v.var_type).Types.tdesc with |
|
| 378 |
| Types.Tbool -> fprintf fmt "((%t)?\\true:\\false)" |
|
| 379 |
| _ -> fprintf fmt "%t") |
|
| 380 |
(if Types.is_array_type v.var_type |
|
| 367 | 381 |
then assert false |
| 368 |
else fprintf fmt "%s%s_reg.%s" self |
|
| 369 |
(if !Options.no_pointer then "." else "->") v.var_id |
|
| 382 |
else fun fmt -> fprintf fmt "%s%s_reg.%s" self
|
|
| 383 |
(if !Options.no_pointer then "." else "->") v.var_id)
|
|
| 370 | 384 |
| Fun (n, vl) -> Format.fprintf fmt "%a" (basic_lib_pp_acsl n Machine_code.get_val_type (pp_acsl_val self pp_var)) vl |
| 371 | 385 |
|
| 372 | 386 |
|
| ... | ... | |
| 446 | 460 |
assert false (* no array *) |
| 447 | 461 |
else ( |
| 448 | 462 |
(if List.exists (fun o -> o.var_id = id.var_id) outputs (* id is output *) |
| 449 |
then fprintf fmt "(*%s%s" id.var_id suffix
|
|
| 463 |
then fprintf fmt "((*%s)%s" id.var_id suffix
|
|
| 450 | 464 |
else fprintf fmt "(%s%s" id.var_id suffix); |
| 451 | 465 |
match (Types.repr id.var_type).Types.tdesc with |
| 452 | 466 |
| Types.Tbool -> fprintf fmt "?\\true:\\false)" |
Also available in: Unified diff
Correct some problem related to new bool encoding