| 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 |
|
no need to reschedule in order to "clock-protect" the unitialized state variables in ACSL !