Revision 2d37a1e1
Added by Pierre-Loïc Garoche over 6 years ago
| regression_tests/lustre_files/success/kind_fmcad08/memory2/SYNAPSE_3_e8_1329_e1_1270.lus | ||
|---|---|---|
| 35 | 35 |
if(e_s3) then if(garde_s3) then 1 else pre dirty_s else |
| 36 | 36 |
pre dirty_s; |
| 37 | 37 |
tel |
| 38 |
--@ ensures OK; |
|
| 39 | 38 |
node top(e_s1, e_s2, e_s3 : bool; init_invalid_s : int) |
| 40 | 39 |
returns( OK : bool ); |
| 40 |
--@ contract guarantees OK; |
|
| 41 | 41 |
var invalid_s, valid_s, dirty_s : int; mem_init_s : int; |
| 42 | 42 |
env : bool; |
| 43 | 43 |
let |
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)