Project

General

Profile

« Previous | Next » 

Revision d0f26f04

Added by LĂ©lio Brun 7 months ago

corrections for stateless nodes

View differences:

src/backends/C/c_backend_spec.ml
22 22

  
23 23
(**************************************************************************)
24 24

  
25
(* TODO ACSL Return updates machines (eg with local annotations) and acsl
26
   preamble *)
27
let preprocess_acsl machines = machines, []
28

  
29 25
let pp_acsl_basic_type_desc t_desc =
30 26
  if Types.is_bool_type t_desc then
31 27
    (* if !Options.cpp then "bool" else "_Bool" *)
......
187 183

  
188 184
let pp_not pp fmt = fprintf fmt "!%a" pp
189 185

  
190
let pp_valid pp =
191
  pp_and_l
192
    (* pp_print_list *)
193
    (* ~pp_sep:pp_print_cut *)
194
    (fun fmt x -> fprintf fmt "\\valid(%a)" pp x)
186
let pp_valid pp = pp_and_l (fun fmt x -> fprintf fmt "\\valid(%a)" pp x)
195 187

  
196 188
let pp_old pp fmt = fprintf fmt "\\old(%a)" pp
197 189

  

Also available in: Unified diff