source: src/Clight/test/badconditional.c.ma @ 2771

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

Add conditional test case that also uses switch removal.

File size: 2.9 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 (* f *), CL_Internal (
6       mk_function (Tint I32 Signed  ) [〈ident_of_nat 3, (Tint I32 Signed  )〉 ] [〈ident_of_nat 1, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tint I32 Signed  )〉 ]
7         (Ssequence
8         (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))
9           (Expr (Ecast (Tint I8 Unsigned )
10             (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
11             (Tint I8 Unsigned )))
12         (Ssequence
13         (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
14           (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
15         (Sswitch (Expr (Econdition (Expr (Evar (ident_of_nat 3))
16                                      (Tint I32 Signed  ))
17                    (Expr (Ecast (Tint I32 Signed  )
18                      (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
19                      (Tint I32 Signed  ))
20                    (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
21                    (Tint I32 Signed  )) (
22           (LScase I32 (repr ? 1)
23             (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 5))
24                                   (Tint I32 Signed  ))))
25             (LScase I32 (repr ? 2)
26               (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 10))
27                                     (Tint I32 Signed  ))))
28               (LSdefault
29                 (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
30                                       (Tint I32 Signed  )))))))
31         ))))
32       
33       
34       
35     )〉;
36    〈ident_of_nat 4 (* main *), CL_Internal (
37      mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 5, (Tint I32 Signed  )〉 ; 〈ident_of_nat 6, (Tint I32 Signed  )〉 ]
38        (Ssequence
39        (Ssequence
40        (Scall (Some expr (Expr (Evar (ident_of_nat 5)) (Tint I32 Signed  )))
41          (Expr (Evar (ident_of_nat 0))
42            (Tfunction (Tcons (Tint I32 Signed  ) Tnil) (Tint I32 Signed  )))
43          [(Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  ))])
44        (Scall (Some expr (Expr (Evar (ident_of_nat 6)) (Tint I32 Signed  )))
45          (Expr (Evar (ident_of_nat 0))
46            (Tfunction (Tcons (Tint I32 Signed  ) Tnil) (Tint I32 Signed  )))
47          [(Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  ))]))
48        (Sreturn (Some expr (Expr (Ebinop Oadd
49                              (Expr (Evar (ident_of_nat 5))
50                                (Tint I32 Signed  ))
51                              (Expr (Evar (ident_of_nat 6))
52                                (Tint I32 Signed  ))) (Tint I32 Signed  )))))
53     
54     
55     
56    )〉]
57  (ident_of_nat 4)
58 
59.
60
61(*
62example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
63normalize  (* you can examine the result here *)
64*)
Note: See TracBrowser for help on using the repository browser.