Project

General

Profile

« Previous | Next » 

Revision 36454535

Added by Pierre-Loïc Garoche over 10 years ago

Merged horn_traces branch

View differences:

src/backends/C/c_backend_spec.ml
31 31
  pp_acsl_type id.var_id fmt id.var_type
32 32

  
33 33

  
34
let pp_econst fmt c = 
35
  match c with
36
    | EConst_int i -> pp_print_int fmt i
37
    | EConst_real r -> pp_print_string fmt r
38
    | EConst_float r -> pp_print_float fmt r
39
    | EConst_bool b -> pp_print_bool fmt b
40
    | EConst_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
41

  
42 34
let rec pp_eexpr is_output fmt eexpr = 
43 35
  let pp_eexpr = pp_eexpr is_output in
44 36
  match eexpr.eexpr_desc with
45
    | EExpr_const c -> pp_econst fmt c
37
    | EExpr_const c -> Printers.pp_econst fmt c
46 38
    | EExpr_ident id -> 
47 39
      if is_output id then pp_print_string fmt ("*" ^ id) else pp_print_string fmt id
48 40
    | EExpr_tuple el -> Utils.fprintf_list ~sep:"," pp_eexpr fmt el

Also available in: Unified diff