Project

General

Profile

Revision 2d37a1e1 regression_tests/lustre_files/success/kind_fmcad08/memory2/SYNAPSE_5.lus

View differences:

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