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

2 | |
---|

3 | example exec: finishes_with (repr I32 15) ? (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 | include "Clight/switchRemoval.ma". |
---|

10 | |
---|

11 | example es: finishes_with (repr I32 15) ? (exec_up_to clight_fullexec (program_switch_removal (simplify_program myprog)) 1000 [ ]). |
---|

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

13 | % |
---|

14 | qed. |
---|

15 | |
---|

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

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

18 | |
---|

19 | example e1: finishes_with (repr I32 15) ? |
---|

20 | (bind ? (snapshot state) (clight_to_cminor (program_switch_removal (simplify_program myprog))) |
---|

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

22 | normalize |
---|

23 | % |
---|

24 | qed. |
---|

25 | |
---|

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

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

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

29 | |
---|

30 | example e2: finishes_with (repr I32 15) ? ( |
---|

31 | let 〈p0,init〉 ≝ clight_label (program_switch_removal myprog) in |
---|

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

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

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

35 | normalize |
---|

36 | % |
---|

37 | qed. |
---|

38 | |
---|

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

40 | |
---|

41 | definition readable_body ≝ |
---|

42 | λfn. insert_sort ? |
---|

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

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

45 | (* |
---|

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

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

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

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

50 | match prog_funct … p2 with |
---|

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

52 | | cons h _ ⇒ |
---|

53 | match \snd h with |
---|

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

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

56 | ] |
---|

57 | ]). |
---|

58 | normalize |
---|

59 | *) |
---|

60 | example c2: ( |
---|

61 | let 〈p0,init〉 ≝ clight_label (program_switch_removal myprog) in |
---|

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

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

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

65 | normalize |
---|

66 | % |
---|

67 | qed. |
---|

68 | |
---|

69 | |
---|