Changeset 2176 for src/Clight/test/sum.c.ma

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:

• src/Clight/test/sum.c.ma (modified) (3 diffs)

src/Clight/test/sum.c.ma

@@ -3 +3 @@
 
 definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
-  [〈〈ident_of_nat 0 (* src *), Any〉,
+  [〈〈ident_of_nat 0 (* src *), XData〉,
      〈[(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ;
         (Init_int8 (repr I8 17)) ; (Init_int8 (repr I8 8)) ;
-        (Init_int8 (repr I8 4)) ], (Tarray Any (Tint I8 Unsigned ) 5)〉〉]
+        (Init_int8 (repr I8 4)) ], (Tarray (Tint I8 Unsigned ) 5)〉〉]
   [〈ident_of_nat 1 (* main *), CL_Internal (
      mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 2, (Tint I32 Signed  )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ]
@@ -21 +21 @@
              (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
              (Tint I32 Unsigned))
-           (Expr (Esizeof (Tarray Any (Tint I8 Unsigned ) 5))
+           (Expr (Esizeof (Tarray (Tint I8 Unsigned ) 5))
              (Tint I32 Unsigned))) (Tint I32 Signed  ))
          (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
@@ -38 +38 @@
                    (Expr (Ebinop Oadd
                      (Expr (Evar (ident_of_nat 0))
-                       (Tarray Any (Tint I8 Unsigned ) 5))
+                       (Tarray (Tint I8 Unsigned ) 5))
                      (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
-                     (Tpointer Any (Tint I8 Unsigned ))))
-                   (Tint I8 Unsigned ))) (Tint I32 Signed  )))
-               (Tint I32 Signed  ))) (Tint I8 Unsigned )))
+                     (Tpointer (Tint I8 Unsigned )))) (Tint I8 Unsigned )))
+                 (Tint I32 Signed  ))) (Tint I32 Signed  )))
+             (Tint I8 Unsigned )))
        )
        (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )