Changeset 1139 for src/Clight/test

Timestamp:

Aug 30, 2011, 12:47:18 PM (10 years ago)

Author:

campbell

Message:

Shift init_data out of generic program record so that it only appears
in programs that contain initialisation data (Clight and Cminor). Other
stages just have the size of each variable and translate it to Init_space
when building the initial state.

Location:

src/Clight/test

Files:

• insertsort.c.ma (modified) (2 diffs)
• search.c.ma (modified) (1 diff)
• sum.c.ma (modified) (2 diffs)

src/Clight/test/insertsort.c.ma

@@ -5 +5 @@
    generate Init_null at the moment. *)
 
-definition myprog := mk_program clight_fundef type
+definition myprog := mk_program clight_fundef ((list init_data) × type)
   [〈ident_of_nat 0 (* insert *), CL_Internal (
      mk_function Tvoid [〈ident_of_nat 2, (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))〉 ; 〈ident_of_nat 6, (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))〉 ] [〈ident_of_nat 1, (Tint I32 Signed  )〉 ]
@@ -167 +167 @@
   )〉]
   (ident_of_nat 12)
-  [〈〈〈ident_of_nat 15 (* l6 *),
-     [(Init_int8 (repr I8 69)) ; (Init_space 3) ; (Init_null Any) ]〉,
-     Any〉,
-     (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉;
-  〈〈〈ident_of_nat 16 (* l5 *),
-    [(Init_int8 (repr I8 36)) ; (Init_space 3) ;
-    (Init_addrof Any (ident_of_nat 15) 0)]〉, Any〉,
-    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉;
-  〈〈〈ident_of_nat 17 (* l4 *),
-    [(Init_int8 (repr I8 136)) ; (Init_space 3) ;
-    (Init_addrof Any (ident_of_nat 16) 0)]〉, Any〉,
-    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉;
-  〈〈〈ident_of_nat 18 (* l3 *),
-    [(Init_int8 (repr I8 105)) ; (Init_space 3) ;
-    (Init_addrof Any (ident_of_nat 17) 0)]〉, Any〉,
-    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉;
-  〈〈〈ident_of_nat 19 (* l2 *),
-    [(Init_int8 (repr I8 234)) ; (Init_space 3) ;
-    (Init_addrof Any (ident_of_nat 18) 0)]〉, Any〉,
-    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉;
-  〈〈〈ident_of_nat 20 (* l1 *),
-    [(Init_int8 (repr I8 240)) ; (Init_space 3) ;
-    (Init_addrof Any (ident_of_nat 19) 0)]〉, Any〉,
-    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉;
-  〈〈〈ident_of_nat 14 (* l0 *),
-    [(Init_int8 (repr I8 102)) ; (Init_space 3) ;
-    (Init_addrof Any (ident_of_nat 20) 0)]〉, Any〉,
-    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉]
+  [〈〈ident_of_nat 15 (* l6 *), Any〉,
+    〈[(Init_int8 (repr I8 69)) ; (Init_space 3) ; (Init_null Any) ], 
+     (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉;
+  〈〈ident_of_nat 16 (* l5 *), Any〉,
+    〈[(Init_int8 (repr I8 36)) ; (Init_space 3) ;
+    (Init_addrof Any (ident_of_nat 15) 0)],
+    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉;
+  〈〈ident_of_nat 17 (* l4 *), Any〉,
+    〈[(Init_int8 (repr I8 136)) ; (Init_space 3) ;
+    (Init_addrof Any (ident_of_nat 16) 0)],
+    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉;
+  〈〈ident_of_nat 18 (* l3 *), Any〉,
+    〈[(Init_int8 (repr I8 105)) ; (Init_space 3) ;
+    (Init_addrof Any (ident_of_nat 17) 0)],
+    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉;
+  〈〈ident_of_nat 19 (* l2 *), Any〉,
+   〈[(Init_int8 (repr I8 234)) ; (Init_space 3) ;
+    (Init_addrof Any (ident_of_nat 18) 0)],
+    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉;
+  〈〈ident_of_nat 20 (* l1 *), Any〉,
+   〈[(Init_int8 (repr I8 240)) ; (Init_space 3) ;
+    (Init_addrof Any (ident_of_nat 19) 0)],
+    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉;
+  〈〈ident_of_nat 14 (* l0 *), Any〉,
+    〈[(Init_int8 (repr I8 102)) ; (Init_space 3) ;
+    (Init_addrof Any (ident_of_nat 20) 0)],
+    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉]
 .
 

src/Clight/test/search.c.ma

@@ -2 +2 @@
 include "common/Animation.ma".
 
-definition myprog := mk_program clight_fundef type
+definition myprog := mk_program clight_fundef ((list init_data) × type)
   [〈ident_of_nat 0 (* search *), CL_Internal (
      mk_function (Tint I8 Unsigned ) [〈ident_of_nat 4, (Tpointer Any (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 5, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 6, (Tint I8 Unsigned )〉 ] [〈ident_of_nat 1, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ]

src/Clight/test/sum.c.ma

@@ -2 +2 @@
 include "common/Animation.ma".
 
-definition myprog := mk_program clight_fundef type
+definition myprog := mk_program clight_fundef (list init_data × type)
   [〈ident_of_nat 0 (* main *), CL_Internal (
      mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 1, (Tint I32 Signed  )〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ]
@@ -48 +48 @@
    )〉]
   (ident_of_nat 0)
-  [〈〈〈ident_of_nat 3 (* src *),
-     [(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ;
+  [〈〈ident_of_nat 3 (* src *), Any〉,
+     〈[(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)) ]〉, Any〉,
-     (Tarray Any (Tint I8 Unsigned ) 5)〉]
+     (Init_int8 (repr I8 4)) ],
+     (Tarray Any (Tint I8 Unsigned ) 5)〉〉]
 .