Revision 2d37a1e1 regression_tests/lustre_files/success/kind_fmcad08/memory2/SYNAPSE_5.lus
regression_tests/lustre_files/success/kind_fmcad08/memory2/SYNAPSE_5.lus | ||
---|---|---|
47 | 47 |
tel |
48 | 48 |
|
49 | 49 |
-- Only provable in nbac |
50 |
--@ ensures OK; |
|
51 | 50 |
node top(e_s1, e_s2, e_s3 : bool; init_invalid_s : int) |
52 | 51 |
returns( OK : bool ); |
52 |
--@ contract guarantees OK; |
|
53 | 53 |
var invalid_s, valid_s, dirty_s : int; mem_init_s : int; |
54 | 54 |
env : bool; |
55 | 55 |
let |
Also available in: Unified diff