Changeset 965


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

Update some Clight examples.

Location:
src/Clight
Files:
2 added
2 deleted
2 edited
2 moved

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
  • src/Clight/test/insertsort.c

    r485 r965  
     1/* Remove memory region for now. */
     2#define __pdata
     3
    14struct list {
    25  unsigned char i;
  • src/Clight/test/null-op.c.ma

    r964 r965  
    99                  (Tpointer Any (Tint I8 Unsigned )))
    1010         (Expr (Ecast (Tpointer Any (Tint I8 Unsigned ))
    11            (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
     11           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    1212           (Tpointer Any (Tint I8 Unsigned ))))
    1313       (Ssequence
     
    2323                        (Tpointer Any (Tint I8 Unsigned ))))
    2424                      (Tint I32 Signed  ))
    25          (Sreturn (Some expr (Expr (Econst_int (repr 0)) (Tint I32 Signed  ))))
     25         (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
     26                               (Tint I32 Signed  ))))
    2627         Sskip)
    2728       (Ssequence
     
    3334                          (Tpointer Any (Tint I8 Unsigned ))))
    3435                        (Tint I32 Signed  ))
    35                       (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
     36                      (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    3637                      (Tint I32 Signed  ))
    37          (Sreturn (Some expr (Expr (Econst_int (repr 0)) (Tint I32 Signed  ))))
     38         (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
     39                               (Tint I32 Signed  ))))
    3840         Sskip)
    3941       (Ssequence
     
    4244         (Expr (Ebinop Oadd
    4345           (Expr (Evar (ident_of_nat 2)) (Tpointer Any (Tint I8 Unsigned )))
    44            (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
     46           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    4547           (Tpointer Any (Tint I8 Unsigned ))))
    4648       (Ssequence
    4749       (Sassign (Expr (Evar (ident_of_nat 2))
    4850                  (Tpointer Any (Tint I8 Unsigned )))
    49          (Expr (Ebinop Oadd (Expr (Econst_int (repr 0)) (Tint I32 Signed  ))
     51         (Expr (Ebinop Oadd
     52           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  ))
    5053           (Expr (Evar (ident_of_nat 2)) (Tpointer Any (Tint I8 Unsigned ))))
    5154           (Tpointer Any (Tint I8 Unsigned ))))
     
    5558         (Expr (Ebinop Osub
    5659           (Expr (Evar (ident_of_nat 2)) (Tpointer Any (Tint I8 Unsigned )))
    57            (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
     60           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    5861           (Tpointer Any (Tint I8 Unsigned ))))
    5962       (Sreturn (Some expr (Expr (Ebinop Oeq
     
    6265                             (Expr (Ecast (Tpointer Any (Tint I8 Unsigned ))
    6366                               (Expr (Ecast (Tpointer Any Tvoid)
    64                                  (Expr (Econst_int (repr 0))
    65                                    (Tint I32 Unsigned)))
     67                                 (Expr (Econst_int I8 (repr ? 0))
     68                                   (Tint I8 Unsigned )))
    6669                                 (Tpointer Any Tvoid)))
    6770                               (Tpointer Any (Tint I8 Unsigned ))))
  • src/Clight/test/sum.c.ma

    r964 r965  
     1include "Clight/Cexec.ma".
    12include "common/Animation.ma".
    2 include "Clight/Cexec.ma".
    33
    44definition myprog := mk_program clight_fundef type
     
    1010           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    1111           (Tint I8 Unsigned )))
    12        (Ssequence
    1312       (Ssequence
    1413       (Sfor (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
     
    3736                       (Tarray Any (Tint I8 Unsigned ) 5))
    3837                     (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  )))
    39                      (Tarray Any (Tint I8 Unsigned ) 5)))
     38                     (Tpointer Any (Tint I8 Unsigned ))))
    4039                   (Tint I8 Unsigned ))) (Tint I32 Signed  )))
    4140               (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    4241       )
    43        Sskip)
    4442       (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
    4543                             (Expr (Evar (ident_of_nat 2))
     
    5149  (ident_of_nat 0)
    5250  [〈〈〈ident_of_nat 3 (* src *),
    53      [(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ; (Init_int8 (repr I8 17)) ;
    54      (Init_int8 (repr I8 8)) ; (Init_int8 (repr I8 4)) ]〉, Any〉,
     51     [(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ;
     52     (Init_int8 (repr I8 17)) ; (Init_int8 (repr I8 8)) ;
     53     (Init_int8 (repr I8 4)) ]〉, Any〉,
    5554     (Tarray Any (Tint I8 Unsigned ) 5)〉]
    5655.
     
    6463include "Cminor/semantics.ma".
    6564
    66 example e1: finishes_with (repr 74) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
     65example e1: finishes_with (repr I32 74) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
    6766normalize
    6867@refl
     
    7271include "RTLabs/semantics.ma".
    7372
    74 example e2: finishes_with (repr 74) ? (
     73example e2: finishes_with (repr I32 74) ? (
    7574do p1 ← clight_to_cminor myprog;
    7675do p2 ← cminor_to_rtlabs p1;
Note: See TracChangeset for help on using the changeset viewer.