Project

General

Profile

« Previous | Next » 

Revision efcc8d7f

Added by LĂ©lio Brun about 2 years ago

move arrow spec in its own header

View differences:

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