source: Deliverables/D3.1/C-semantics/test/funptr.ma @ 457

Last change on this file since 457 was 457, checked in by campbell, 10 years ago

Correct checking of function pointers.

File size: 2.0 KB
Line 
1include "Animation.ma".
2
3ndefinition myprog := mk_program fundef type
4  [mk_pair ?? (succ_pos_of_nat 0 (* g *)) (Internal (
5     mk_function (Tint I32 Signed  ) [mk_pair ?? (succ_pos_of_nat 1) (Tint I8 Unsigned )] []
6       (Sreturn (Some ? (Expr (Ebinop Oadd
7                          (Expr (Ecast (Tint I32 Signed  )
8                            (Expr (Evar (succ_pos_of_nat 1))
9                              (Tint I8 Unsigned ))) (Tint I32 Signed  ))
10                          (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
11                          (Tint I32 Signed  ))))
12     
13     
14     
15   ));
16  mk_pair ?? (succ_pos_of_nat 2 (* main *)) (Internal (
17    mk_function (Tint I32 Signed  ) [] [mk_pair ?? (succ_pos_of_nat 3) (Tint I32 Signed  )]
18      (Ssequence
19      (Sassign (Expr (Evar (succ_pos_of_nat 4))
20                 (Tpointer Any (Tfunction (Tcons (Tint I8 Unsigned ) Tnil) (Tint I32 Signed  ))))
21        (Expr (Ecast (Tpointer Any (Tfunction (Tcons (Tint I8 Unsigned ) Tnil) (Tint I32 Signed  )))
22          (Expr (Evar (succ_pos_of_nat 0))
23            (Tfunction (Tcons (Tint I8 Unsigned ) Tnil) (Tint I32 Signed  ))))
24          (Tpointer Any (Tfunction (Tcons (Tint I8 Unsigned ) Tnil) (Tint I32 Signed  )))))
25      (Ssequence
26      (Scall (Some ? (Expr (Evar (succ_pos_of_nat 3)) (Tint I32 Signed  )))
27        (Expr (Evar (succ_pos_of_nat 4))
28          (Tpointer Any (Tfunction (Tcons (Tint I8 Unsigned ) Tnil) (Tint I32 Signed  ))))
29        [(Expr (Ecast (Tint I8 Unsigned )
30           (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
31           (Tint I8 Unsigned ))])
32      (Sreturn (Some ? (Expr (Evar (succ_pos_of_nat 3)) (Tint I32 Signed  ))))))
33   
34   
35   
36  ))]
37  (succ_pos_of_nat 2)
38  [(mk_pair ?? (mk_pair ?? (mk_pair ?? (succ_pos_of_nat 4 (* f *))
39     [(Init_int24 (repr 0)) ]) Any)
40     (Tpointer Any (Tfunction (Tcons (Tint I8 Unsigned ) Tnil) (Tint I32 Signed  ))))]
41.
42
43  nremark exec: result ? (exec_up_to myprog 20 [EVint (repr 12)]).
44   nnormalize;  (* you can examine the result here *)
45   @; nqed.
46 
Note: See TracBrowser for help on using the repository browser.