Project

General

Profile

« Previous | Next » 

Revision c226a3ba

Added by LĂ©lio Brun over 2 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