source: src/Clight/test/goto-if.c.ma @ 1914

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

Fix bug in Clight semantics that misses goto-labels inside a cost label
statement.

File size: 856 bytes
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  ) [] []
7         (Ssequence
8         (Sgoto (ident_of_nat 1))
9         (Sifthenelse (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  ))
10           (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 1))
11                                 (Tint I32 Signed  ))))
12           (Slabel (ident_of_nat 1)
13           (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
14                                 (Tint I32 Signed  )))))))
15       
16       
17       
18     )〉]
19  (ident_of_nat 0)
20 
21.
22
23(*
24example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
25normalize  (* you can examine the result here *)
26*)
Note: See TracBrowser for help on using the repository browser.