source: src/Clight/test/sum.test.ma @ 1332

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

Summation example updated (needs computational K).

File size: 936 bytes
Line 
1include "Clight/test/sum.c.ma".
2
3example exec: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
4normalize  (* you can examine the result here *)
5@refl
6qed.
7
8include "Clight/SimplifyCasts.ma".
9
10example es: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec (simplify_program myprog) 1000 [ ]).
11normalize  (* you can examine the result here *)
12@refl
13qed.
14
15include "Clight/toCminor.ma".
16include "Cminor/semantics.ma".
17
18example e1: finishes_with (repr I32 74) ?
19  (bind ? (snapshot state) (clight_to_cminor (simplify_program myprog))
20   (λp. exec_up_to Cminor_fullexec p 1000 [ ])).
21normalize
22@refl
23qed.
24
25include "Cminor/toRTLabs.ma".
26include "RTLabs/semantics.ma".
27
28example e2: finishes_with (repr I32 74) ? (
29bind ? (snapshot state) (clight_to_cminor (simplify_program myprog))
30(λp1. bind ? (snapshot state) (cminor_to_rtlabs p1)
31 (λp2. exec_up_to RTLabs_fullexec p2 1000 [ ]))).
32normalize
33@refl
34qed.
Note: See TracBrowser for help on using the repository browser.