Revision 97602f7c
Added by Guillaume Davy over 10 years ago
| src/backends/C/c_backend_spec.ml | ||
|---|---|---|
| 72 | 72 |
let rec aux t pp_suffix = |
| 73 | 73 |
match (Types.repr t).Types.tdesc with |
| 74 | 74 |
| Types.Tclock t' -> aux t' pp_suffix |
| 75 |
| Types.Tbool -> fprintf fmt "integer %s%a" var pp_suffix ()
|
|
| 75 |
| Types.Tbool -> fprintf fmt "boolean %s%a" var pp_suffix ()
|
|
| 76 | 76 |
| Types.Treal -> fprintf fmt "real %s%a" var pp_suffix () |
| 77 | 77 |
| Types.Tint -> fprintf fmt "integer %s%a" var pp_suffix () |
| 78 | 78 |
| Types.Tarray (d, t') -> |
| ... | ... | |
| 365 | 365 |
| StateVar v -> |
| 366 | 366 |
if Types.is_array_type v.var_type |
| 367 | 367 |
then assert false |
| 368 |
else fprintf fmt "%s%s_reg.%a" self
|
|
| 369 |
(if !Options.no_pointer then "." else "->") pp_var v
|
|
| 368 |
else fprintf fmt "%s%s_reg.%s" self
|
|
| 369 |
(if !Options.no_pointer then "." else "->") v.var_id
|
|
| 370 | 370 |
| 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 | 371 |
|
| 372 | 372 |
|
| ... | ... | |
| 440 | 440 |
despite its scalar Lustre type) |
| 441 | 441 |
- moreover, cast arrays variables into their original array type. |
| 442 | 442 |
*) |
| 443 |
let pp_acsl_var_read outputs fmt id = |
|
| 443 |
let pp_acsl_var_read suffix outputs fmt id =
|
|
| 444 | 444 |
if Types.is_array_type id.var_type |
| 445 | 445 |
then |
| 446 | 446 |
assert false (* no array *) |
| 447 | 447 |
else ( |
| 448 |
if List.exists (fun o -> o.var_id = id.var_id) outputs (* id is output *) |
|
| 449 |
then fprintf fmt "*%s" id.var_id |
|
| 450 |
else fprintf fmt "%s" id.var_id |
|
| 448 |
(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 |
|
| 450 |
else fprintf fmt "(%s%s" id.var_id suffix); |
|
| 451 |
match (Types.repr id.var_type).Types.tdesc with |
|
| 452 |
| Types.Tbool -> fprintf fmt "?\\true:\\false)" |
|
| 453 |
| _ -> fprintf fmt ")" |
|
| 451 | 454 |
) |
| 452 | 455 |
|
| 453 | 456 |
|
| ... | ... | |
| 548 | 551 |
) |
| 549 | 552 |
| _ -> fprintf fmt "spec_%i(%a%t);" |
| 550 | 553 |
ee.muid |
| 551 |
(Utils.fprintf_list ~sep:", " (pp_acsl_var_read outputs)) ee.mmstep_logic.step_inputs |
|
| 554 |
(Utils.fprintf_list ~sep:", " (pp_acsl_var_read "" outputs)) ee.mmstep_logic.step_inputs
|
|
| 552 | 555 |
(fun fmt -> if stateless then fprintf fmt "" else fprintf fmt ", %s%s" (if !Options.no_pointer then "*" else "") self) |
| 553 | 556 |
in |
| 554 | 557 |
fprintf fmt "@[<v 2>/*@@ "; |
Also available in: Unified diff
Correct bug when there is no precondition and change reprensentation
of boolean in ACSL