Revision 2d37a1e1 regression_tests/lustre_files/success/kind_fmcad08/simulation/metros_2.lus
regression_tests/lustre_files/success/kind_fmcad08/simulation/metros_2.lus | ||
---|---|---|
45 | 45 |
tel |
46 | 46 |
|
47 | 47 |
-- Not provable? |
48 |
--@ ensures OK; |
|
49 | 48 |
node top(B0, B1 : bool; S : bool) |
50 | 49 |
returns (OK:bool); |
50 |
--@ contract guarantees OK; |
|
51 | 51 |
var nB0, nB1 : int; |
52 | 52 |
nS : int; |
53 | 53 |
diff0,diff1:int; |
Also available in: Unified diff