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