Revision efcc8d7f
Added by Lélio Brun about 2 years ago
| src/backends/C/c_backend_spec.ml | ||
|---|---|---|
| 135 | 135 |
let preprocess_acsl machines = machines, [] |
| 136 | 136 |
|
| 137 | 137 |
(* TODO: This preamble shall be a list of types, axiomatics, predicates, theorems *) |
| 138 |
let pp_acsl_preamble fmt _preamble = |
|
| 139 |
fprintf fmt ""; |
|
| 140 |
()
|
|
| 138 |
(* let pp_acsl_preamble fmt _preamble =
|
|
| 139 |
* fprintf fmt "";
|
|
| 140 |
* () *)
|
|
| 141 | 141 |
|
| 142 | 142 |
let pp_acsl_basic_type_desc t_desc = |
| 143 | 143 |
if Types.is_bool_type t_desc then |
| ... | ... | |
| 679 | 679 |
let rec aux fmt instr = match instr.instr_desc with |
| 680 | 680 |
| MLocalAssign (x, v) |
| 681 | 681 |
| MStateAssign (x, v) -> |
| 682 |
pp_assign_spec m mem_out (pp_c_var_read m) mem_in (pp_c_var_read m)fmt |
|
| 682 |
pp_assign_spec m mem_out (pp_c_var_read m) mem_in (pp_c_var_read m) fmt
|
|
| 683 | 683 |
(x.var_type, mk_val (Var x) x.var_type, v) |
| 684 | 684 |
| MStep ([i0], i, vl) |
| 685 | 685 |
when Basic_library.is_value_internal_fun |
| ... | ... | |
| 689 | 689 |
pp_true fmt () |
| 690 | 690 |
| MStep ([_], i, _) when has_c_prototype i dependencies -> |
| 691 | 691 |
pp_true fmt () |
| 692 |
| MStep (xs, f, ys) ->
|
|
| 692 |
| MStep (xs, i, ys) ->
|
|
| 693 | 693 |
begin try |
| 694 |
let n, _ = List.assoc f m.minstances in
|
|
| 694 |
let n, _ = List.assoc i m.minstances in
|
|
| 695 | 695 |
pp_mem_trans_aux |
| 696 | 696 |
pp_access' pp_access' |
| 697 | 697 |
(pp_c_val m mem_in (pp_c_var_read m)) |
| 698 | 698 |
pp_var_decl |
| 699 | 699 |
fmt |
| 700 |
(node_name n, ys, [], xs, (mem_in, f), (mem_out, f))
|
|
| 700 |
(node_name n, ys, [], xs, (mem_in, i), (mem_out, i))
|
|
| 701 | 701 |
with Not_found -> pp_true fmt () |
| 702 | 702 |
end |
| 703 |
| MReset f ->
|
|
| 703 |
| MReset i ->
|
|
| 704 | 704 |
begin try |
| 705 |
let n, _ = List.assoc f m.minstances in
|
|
| 705 |
let n, _ = List.assoc i m.minstances in
|
|
| 706 | 706 |
pp_mem_init' fmt (node_name n, mem_out) |
| 707 | 707 |
with Not_found -> pp_true fmt () |
| 708 | 708 |
end |
| ... | ... | |
| 711 | 711 |
then (* boolean case *) |
| 712 | 712 |
pp_ite (pp_c_val m mem_in (pp_c_var_read m)) |
| 713 | 713 |
(fun fmt () -> |
| 714 |
try
|
|
| 715 |
let l = List.assoc tag_true brs in
|
|
| 716 |
pp_paren (pp_and_l aux) fmt l
|
|
| 717 |
with Not_found -> pp_true fmt ())
|
|
| 714 |
match List.assoc tag_true brs with
|
|
| 715 |
| _ :: _ as l -> pp_paren (pp_and_l aux) fmt l
|
|
| 716 |
| []
|
|
| 717 |
| exception Not_found -> pp_true fmt ())
|
|
| 718 | 718 |
(fun fmt () -> |
| 719 |
try |
|
| 720 |
let l = List.assoc tag_false brs in |
|
| 721 |
pp_paren (pp_and_l aux) fmt l |
|
| 722 |
with Not_found -> pp_true fmt ()) |
|
| 719 |
match List.assoc tag_false brs with |
|
| 720 |
| _ :: _ as l -> pp_paren (pp_and_l aux) fmt l |
|
| 721 |
| [] |
|
| 722 |
| exception Not_found -> |
|
| 723 |
(* try |
|
| 724 |
* let l = List.assoc tag_false brs in |
|
| 725 |
* pp_paren (pp_and_l aux) fmt l |
|
| 726 |
* with Not_found -> *) pp_true fmt ()) |
|
| 723 | 727 |
|
| 724 | 728 |
(* (pp_paren (pp_and_l aux)) (pp_paren (pp_and_l aux)) *) |
| 725 | 729 |
fmt (v, (), ()) |
| ... | ... | |
| 795 | 799 |
let pp_at_pre pp_p fmt p = |
| 796 | 800 |
pp_at pp_p fmt (p, label_pre) |
| 797 | 801 |
|
| 798 |
let pp_arrow_spec fmt () = |
|
| 799 |
let name = "_arrow" in |
|
| 800 |
let mem_in = "mem_in" in |
|
| 801 |
let mem_out = "mem_out" in |
|
| 802 |
let reg_first = "_reg", "_first" in |
|
| 803 |
let mem_in_first = mem_in, reg_first in |
|
| 804 |
let mem_out_first = mem_out, reg_first in |
|
| 805 |
let mem = "mem" in |
|
| 806 |
let self = "self" in |
|
| 807 |
fprintf fmt "/* ACSL arrow spec */@,%a%a%a%a%a" |
|
| 808 |
|
|
| 809 |
(pp_spec_line (pp_ghost pp_print_string)) |
|
| 810 |
"struct _arrow_mem_ghost {struct _arrow_reg _reg;};"
|
|
| 811 |
|
|
| 812 |
(pp_spec_cut |
|
| 813 |
(pp_predicate |
|
| 814 |
(pp_mem_valid pp_machine_decl) |
|
| 815 |
(pp_valid pp_print_string))) |
|
| 816 |
((name, (name, "mem", "*" ^ self)), [self]) |
|
| 817 |
|
|
| 818 |
(pp_spec_cut |
|
| 819 |
(pp_predicate |
|
| 820 |
(pp_mem_init pp_machine_decl) |
|
| 821 |
(pp_equal |
|
| 822 |
(pp_access pp_print_string pp_access') |
|
| 823 |
pp_print_int))) |
|
| 824 |
((name, (name, "mem_ghost", mem_in)), |
|
| 825 |
(mem_in_first, 1)) |
|
| 826 |
|
|
| 827 |
(pp_spec_cut |
|
| 828 |
(pp_predicate |
|
| 829 |
(pp_mem_trans_aux |
|
| 830 |
pp_machine_decl pp_machine_decl pp_print_string pp_print_string) |
|
| 831 |
(pp_ite |
|
| 832 |
(pp_access pp_print_string pp_access') |
|
| 833 |
(pp_paren |
|
| 834 |
(pp_and |
|
| 835 |
(pp_equal |
|
| 836 |
(pp_access pp_print_string pp_access') |
|
| 837 |
pp_print_int) |
|
| 838 |
(pp_equal pp_print_string pp_print_string))) |
|
| 839 |
(pp_paren |
|
| 840 |
(pp_and |
|
| 841 |
(pp_equal |
|
| 842 |
(pp_access pp_print_string pp_access') |
|
| 843 |
(pp_access pp_print_string pp_access')) |
|
| 844 |
(pp_equal pp_print_string pp_print_string)))))) |
|
| 845 |
((name, ["integer x"; "integer y"], [], ["_Bool out"], |
|
| 846 |
(name, "mem_ghost", mem_in), (name, "mem_ghost", mem_out)), |
|
| 847 |
(* (("out", mem_in_first), *)
|
|
| 848 |
(mem_in_first, ((mem_out_first, 0), ("out", "x")),
|
|
| 849 |
((mem_out_first, mem_in_first), ("out", "y"))))
|
|
| 850 |
|
|
| 851 |
(pp_spec_cut |
|
| 852 |
(pp_predicate |
|
| 853 |
(pp_mem_ghost pp_machine_decl pp_machine_decl) |
|
| 854 |
(pp_equal |
|
| 855 |
(pp_access pp_print_string pp_access') |
|
| 856 |
(pp_indirect pp_print_string pp_access')))) |
|
| 857 |
((name, (name, "mem_ghost", mem), (name, "mem", "*" ^ self)), |
|
| 858 |
((mem, reg_first), (self, reg_first))) |
|
| 802 |
let pp_register = |
|
| 803 |
pp_print_list |
|
| 804 |
~pp_prologue:(fun fmt () -> pp_print_string fmt "self->") |
|
| 805 |
~pp_epilogue:(fun fmt () -> pp_print_string fmt "->_reg._first") |
|
| 806 |
~pp_sep:(fun fmt () -> pp_print_string fmt "->") |
|
| 807 |
(fun fmt (i, _) -> pp_print_string fmt i) |
|
| 808 |
|
|
| 809 |
module HdrMod = struct |
|
| 810 |
|
|
| 811 |
let print_machine_decl_prefix = fun _ _ -> () |
|
| 812 |
|
|
| 813 |
let pp_import_standard_spec fmt () = |
|
| 814 |
fprintf fmt "@,#include \"%s/arrow_spec.h%s\"" |
|
| 815 |
(Arrow.arrow_top_decl ()).top_decl_owner |
|
| 816 |
(if !Options.cpp then "pp" else "") |
|
| 817 |
|
|
| 818 |
end |
|
| 859 | 819 |
|
| 860 | 820 |
module SrcMod = struct |
| 861 | 821 |
|
| 862 | 822 |
let pp_predicates dependencies fmt machines = |
| 863 | 823 |
fprintf fmt |
| 864 |
"%a@,%a%a%a%a" |
|
| 865 |
pp_arrow_spec () |
|
| 824 |
"%a%a%a%a" |
|
| 866 | 825 |
(pp_print_list |
| 867 | 826 |
~pp_open_box:pp_open_vbox0 |
| 868 | 827 |
~pp_prologue:(pp_print_endcut "/* ACSL `valid` predicates */") |
| ... | ... | |
| 887 | 846 |
(print_machine_trans_annotations machines dependencies) |
| 888 | 847 |
~pp_epilogue:pp_print_cutcut) machines |
| 889 | 848 |
|
| 890 |
let pp_register = |
|
| 891 |
pp_print_list |
|
| 892 |
~pp_prologue:(fun fmt () -> pp_print_string fmt "self->") |
|
| 893 |
~pp_epilogue:(fun fmt () -> pp_print_string fmt "->_reg._first") |
|
| 894 |
~pp_sep:(fun fmt () -> pp_print_string fmt "->") |
|
| 895 |
(fun fmt (i, _) -> pp_print_string fmt i) |
|
| 896 |
|
|
| 897 | 849 |
let pp_reset_spec fmt machines self m = |
| 898 | 850 |
let name = m.mname.node_id in |
| 899 | 851 |
let mem = mk_mem m in |
Also available in: Unified diff
move arrow spec in its own header