source: src/Clight/test/forcont.c.ma @ 2407

Last change on this file since 2407 was 2407, checked in by campbell, 7 years ago

Sigh, continue in for loops was broken too.

File size: 2.0 KB
Line 
1include "Clight/Cexec.ma".
2include "common/Animation.ma".
3
4definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
5  [][〈ident_of_nat 0 (* main *), CL_Internal (
6       mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 1, (Tint I32 Signed  )〉 ; 〈ident_of_nat 2, (Tint I32 Signed  )〉 ]
7         (Ssequence
8         (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
9           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
10         (Ssequence
11         (Sfor (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
12                 (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
13           (Expr (Ebinop Olt
14             (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
15             (Expr (Econst_int I32 (repr ? 10)) (Tint I32 Signed  )))
16             (Tint I32 Signed  ))
17           (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
18             (Expr (Ebinop Oadd
19               (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
20               (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
21               (Tint I32 Signed  )))
22           (Ssequence
23           (Sifthenelse (Expr (Ebinop Oeq
24                          (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
25                          (Expr (Econst_int I32 (repr ? 1))
26                            (Tint I32 Signed  ))) (Tint I32 Signed  ))
27             Scontinue
28             Sskip)
29           (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
30             (Expr (Ebinop Oadd
31               (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
32               (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
33               (Tint I32 Signed  ))))
34         )
35         (Sreturn (Some expr (Expr (Evar (ident_of_nat 2))
36                               (Tint I32 Signed  ))))))
37       
38       
39       
40     )〉]
41  (ident_of_nat 0)
42 
43.
44
45(*
46example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
47normalize  (* you can examine the result here *)
48*)
Note: See TracBrowser for help on using the repository browser.