Project

General

Profile

« Previous | Next » 

Revision 186e1aef

Added by LĂ©lio Brun about 2 years ago

working proto

View differences:

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