Revision 186e1aef
Added by Lélio Brun about 2 years ago
| src/backends/C/c_backend_spec.ml | ||
|---|---|---|
| 136 | 136 |
|
| 137 | 137 |
(* TODO: This preamble shall be a list of types, axiomatics, predicates, theorems *) |
| 138 | 138 |
let pp_acsl_preamble fmt _preamble = |
| 139 |
Format.fprintf fmt "";
|
|
| 139 |
fprintf fmt ""; |
|
| 140 | 140 |
() |
| 141 | 141 |
|
| 142 | 142 |
let pp_acsl_basic_type_desc t_desc = |
| ... | ... | |
| 316 | 316 |
pp_l l |
| 317 | 317 |
pp_r r |
| 318 | 318 |
|
| 319 |
let pp_valid = |
|
| 320 |
pp_print_braced |
|
| 321 |
~pp_nil:pp_true |
|
| 322 |
~pp_prologue:(fun fmt () -> pp_print_string fmt "\\valid(")
|
|
| 323 |
~pp_epilogue:pp_print_cpar |
|
| 324 |
|
|
| 325 | 319 |
let pp_equal pp_l pp_r fmt (l, r) = |
| 326 | 320 |
fprintf fmt "%a == %a" |
| 327 | 321 |
pp_l l |
| ... | ... | |
| 349 | 343 |
pp_v |
| 350 | 344 |
fmt |
| 351 | 345 |
|
| 346 |
let pp_valid pp = |
|
| 347 |
pp_and_l |
|
| 348 |
(* pp_print_list *) |
|
| 349 |
(* ~pp_sep:pp_print_cut *) |
|
| 350 |
(fun fmt x -> fprintf fmt "\\valid(%a)" pp x) |
|
| 351 |
|
|
| 352 | 352 |
let pp_ite pp_c pp_t pp_f fmt (c, t, f) = |
| 353 |
fprintf fmt "%a @[<hov>? %a@ : %a@]"
|
|
| 353 |
fprintf fmt "(%a @[<hov>? %a@ : %a)@]"
|
|
| 354 | 354 |
pp_c c |
| 355 | 355 |
pp_t t |
| 356 | 356 |
pp_f f |
| ... | ... | |
| 661 | 661 |
let d = VDSet.(diff (union (live_i m i) (assigned empty instr)) |
| 662 | 662 |
(live_i m (i+1))) in |
| 663 | 663 |
(* XXX *) |
| 664 |
printf "%d : %a\n%d : %a\nocc: %a\n\n" |
|
| 665 |
i |
|
| 666 |
(pp_print_parenthesized pp_var_decl) (VDSet.elements (live_i m i)) |
|
| 667 |
(i+1) |
|
| 668 |
(pp_print_parenthesized pp_var_decl) (VDSet.elements (live_i m (i+1))) |
|
| 669 |
(pp_print_parenthesized pp_var_decl) VDSet.(elements (assigned empty instr));
|
|
| 664 |
(* printf "%d : %a\n%d : %a\nocc: %a\n\n"
|
|
| 665 |
* i
|
|
| 666 |
* (pp_print_parenthesized pp_var_decl) (VDSet.elements (live_i m i))
|
|
| 667 |
* (i+1)
|
|
| 668 |
* (pp_print_parenthesized pp_var_decl) (VDSet.elements (live_i m (i+1)))
|
|
| 669 |
* (pp_print_parenthesized pp_var_decl) VDSet.(elements (assigned empty instr)); *)
|
|
| 670 | 670 |
let prev_trans fmt () = pp_mem_trans' ~i fmt (m, mem_in, mem_out) in |
| 671 | 671 |
let pred pp v = |
| 672 | 672 |
let vars = VDSet.(union (of_list m.mstep.step_locals) |
| ... | ... | |
| 932 | 932 |
(pp_assigns pp_register) insts |
| 933 | 933 |
(pp_ensures |
| 934 | 934 |
(pp_forall |
| 935 |
(fun fmt () -> |
|
| 936 |
fprintf fmt "%a, %s" |
|
| 937 |
pp_machine_decl (name, "mem_ghost", mem_in) |
|
| 938 |
mem_out) |
|
| 939 |
(pp_implies |
|
| 940 |
(pp_at_pre pp_mem_ghost') |
|
| 935 |
pp_machine_decl |
|
| 936 |
(pp_forall |
|
| 937 |
pp_machine_decl |
|
| 941 | 938 |
(pp_implies |
| 942 |
pp_mem_ghost' |
|
| 943 |
pp_mem_trans'')))) |
|
| 944 |
((), |
|
| 945 |
((name, mem_in, self), |
|
| 946 |
((name, mem_out, self), |
|
| 947 |
(m, mem_in, mem_out))))) |
|
| 939 |
(pp_at_pre pp_mem_ghost') |
|
| 940 |
(pp_implies |
|
| 941 |
pp_mem_ghost' |
|
| 942 |
pp_mem_trans''))))) |
|
| 943 |
((name, "mem_ghost", mem_in), |
|
| 944 |
((name, "mem_ghost", mem_out), |
|
| 945 |
((name, mem_in, self), |
|
| 946 |
((name, mem_out, self), |
|
| 947 |
(m, mem_in, mem_out))))) |
|
| 948 |
) |
|
| 948 | 949 |
fmt () |
| 949 | 950 |
|
| 950 | 951 |
let pp_step_instr_spec m self fmt (i, _instr) = |
| ... | ... | |
| 955 | 956 |
(pp_spec |
| 956 | 957 |
(pp_assert |
| 957 | 958 |
(pp_forall |
| 958 |
(fun fmt () -> |
|
| 959 |
fprintf fmt "%a, %s" |
|
| 960 |
pp_machine_decl (name, "mem_ghost", mem_in) |
|
| 961 |
mem_out) |
|
| 962 |
(pp_implies |
|
| 963 |
(pp_at_pre pp_mem_ghost') |
|
| 959 |
pp_machine_decl |
|
| 960 |
(pp_forall |
|
| 961 |
pp_machine_decl |
|
| 964 | 962 |
(pp_implies |
| 965 |
(pp_mem_ghost' ~i) |
|
| 966 |
(pp_mem_trans'' ~i)))))) |
|
| 967 |
((), |
|
| 968 |
((name, mem_in, self), |
|
| 969 |
((name, mem_out, self), |
|
| 970 |
(m, mem_in, mem_out)))) |
|
| 963 |
(pp_at_pre pp_mem_ghost') |
|
| 964 |
(pp_implies |
|
| 965 |
(pp_mem_ghost' ~i) |
|
| 966 |
(pp_mem_trans'' ~i))))))) |
|
| 967 |
((name, "mem_ghost", mem_in), |
|
| 968 |
((name, "mem_ghost", mem_out), |
|
| 969 |
((name, mem_in, self), |
|
| 970 |
((name, mem_out, self), |
|
| 971 |
(m, mem_in, mem_out))))) |
|
| 971 | 972 |
|
| 972 | 973 |
end |
| 973 | 974 |
|
Also available in: Unified diff
working proto