Ignore:
Timestamp:
Jul 12, 2012, 1:28:28 PM (7 years ago)
Author:
campbell
Message:

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/clightPrintMatita.ml

    r1633 r2176  
    151151  | Tint(sz, sg) -> "(Tint " ^ name_inttype sz sg ^ ")"
    152152  | Tfloat sz -> "(Tfloat " ^ name_floattype sz ^ ")"
    153   | Tpointer t -> "(Tpointer Any " ^ stype t ^ ")"
    154   | Tarray(t, n) -> "(Tarray Any " ^ stype t ^ " " ^ (string_of_int n) ^ ")"
     153  | Tpointer t -> "(Tpointer " ^ stype t ^ ")"
     154  | Tarray(t, n) -> "(Tarray " ^ stype t ^ " " ^ (string_of_int n) ^ ")"
    155155  | Tfunction(args, res) -> "(Tfunction " ^ typelist args ^ " " ^ stype res ^ ")"
    156156  | Tstruct(name, fld) ->
     
    159159      fieldlist "(Tunion (ident_of_nat " name fld
    160160  | Tcomp_ptr (name) ->
    161       "(Tcomp_ptr Any (ident_of_nat " ^ id_s name ^ "))"
     161      "(Tcomp_ptr (ident_of_nat " ^ id_s name ^ "))"
    162162 and typelist l =
    163163    let b = Buffer.create 20 in
     
    357357  | Init_int8 n -> fprintf p "(Init_int8 (repr I8 %d))@ " n
    358358  | Init_int16 n -> fprintf p "(Init_int16 (repr I16 %d))@ " n
    359   (*| Init_null r -> fprintf p "(Init_null Any)@"*)
     359  (*| Init_null r -> fprintf p "(Init_null)@"*)
    360360  | Init_int32 n -> fprintf p "(Init_int32 (repr I32 %d))@ " n
    361361  | Init_float32 n -> fprintf p "(Init_float32 %F)@ " n
    362362  | Init_float64 n -> fprintf p "(Iinit_float64 %F)@ " n
    363363  | Init_space n -> fprintf p "(Init_space %d)@ " n
    364   | Init_addrof(symb, ofs) -> fprintf p "(Init_addrof Any (ident_of_nat %i) %d)" (id_i symb) ofs
     364  | Init_addrof(symb, ofs) -> fprintf p "(Init_addrof (ident_of_nat %i) %d)" (id_i symb) ofs
    365365
    366366let re_string_literal = Str.regexp "__stringlit_[0-9]+"
    367367
    368368let print_globvar p (((id, init), ty)) =
    369   fprintf p "@[<hov 2>〈〈ident_of_nat %i (* %s *),@ Any〉,@ 〈%a,@ %s〉〉@]"
     369  fprintf p "@[<hov 2>〈〈ident_of_nat %i (* %s *),@ XData〉,@ 〈%a,@ %s〉〉@]"
    370370    (id_i id)
    371371    id
Note: See TracChangeset for help on using the changeset viewer.