1 | (* Note that the c.ma file needs tweaked to have an Init_null at the end of the |
---|

2 | list because acc doesn't use them *) |
---|

3 | |
---|

4 | include "Clight/test/insertsort.c.ma". |
---|

5 | |
---|

6 | (* The id for the function which outputs the sorted list. *) |
---|

7 | definition f_id ≝ 18. |
---|

8 | |
---|

9 | example exec: |
---|

10 | (do s ← exec_up_to clight_fullexec myprog 1000 |
---|

11 | [EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0)]; |
---|

12 | match s with [ finished t _ _ ⇒ OK ? t | _ ⇒ Error ? [ ] ]) = OK ? |
---|

13 | [EVextcall (ident_of_nat f_id) [EVint I8 (repr ? 36)] (EVint I32 (repr ? 0)); |
---|

14 | EVextcall (ident_of_nat f_id) [EVint I8 (repr ? 69)] (EVint I32 (repr ? 0)); |
---|

15 | EVextcall (ident_of_nat f_id) [EVint I8 (repr ? 102)] (EVint I32 (repr ? 0)); |
---|

16 | EVextcall (ident_of_nat f_id) [EVint I8 (repr ? 105)] (EVint I32 (repr ? 0)); |
---|

17 | EVextcall (ident_of_nat f_id) [EVint I8 (repr ? 136)] (EVint I32 (repr ? 0)); |
---|

18 | EVextcall (ident_of_nat f_id) [EVint I8 (repr ? 234)] (EVint I32 (repr ? 0)); |
---|

19 | EVextcall (ident_of_nat f_id) [EVint I8 (repr ? 240)] (EVint I32 (repr ? 0))] |
---|

20 | . |
---|

21 | normalize (* you can examine the result here *) |
---|

22 | @refl |
---|

23 | qed. |
---|

24 | |
---|

25 | include "Clight/label.ma". |
---|

26 | |
---|

27 | example labelled_exec: |
---|

28 | (let p ≝ clight_label myprog in |
---|

29 | do s ← exec_up_to clight_fullexec p 1000 |
---|

30 | [EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0)]; |
---|

31 | match s with [ finished t _ _ ⇒ OK ? (remove_costs t) | _ ⇒ Error ? [ ] ]) = OK ? |
---|

32 | [EVextcall (ident_of_nat f_id) [EVint I8 (repr ? 36)] (EVint I32 (repr ? 0)); |
---|

33 | EVextcall (ident_of_nat f_id) [EVint I8 (repr ? 69)] (EVint I32 (repr ? 0)); |
---|

34 | EVextcall (ident_of_nat f_id) [EVint I8 (repr ? 102)] (EVint I32 (repr ? 0)); |
---|

35 | EVextcall (ident_of_nat f_id) [EVint I8 (repr ? 105)] (EVint I32 (repr ? 0)); |
---|

36 | EVextcall (ident_of_nat f_id) [EVint I8 (repr ? 136)] (EVint I32 (repr ? 0)); |
---|

37 | EVextcall (ident_of_nat f_id) [EVint I8 (repr ? 234)] (EVint I32 (repr ? 0)); |
---|

38 | EVextcall (ident_of_nat f_id) [EVint I8 (repr ? 240)] (EVint I32 (repr ? 0))] |
---|

39 | . |
---|

40 | normalize (* you can examine the result here *) |
---|

41 | @refl |
---|

42 | qed. |
---|