Project

General

Profile

« Previous | Next » 

Revision 2d37a1e1

Added by Pierre-Loïc Garoche over 6 years ago

Renaminig lustre contracts from ensures to guarantees
Will require the latest cocospec branch to compile (before it is integrated in the unstable/master branches)

View differences:

regression_tests/lustre_files/success/kind_fmcad08/large/microwave32.lus
1 
--@ ensures OK;
2 1 
node top(KP_START: bool;
3 2 
      KP_CLEAR: bool;
4 3 
      KP_0: bool;
......
15 14 
) returns (OK:bool);
16 15 

  		




  17
  16
  
    
   


  		




  
  17
  
    
--@ contract guarantees OK;


  		




  18
  18
  
    
var


  		




  19
  19
  
    
   LEFT_DIGIT: int; 


  		




  20
  20
  
    
      SETUP: bool; 


  		












Also available in:  Unified diff