Project

General

Profile

« Previous | Next » 

Revision c226a3ba

Added by Lélio Brun over 3 years ago

start generating ACSL spec

View differences:

src/backends/C/c_backend_header.ml
105 105 
      (* constants *)
106 106 
      (print_static_constant_decl macro) const_locals
107 107 
      attr
108 
      pp_machine_memtype_name m.mname.node_id
108 
      (pp_machine_memtype_name ~ghost:false) m.mname.node_id
109 109 
      inst
110 110 
      (pp_print_list ~pp_open_box:pp_open_vbox0
111 111 
         ~pp_sep:(pp_print_endcut ";\\") ~pp_eol:(pp_print_endcut ";\\")
......
201 201 
    if not inode.nodei_stateless then
202 202 
      (* Declare struct *)
203 203 
      fprintf fmt "%a;"
204 
        pp_machine_memtype_name inode.nodei_id
204 
        (pp_machine_memtype_name ~ghost:false) inode.nodei_id
205 205 

  		




  206
  206
  
    
  let print_stateless_C_prototype fmt (name, inputs, outputs) =


  		




  207
  207
  
    
    let output =


  		












Also available in:  Unified diff