- Timestamp:
- Jun 15, 2011, 4:15:56 PM (10 years ago)
- Location:
- src/Clight
- Files:
-
- 2 added
- 2 deleted
- 2 edited
- 2 moved
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/clightPrintMatita.ml
r786 r965 63 63 | Ole -> "Ole" 64 64 | Oge -> "Oge" 65 66 let name_intsize = function 67 | I8 -> "I8" 68 | I16 -> "I16" 69 | I32 -> "I32" 65 70 66 71 let name_inttype sz sg = … … 191 196 192 197 let rec print_expr p (Expr (eb, ty)) = 193 fprintf p "@[<hov 2>(Expr %a@ %s)@]" print_expr_descreb (stype ty)194 and print_expr_descr p eb =198 fprintf p "@[<hov 2>(Expr %a@ %s)@]" (print_expr_descr ty) eb (stype ty) 199 and print_expr_descr ty p eb = 195 200 match eb with 196 | Ecost (_, Expr (e, _)) -> print_expr_descrp e201 | Ecost (_, Expr (e, ty)) -> print_expr_descr ty p e 197 202 | 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 199 206 | Econst_float f -> 200 207 fprintf p "(Econst_float %F)" f … … 294 301 fprintf p "@[<v 2>(LSdefault@ %a)@]" print_stmt s 295 302 | 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)@]" 297 304 lbl 298 305 print_stmt s … … 348 355 349 356 let print_init p = function 350 | Init_int8 n -> fprintf p "(Init_int8 (repr %d))@ " n351 | Init_int16 n -> fprintf p "(Init_int16 (repr %d))@ " n357 | Init_int8 n -> fprintf p "(Init_int8 (repr I8 %d))@ " n 358 | Init_int16 n -> fprintf p "(Init_int16 (repr I16 %d))@ " n 352 359 (*| Init_null r -> fprintf p "(Init_null Any)@"*) 353 | Init_int32 n -> fprintf p "(Init_int32 (repr %d))@ " n360 | Init_int32 n -> fprintf p "(Init_int32 (repr I32 %d))@ " n 354 361 | Init_float32 n -> fprintf p "(Init_float32 %F)@ " n 355 362 | Init_float64 n -> fprintf p "(Iinit_float64 %F)@ " n 356 363 | 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) ofs364 | Init_addrof(symb, ofs) -> fprintf p "(Init_addrof Any (ident_of_nat %i) %d)" (id_i symb) ofs 358 365 359 366 let re_string_literal = Str.regexp "__stringlit_[0-9]+" … … 466 473 print_list print_globvar p prog.prog_vars; 467 474 fprintf p "@;<0 -2>.@]@\n@\n"; 468 fprintf p "example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr0)]).@\n";475 fprintf p "example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).@\n"; 469 476 fprintf p "normalize (* you can examine the result here *)@." 470 477 -
src/Clight/test/insertsort.c
r485 r965 1 /* Remove memory region for now. */ 2 #define __pdata 3 1 4 struct list { 2 5 unsigned char i; -
src/Clight/test/null-op.c.ma
r964 r965 9 9 (Tpointer Any (Tint I8 Unsigned ))) 10 10 (Expr (Ecast (Tpointer Any (Tint I8 Unsigned )) 11 (Expr (Econst_int (repr0)) (Tint I32 Signed )))11 (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed ))) 12 12 (Tpointer Any (Tint I8 Unsigned )))) 13 13 (Ssequence … … 23 23 (Tpointer Any (Tint I8 Unsigned )))) 24 24 (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 )))) 26 27 Sskip) 27 28 (Ssequence … … 33 34 (Tpointer Any (Tint I8 Unsigned )))) 34 35 (Tint I32 Signed )) 35 (Expr (Econst_int (repr0)) (Tint I32 Signed )))36 (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed ))) 36 37 (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 )))) 38 40 Sskip) 39 41 (Ssequence … … 42 44 (Expr (Ebinop Oadd 43 45 (Expr (Evar (ident_of_nat 2)) (Tpointer Any (Tint I8 Unsigned ))) 44 (Expr (Econst_int (repr0)) (Tint I32 Signed )))46 (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed ))) 45 47 (Tpointer Any (Tint I8 Unsigned )))) 46 48 (Ssequence 47 49 (Sassign (Expr (Evar (ident_of_nat 2)) 48 50 (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 )) 50 53 (Expr (Evar (ident_of_nat 2)) (Tpointer Any (Tint I8 Unsigned )))) 51 54 (Tpointer Any (Tint I8 Unsigned )))) … … 55 58 (Expr (Ebinop Osub 56 59 (Expr (Evar (ident_of_nat 2)) (Tpointer Any (Tint I8 Unsigned ))) 57 (Expr (Econst_int (repr0)) (Tint I32 Signed )))60 (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed ))) 58 61 (Tpointer Any (Tint I8 Unsigned )))) 59 62 (Sreturn (Some expr (Expr (Ebinop Oeq … … 62 65 (Expr (Ecast (Tpointer Any (Tint I8 Unsigned )) 63 66 (Expr (Ecast (Tpointer Any Tvoid) 64 (Expr (Econst_int (repr0))65 (Tint I 32 Unsigned)))67 (Expr (Econst_int I8 (repr ? 0)) 68 (Tint I8 Unsigned ))) 66 69 (Tpointer Any Tvoid))) 67 70 (Tpointer Any (Tint I8 Unsigned )))) -
src/Clight/test/sum.c.ma
r964 r965 1 include "Clight/Cexec.ma". 1 2 include "common/Animation.ma". 2 include "Clight/Cexec.ma".3 3 4 4 definition myprog := mk_program clight_fundef type … … 10 10 (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed ))) 11 11 (Tint I8 Unsigned ))) 12 (Ssequence13 12 (Ssequence 14 13 (Sfor (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed )) … … 37 36 (Tarray Any (Tint I8 Unsigned ) 5)) 38 37 (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed ))) 39 (T array Any (Tint I8 Unsigned ) 5)))38 (Tpointer Any (Tint I8 Unsigned )))) 40 39 (Tint I8 Unsigned ))) (Tint I32 Signed ))) 41 40 (Tint I32 Signed ))) (Tint I8 Unsigned ))) 42 41 ) 43 Sskip)44 42 (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed ) 45 43 (Expr (Evar (ident_of_nat 2)) … … 51 49 (ident_of_nat 0) 52 50 [〈〈〈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〉, 55 54 (Tarray Any (Tint I8 Unsigned ) 5)〉] 56 55 . … … 64 63 include "Cminor/semantics.ma". 65 64 66 example e1: finishes_with (repr 74) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).65 example e1: finishes_with (repr I32 74) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]). 67 66 normalize 68 67 @refl … … 72 71 include "RTLabs/semantics.ma". 73 72 74 example e2: finishes_with (repr 74) ? (73 example e2: finishes_with (repr I32 74) ? ( 75 74 do p1 ← clight_to_cminor myprog; 76 75 do p2 ← cminor_to_rtlabs p1;
Note: See TracChangeset
for help on using the changeset viewer.