Last change
on this file since 2253 was
2253,
checked in by campbell, 9 years ago

Cminor to RTLabs is now a total function.

File size:
1.1 KB

Line  

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

2  

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

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

5  % 

6  qed. 

7  

8  include "Clight/label.ma". 

9  

10  definition myprog' ≝ clight_label myprog. 

11  

12  example el: finishes_with (repr I32 0) ? (exec_up_to clight_fullexec myprog' 1000 [ ]). 

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

14  % 

15  qed. 

16  

17  include "Clight/SimplifyCasts.ma". 

18  

19  example es: finishes_with (repr I32 0) ? (exec_up_to clight_fullexec (simplify_program myprog') 1000 [ ]). 

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

21  % 

22  qed. 

23  

24  include "Clight/toCminor.ma". 

25  include "Cminor/semantics.ma". 

26  

27  example e1: finishes_with (repr I32 0) ? 

28  (bind ? (snapshot state) (clight_to_cminor (simplify_program myprog')) 

29  (λp. exec_up_to Cminor_fullexec p 1000 [ ])). 

30  normalize 

31  % 

32  qed. 

33  

34  include "Cminor/toRTLabs.ma". 

35  include "RTLabs/semantics.ma". 

36  

37  example e2: finishes_with (repr I32 0) ? ( 

38  bind ? (snapshot state) (clight_to_cminor (simplify_program myprog')) 

39  (λp1. let p2 ≝ cminor_to_rtlabs p1 in 

40  exec_up_to RTLabs_fullexec p2 1000 [ ])). 

41  normalize 

42  % 

43  qed. 

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