Ignore:
Timestamp:
Jun 15, 2011, 4:15:56 PM (8 years ago)
Author:
campbell
Message:

Update some Clight examples.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/clightPrintMatita.ml

    r786 r965  
    6363  | Ole  -> "Ole"
    6464  | Oge  -> "Oge"
     65
     66let name_intsize = function
     67  | I8  -> "I8"
     68  | I16 -> "I16"
     69  | I32 -> "I32"
    6570
    6671let name_inttype sz sg =
     
    191196
    192197let rec print_expr p (Expr (eb, ty)) =
    193   fprintf p "@[<hov 2>(Expr %a@ %s)@]" print_expr_descr eb (stype ty)
    194 and print_expr_descr p eb =
     198  fprintf p "@[<hov 2>(Expr %a@ %s)@]" (print_expr_descr ty) eb (stype ty)
     199and print_expr_descr ty p eb =
    195200  match eb with
    196   | Ecost (_, Expr (e, _)) -> print_expr_descr p e
     201  | Ecost (_, Expr (e, ty)) -> print_expr_descr ty p e
    197202  | Econst_int n ->
    198       fprintf p "(Econst_int (repr %d))" n
     203      fprintf p "(Econst_int %s (repr ? %d))"
     204        (match ty with Tint (sz, _) -> name_intsize sz | _ -> "I32")
     205        n
    199206  | Econst_float f ->
    200207      fprintf p "(Econst_float %F)" f
     
    294301      fprintf p "@[<v 2>(LSdefault@ %a)@]" print_stmt s
    295302  | LScase(lbl, s, rem) ->
    296       fprintf p "@[<v 2>(LScase (repr %d)@ %a@ %a)@]"
     303      fprintf p "@[<v 2>(LScase I32 (repr ? %d)@ %a@ %a)@]"
    297304              lbl
    298305              print_stmt s
     
    348355
    349356let print_init p = function
    350   | Init_int8 n -> fprintf p "(Init_int8 (repr %d))@ " n
    351   | Init_int16 n -> fprintf p "(Init_int16 (repr %d))@ " n
     357  | Init_int8 n -> fprintf p "(Init_int8 (repr I8 %d))@ " n
     358  | Init_int16 n -> fprintf p "(Init_int16 (repr I16 %d))@ " n
    352359  (*| Init_null r -> fprintf p "(Init_null Any)@"*)
    353   | Init_int32 n -> fprintf p "(Init_int32 (repr %d))@ " n
     360  | Init_int32 n -> fprintf p "(Init_int32 (repr I32 %d))@ " n
    354361  | Init_float32 n -> fprintf p "(Init_float32 %F)@ " n
    355362  | Init_float64 n -> fprintf p "(Iinit_float64 %F)@ " n
    356363  | Init_space n -> fprintf p "(Init_space %d)@ " n
    357   | Init_addrof(symb, ofs) -> fprintf p "(Init_addrof Any (ident_of_nat %i) (repr %d))" (id_i symb) ofs
     364  | Init_addrof(symb, ofs) -> fprintf p "(Init_addrof Any (ident_of_nat %i) %d)" (id_i symb) ofs
    358365
    359366let re_string_literal = Str.regexp "__stringlit_[0-9]+"
     
    466473  print_list print_globvar p prog.prog_vars;
    467474  fprintf p "@;<0 -2>.@]@\n@\n";
    468   fprintf p "example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr 0)]).@\n";
     475  fprintf p "example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).@\n";
    469476  fprintf p "normalize  (* you can examine the result here *)@."
    470477
Note: See TracChangeset for help on using the changeset viewer.