1 | include "Clight/test/implicitcond.c.ma". |
---|

2 | |
---|

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

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

5 | % |
---|

6 | qed. |
---|

7 | |
---|

8 | include "Clight/SimplifyCasts.ma". |
---|

9 | |
---|

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

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

12 | % |
---|

13 | qed. |
---|

14 | |
---|

15 | include "Clight/toCminor.ma". |
---|

16 | include "Cminor/Cminor_semantics.ma". |
---|

17 | |
---|

18 | example e1: finishes_with (repr I32 2) ? |
---|

19 | (bind ? (snapshot state) (clight_to_cminor (simplify_program myprog)) |
---|

20 | (λp. exec_up_to Cminor_fullexec p 1000 [ ])). |
---|

21 | normalize |
---|

22 | % |
---|

23 | qed. |
---|

24 | |
---|

25 | include "Cminor/toRTLabs.ma". |
---|

26 | include "RTLabs/RTLabs_semantics.ma". |
---|

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

28 | |
---|

29 | example e2: finishes_with (repr I32 2) ? ( |
---|

30 | let 〈p0,init〉 ≝ clight_label myprog in |
---|

31 | bind ? (snapshot state) (clight_to_cminor (simplify_program p0)) |
---|

32 | (λp1. let p2 ≝ cminor_to_rtlabs init p1 in |
---|

33 | exec_up_to RTLabs_fullexec p2 1000 [ ])). |
---|

34 | normalize |
---|

35 | % |
---|

36 | qed. |
---|

37 | |
---|

38 | include "RTLabs/CostCheck.ma". |
---|

39 | |
---|

40 | definition readable_body ≝ |
---|

41 | λfn. insert_sort ? |
---|

42 | (λx,y. leb (succ (match \fst x with [an_identifier z ⇒ z])) (match \fst y with [an_identifier z ⇒ z])) |
---|

43 | (elements ?? (f_graph fn)). |
---|

44 | (* |
---|

45 | example c2: result ? ( |
---|

46 | let 〈p0,init〉 ≝ clight_label myprog in |
---|

47 | ! p1 ← clight_to_cminor (simplify_program p0); |
---|

48 | let p2 ≝ cminor_to_rtlabs init p1 in |
---|

49 | match prog_funct … p2 with |
---|

50 | [ nil ⇒ Error ? (msg MISSING) |
---|

51 | | cons h _ ⇒ |
---|

52 | match \snd h with |
---|

53 | [ External _ ⇒ Error ? (msg EXTERNAL) |
---|

54 | | Internal fn ⇒ return 〈pi1 … (f_entry fn), readable_body fn〉 |
---|

55 | ] |
---|

56 | ]). |
---|

57 | normalize |
---|

58 | *) |
---|

59 | example c2: ( |
---|

60 | let 〈p0,init〉 ≝ clight_label myprog in |
---|

61 | ! p1 ← clight_to_cminor (simplify_program p0); |
---|

62 | let p2 ≝ cminor_to_rtlabs init p1 in |
---|

63 | return (check_cost_program p2)) = OK bool true. |
---|

64 | normalize |
---|

65 | % |
---|

66 | qed. |
---|

67 | |
---|

68 | |
---|