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/test/sum.c.ma

    r1226 r2176  
    33
    44definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
    5   [〈〈ident_of_nat 0 (* src *), Any〉,
     5  [〈〈ident_of_nat 0 (* src *), XData〉,
    66     〈[(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ;
    77        (Init_int8 (repr I8 17)) ; (Init_int8 (repr I8 8)) ;
    8         (Init_int8 (repr I8 4)) ], (Tarray Any (Tint I8 Unsigned ) 5)〉〉]
     8        (Init_int8 (repr I8 4)) ], (Tarray (Tint I8 Unsigned ) 5)〉〉]
    99  [〈ident_of_nat 1 (* main *), CL_Internal (
    1010     mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 2, (Tint I32 Signed  )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ]
     
    2121             (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
    2222             (Tint I32 Unsigned))
    23            (Expr (Esizeof (Tarray Any (Tint I8 Unsigned ) 5))
     23           (Expr (Esizeof (Tarray (Tint I8 Unsigned ) 5))
    2424             (Tint I32 Unsigned))) (Tint I32 Signed  ))
    2525         (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
     
    3838                   (Expr (Ebinop Oadd
    3939                     (Expr (Evar (ident_of_nat 0))
    40                        (Tarray Any (Tint I8 Unsigned ) 5))
     40                       (Tarray (Tint I8 Unsigned ) 5))
    4141                     (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
    42                      (Tpointer Any (Tint I8 Unsigned ))))
    43                    (Tint I8 Unsigned ))) (Tint I32 Signed  )))
    44                (Tint I32 Signed  ))) (Tint I8 Unsigned )))
     42                     (Tpointer (Tint I8 Unsigned )))) (Tint I8 Unsigned )))
     43                 (Tint I32 Signed ))) (Tint I32 Signed  )))
     44             (Tint I8 Unsigned )))
    4545       )
    4646       (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
Note: See TracChangeset for help on using the changeset viewer.