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/null-op.c.ma

    r1513 r2176  
    44definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
    55  [][〈ident_of_nat 0 (* main *), CL_Internal (
    6        mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 1, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tpointer Any (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 3, (Tpointer Any (Tint I8 Unsigned ))〉 ]
     6       mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 1, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tpointer (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 3, (Tpointer (Tint I8 Unsigned ))〉 ]
    77         (Ssequence
    88         (Sassign (Expr (Evar (ident_of_nat 2))
    9                     (Tpointer Any (Tint I8 Unsigned )))
    10            (Expr (Ecast (Tpointer Any (Tint I8 Unsigned ))
     9                    (Tpointer (Tint I8 Unsigned )))
     10           (Expr (Ecast (Tpointer (Tint I8 Unsigned ))
    1111             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    12              (Tpointer Any (Tint I8 Unsigned ))))
     12             (Tpointer (Tint I8 Unsigned ))))
    1313         (Ssequence
    1414         (Sassign (Expr (Evar (ident_of_nat 3))
    15                     (Tpointer Any (Tint I8 Unsigned )))
     15                    (Tpointer (Tint I8 Unsigned )))
    1616           (Expr (Eaddrof (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
    17              (Tpointer Any (Tint I8 Unsigned ))))
     17             (Tpointer (Tint I8 Unsigned ))))
    1818         (Ssequence
    1919         (Sifthenelse (Expr (Ebinop Oeq
    2020                        (Expr (Evar (ident_of_nat 2))
    21                           (Tpointer Any (Tint I8 Unsigned )))
     21                          (Tpointer (Tint I8 Unsigned )))
    2222                        (Expr (Evar (ident_of_nat 3))
    23                           (Tpointer Any (Tint I8 Unsigned ))))
     23                          (Tpointer (Tint I8 Unsigned ))))
    2424                        (Tint I32 Signed  ))
    2525           (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
     
    3030                        (Expr (Ebinop Osub
    3131                          (Expr (Evar (ident_of_nat 2))
    32                             (Tpointer Any (Tint I8 Unsigned )))
     32                            (Tpointer (Tint I8 Unsigned )))
    3333                          (Expr (Evar (ident_of_nat 2))
    34                             (Tpointer Any (Tint I8 Unsigned ))))
     34                            (Tpointer (Tint I8 Unsigned ))))
    3535                          (Tint I32 Signed  ))
    3636                        (Expr (Econst_int I32 (repr ? 0))
     
    4141         (Ssequence
    4242         (Sassign (Expr (Evar (ident_of_nat 2))
    43                     (Tpointer Any (Tint I8 Unsigned )))
     43                    (Tpointer (Tint I8 Unsigned )))
    4444           (Expr (Ebinop Oadd
    45              (Expr (Evar (ident_of_nat 2))
    46                (Tpointer Any (Tint I8 Unsigned )))
     45             (Expr (Evar (ident_of_nat 2)) (Tpointer (Tint I8 Unsigned )))
    4746             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    48              (Tpointer Any (Tint I8 Unsigned ))))
     47             (Tpointer (Tint I8 Unsigned ))))
    4948         (Ssequence
    5049         (Sassign (Expr (Evar (ident_of_nat 2))
    51                     (Tpointer Any (Tint I8 Unsigned )))
     50                    (Tpointer (Tint I8 Unsigned )))
    5251           (Expr (Ebinop Oadd
    5352             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  ))
    54              (Expr (Evar (ident_of_nat 2))
    55                (Tpointer Any (Tint I8 Unsigned ))))
    56              (Tpointer Any (Tint I8 Unsigned ))))
     53             (Expr (Evar (ident_of_nat 2)) (Tpointer (Tint I8 Unsigned ))))
     54             (Tpointer (Tint I8 Unsigned ))))
    5755         (Ssequence
    5856         (Sassign (Expr (Evar (ident_of_nat 2))
    59                     (Tpointer Any (Tint I8 Unsigned )))
     57                    (Tpointer (Tint I8 Unsigned )))
    6058           (Expr (Ebinop Osub
    61              (Expr (Evar (ident_of_nat 2))
    62                (Tpointer Any (Tint I8 Unsigned )))
     59             (Expr (Evar (ident_of_nat 2)) (Tpointer (Tint I8 Unsigned )))
    6360             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    64              (Tpointer Any (Tint I8 Unsigned ))))
     61             (Tpointer (Tint I8 Unsigned ))))
    6562         (Sreturn (Some expr (Expr (Ebinop Oeq
    6663                               (Expr (Evar (ident_of_nat 2))
    67                                  (Tpointer Any (Tint I8 Unsigned )))
    68                                (Expr (Ecast (Tpointer Any (Tint I8 Unsigned ))
    69                                  (Expr (Ecast (Tpointer Any Tvoid)
     64                                 (Tpointer (Tint I8 Unsigned )))
     65                               (Expr (Ecast (Tpointer (Tint I8 Unsigned ))
     66                                 (Expr (Ecast (Tpointer Tvoid)
    7067                                   (Expr (Econst_int I8 (repr ? 0))
    71                                      (Tint I8 Unsigned )))
    72                                    (Tpointer Any Tvoid)))
    73                                  (Tpointer Any (Tint I8 Unsigned ))))
     68                                     (Tint I8 Unsigned ))) (Tpointer Tvoid)))
     69                                 (Tpointer (Tint I8 Unsigned ))))
    7470                               (Tint I32 Signed  )))))))))))
    7571       
Note: See TracChangeset for help on using the changeset viewer.