Changeset 2395 for src/Clight
- Timestamp:
- Oct 12, 2012, 3:33:53 PM (9 years ago)
- Location:
- src/Clight
- Files:
-
- 2 added
- 2 edited
- 1 copied
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/Csem.ma
r2391 r2395 348 348 match v2 with 349 349 [ Vptr ptr2 ⇒ 350 if valid_pointer m ptr1 351 ∧ valid_pointer m ptr2 then 352 if eq_block (pblock ptr1) (pblock ptr2) 350 (* Pointers one-off-the-end require careful treatment - they may end 351 up equal to a pointer to another object. I don't think we have 352 the corresponding definitions in the back-end, so we may need to 353 compromise on this; if so, the pointer comparison in FrontEndOps 354 will need changed too. *) 355 if eq_block (pblock ptr1) (pblock ptr2) then 356 if (valid_pointer m ptr1 ∨ end_pointer m ptr1) ∧ 357 (valid_pointer m ptr2 ∨ end_pointer m ptr2) 353 358 then Some ? (of_bool (cmp_offset c (poff ptr1) (poff ptr2))) 354 else sem_cmp_mismatch c 355 else None ? 359 else None ? 360 else 361 if valid_pointer m ptr1 ∧ 362 valid_pointer m ptr2 363 then sem_cmp_mismatch c 364 else None ? 356 365 | Vnull ⇒ sem_cmp_mismatch c 357 366 | _ ⇒ None ? ] -
src/Clight/test/endptr.test.ma
r2393 r2395 1 1 include "Clight/test/endptr.c.ma". 2 2 3 example exec: result ? (exec_up_to clight_fullexec myprog 1000 [ ]).3 example exec: exec_up_to clight_fullexec myprog 1000 [ ] = Error ? (msg FailedOp). 4 4 normalize (* you can examine the result here *) 5 5 % … … 9 9 include "Clight/toCminor.ma". 10 10 include "Cminor/semantics.ma". 11 12 (* This succeeds because the variables have been arranged in the stack frame. *) 11 13 12 14 example e1: result ? -
src/Clight/test/endptr2.test.ma
r2393 r2395 1 include "Clight/test/endptr .c.ma".1 include "Clight/test/endptr2.c.ma". 2 2 3 example exec: result ? (exec_up_to clight_fullexec myprog 1000 [ ]).3 example exec: exec_up_to clight_fullexec myprog 1000 [ ] = Error ? (msg FailedOp). 4 4 normalize (* you can examine the result here *) 5 5 % … … 10 10 include "Cminor/semantics.ma". 11 11 12 example e1: result ?12 example e1: 13 13 (bind ? (snapshot state) (clight_to_cminor (simplify_program myprog)) 14 (λp. exec_up_to Cminor_fullexec p 1000 [ ])). 14 (λp. exec_up_to Cminor_fullexec p 1000 [ ])) 15 = Error ? (msg FailedOp). 15 16 normalize 16 17 % … … 21 22 include "Clight/label.ma". 22 23 23 example e2: result ? (24 example e2: 24 25 let 〈p0,init〉 ≝ clight_label myprog in 25 26 bind ? (snapshot state) (clight_to_cminor (simplify_program p0)) 26 27 (λp1. let p2 ≝ cminor_to_rtlabs init p1 in 27 exec_up_to RTLabs_fullexec p2 1000 [ ])). 28 exec_up_to RTLabs_fullexec p2 1000 [ ]) 29 = Error ? (msg FailedOp). 28 30 normalize 29 31 %
Note: See TracChangeset
for help on using the changeset viewer.