Revision f51926b8
Added by Lélio Brun over 3 years ago
| src/backends/C/c_backend_spec.ml | ||
|---|---|---|
| 211 | 211 |
pp_print_list |
| 212 | 212 |
~pp_open_box:pp_open_vbox0 |
| 213 | 213 |
~pp_sep:(fun fmt () -> fprintf fmt "@,&& ") |
| 214 |
~pp_nil:pp_true |
|
| 214 | 215 |
pp_v |
| 215 | 216 |
fmt |
| 216 | 217 |
|
| ... | ... | |
| 492 | 493 |
eprintf "Internal error: arrow not found"; |
| 493 | 494 |
raise Not_found |
| 494 | 495 |
|
| 496 |
let rec has_memory_val m v = |
|
| 497 |
let has_mem = has_memory_val m in |
|
| 498 |
match v.value_desc with |
|
| 499 |
| Var v -> |
|
| 500 |
is_memory m v |
|
| 501 |
| Array vl |
|
| 502 |
| Fun (_, vl) -> |
|
| 503 |
List.exists has_mem vl |
|
| 504 |
| Access (t, i) |
|
| 505 |
| Power (t, i) -> |
|
| 506 |
has_mem t || has_mem i |
|
| 507 |
| _ -> |
|
| 508 |
false |
|
| 509 |
|
|
| 510 |
let has_memory : type a. machine_t -> (value_t, a) expression_t -> bool = fun m -> function |
|
| 511 |
| Val v -> has_memory_val m v |
|
| 512 |
| _ -> false |
|
| 513 |
|
|
| 495 | 514 |
let pp_spec mode m = |
| 496 | 515 |
let rec pp_spec mode fmt f = |
| 497 | 516 |
let mem_in, mem_in', indirect_r, mem_out, mem_out', indirect_l = |
| ... | ... | |
| 526 | 545 |
| False -> |
| 527 | 546 |
pp_false fmt () |
| 528 | 547 |
| Equal (a, b) -> |
| 529 |
pp_assign_spec |
|
| 530 |
m |
|
| 531 |
mem_out |
|
| 532 |
(pp_c_var_read ~test_output:false m) |
|
| 533 |
indirect_l |
|
| 534 |
mem_in |
|
| 535 |
(pp_c_var_read ~test_output:false m) |
|
| 536 |
indirect_r |
|
| 537 |
fmt |
|
| 538 |
(type_of_l_value a, val_of_expr a, val_of_expr b) |
|
| 548 |
let pp_eq fmt () = |
|
| 549 |
pp_assign_spec |
|
| 550 |
m |
|
| 551 |
mem_out |
|
| 552 |
(pp_c_var_read ~test_output:false m) |
|
| 553 |
indirect_l |
|
| 554 |
mem_in |
|
| 555 |
(pp_c_var_read ~test_output:false m) |
|
| 556 |
indirect_r |
|
| 557 |
fmt |
|
| 558 |
(type_of_l_value a, val_of_expr a, val_of_expr b) |
|
| 559 |
in |
|
| 560 |
if has_memory m b then |
|
| 561 |
let inst = find_arrow m in |
|
| 562 |
pp_paren |
|
| 563 |
(pp_implies |
|
| 564 |
(pp_not (pp_initialization pp_access')) |
|
| 565 |
pp_eq) |
|
| 566 |
fmt |
|
| 567 |
((Arrow.arrow_id, (mem_in, inst)), ()) |
|
| 568 |
else |
|
| 569 |
pp_eq fmt () |
|
| 539 | 570 |
| And fs -> |
| 540 | 571 |
pp_and_l pp_spec' fmt fs |
| 541 | 572 |
| Or fs -> |
| ... | ... | |
| 963 | 994 |
let pp_node_spec m fmt = function |
| 964 | 995 |
| Contract c |
| 965 | 996 |
| NodeSpec (_, Some c) -> |
| 966 |
PrintSpec.pp_spec PrintSpec.TransitionMode m fmt (Imply (c.mc_pre, c.mc_post)) |
|
| 997 |
PrintSpec.pp_spec PrintSpec.TransitionMode m fmt |
|
| 998 |
(Spec_common.red (Imply (c.mc_pre, c.mc_post))) |
|
| 967 | 999 |
| NodeSpec (f, None) -> |
| 968 | 1000 |
pp_print_string fmt f |
| 969 | 1001 |
|
Also available in: Unified diff
no need to reschedule in order to "clock-protect" the unitialized state variables in ACSL !