Changeset 1139 for src/Clight/test
- Timestamp:
- Aug 30, 2011, 12:47:18 PM (10 years ago)
- Location:
- src/Clight/test
- Files:
-
- 3 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/test/insertsort.c.ma
r965 r1139 5 5 generate Init_null at the moment. *) 6 6 7 definition myprog := mk_program clight_fundef type7 definition myprog := mk_program clight_fundef ((list init_data) × type) 8 8 [〈ident_of_nat 0 (* insert *), CL_Internal ( 9 9 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 )〉] 168 168 (ident_of_nat 12) 169 [〈〈〈ident_of_nat 15 (* l6 *), 170 [(Init_int8 (repr I8 69)) ; (Init_space 3) ; (Init_null Any) ]〉, 171 Any〉, 172 (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)))〉; 173 〈〈〈ident_of_nat 16 (* l5 *), 174 [(Init_int8 (repr I8 36)) ; (Init_space 3) ; 175 (Init_addrof Any (ident_of_nat 15) 0)]〉, Any〉, 176 (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)))〉; 177 〈〈〈ident_of_nat 17 (* l4 *), 178 [(Init_int8 (repr I8 136)) ; (Init_space 3) ; 179 (Init_addrof Any (ident_of_nat 16) 0)]〉, Any〉, 180 (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)))〉; 181 〈〈〈ident_of_nat 18 (* l3 *), 182 [(Init_int8 (repr I8 105)) ; (Init_space 3) ; 183 (Init_addrof Any (ident_of_nat 17) 0)]〉, Any〉, 184 (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)))〉; 185 〈〈〈ident_of_nat 19 (* l2 *), 186 [(Init_int8 (repr I8 234)) ; (Init_space 3) ; 187 (Init_addrof Any (ident_of_nat 18) 0)]〉, Any〉, 188 (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)))〉; 189 〈〈〈ident_of_nat 20 (* l1 *), 190 [(Init_int8 (repr I8 240)) ; (Init_space 3) ; 191 (Init_addrof Any (ident_of_nat 19) 0)]〉, Any〉, 192 (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)))〉; 193 〈〈〈ident_of_nat 14 (* l0 *), 194 [(Init_int8 (repr I8 102)) ; (Init_space 3) ; 195 (Init_addrof Any (ident_of_nat 20) 0)]〉, Any〉, 196 (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)))〉] 169 [〈〈ident_of_nat 15 (* l6 *), Any〉, 170 〈[(Init_int8 (repr I8 69)) ; (Init_space 3) ; (Init_null Any) ], 171 (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)))〉〉; 172 〈〈ident_of_nat 16 (* l5 *), Any〉, 173 〈[(Init_int8 (repr I8 36)) ; (Init_space 3) ; 174 (Init_addrof Any (ident_of_nat 15) 0)], 175 (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)))〉〉; 176 〈〈ident_of_nat 17 (* l4 *), Any〉, 177 〈[(Init_int8 (repr I8 136)) ; (Init_space 3) ; 178 (Init_addrof Any (ident_of_nat 16) 0)], 179 (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)))〉〉; 180 〈〈ident_of_nat 18 (* l3 *), Any〉, 181 〈[(Init_int8 (repr I8 105)) ; (Init_space 3) ; 182 (Init_addrof Any (ident_of_nat 17) 0)], 183 (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)))〉〉; 184 〈〈ident_of_nat 19 (* l2 *), Any〉, 185 〈[(Init_int8 (repr I8 234)) ; (Init_space 3) ; 186 (Init_addrof Any (ident_of_nat 18) 0)], 187 (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)))〉〉; 188 〈〈ident_of_nat 20 (* l1 *), Any〉, 189 〈[(Init_int8 (repr I8 240)) ; (Init_space 3) ; 190 (Init_addrof Any (ident_of_nat 19) 0)], 191 (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)))〉〉; 192 〈〈ident_of_nat 14 (* l0 *), Any〉, 193 〈[(Init_int8 (repr I8 102)) ; (Init_space 3) ; 194 (Init_addrof Any (ident_of_nat 20) 0)], 195 (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)))〉〉] 197 196 . 198 197 -
src/Clight/test/search.c.ma
r978 r1139 2 2 include "common/Animation.ma". 3 3 4 definition myprog := mk_program clight_fundef type4 definition myprog := mk_program clight_fundef ((list init_data) × type) 5 5 [〈ident_of_nat 0 (* search *), CL_Internal ( 6 6 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
r965 r1139 2 2 include "common/Animation.ma". 3 3 4 definition myprog := mk_program clight_fundef type4 definition myprog := mk_program clight_fundef (list init_data × type) 5 5 [〈ident_of_nat 0 (* main *), CL_Internal ( 6 6 mk_function (Tint I32 Signed ) [] [〈ident_of_nat 1, (Tint I32 Signed )〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ] … … 48 48 )〉] 49 49 (ident_of_nat 0) 50 [〈〈 〈ident_of_nat 3 (* src *),51 [(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ;50 [〈〈ident_of_nat 3 (* src *), Any〉, 51 〈[(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ; 52 52 (Init_int8 (repr I8 17)) ; (Init_int8 (repr I8 8)) ; 53 (Init_int8 (repr I8 4)) ] 〉, Any〉,54 (Tarray Any (Tint I8 Unsigned ) 5)〉 ]53 (Init_int8 (repr I8 4)) ], 54 (Tarray Any (Tint I8 Unsigned ) 5)〉〉] 55 55 . 56 56
Note: See TracChangeset
for help on using the changeset viewer.