Revision 2d37a1e1
Added by Pierre-Loïc Garoche over 6 years ago
| regression_tests/lustre_files/success/kind_fmcad08/simulation/fast_1_e8_747_e8_1041.lus | ||
|---|---|---|
| 69 | 69 |
and ccall then true else if not ccall then false |
| 70 | 70 |
else pre(cca); |
| 71 | 71 |
tel |
| 72 |
--@ ensures OK; |
|
| 73 | 72 |
node top (igsw, ccd, cconoff, bpa, cccanc, battok, gearok, |
| 74 | 73 |
qfok, sdok, accok, ccseti, ccsetd, ccr: bool; vs: int) |
| 75 | 74 |
returns (OK : bool); |
| 75 |
--@ contract guarantees OK; |
|
| 76 | 76 |
var |
| 77 | 77 |
ccont, cca: bool; |
| 78 | 78 |
env : bool; |
Also available in: Unified diff
Renaminig lustre contracts from ensures to guarantees
Will require the latest cocospec branch to compile (before it is integrated in the unstable/master branches)