Last change
on this file since 1226 was
1226,
checked in by campbell, 8 years ago

Adjust pretty printers for change in program records, try a test of each.

File size:
862 bytes

Line  

1  include "Clight/test/sum.c.ma". 

2  

3  example exec: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec myprog 1000 [ ]). 

4  normalize (* you can examine the result here *) 

5  @refl 

6  qed. 

7  

8  include "Clight/SimplifyCasts.ma". 

9  

10  example es: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec (simplify_program myprog) 1000 [ ]). 

11  normalize (* you can examine the result here *) 

12  @refl 

13  qed. 

14  

15  include "Clight/toCminor.ma". 

16  include "Cminor/semantics.ma". 

17  

18  example e1: finishes_with (repr I32 74) ? (do p ← clight_to_cminor (simplify_program myprog); exec_up_to Cminor_fullexec p 1000 [ ]). 

19  normalize 

20  @refl 

21  qed. 

22  

23  include "Cminor/toRTLabs.ma". 

24  include "RTLabs/semantics.ma". 

25  

26  example e2: finishes_with (repr I32 74) ? ( 

27  do p1 ← clight_to_cminor (simplify_program myprog); 

28  do p2 ← cminor_to_rtlabs p1; 

29  exec_up_to RTLabs_fullexec p2 1000 [ ]). 

30  normalize 

31  @refl 

32  qed. 

Note: See
TracBrowser
for help on using the repository browser.