Project

General

Profile

« Previous | Next » 

Revision 7291cb80

Added by Xavier Thirioux over 9 years ago

- merged test script
- added -d support
- corrected #open parser problem
- corrected interface/implementation (.lusi/.lus) checking
for types (not yet for clocks)

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@171 041b043f-8d7c-46b2-b46e-ef0dd855326e

View differences:

src/options.ml
31 31 
let check = ref false
32 32 
let c_spec = ref false
33 33 
let output = ref "C"
34 
let dest_dir = ref ""
34 
let dest_dir = ref "."
35 35 
let verbose_level = ref 1
36 36 
let global_inline = ref false
37 37 
let witnesses = ref false
38 38 

  		




  39
  39
  
    
let options =


  		




  40
  40
  
    
  [ "-d", Arg.Set_string dest_dir,


  		




  41
  
  
    
    "produces code in the specified directory";


  		




  
  41
  
    
    "produces code in the specified directory (default: .)";


  		




  42
  42
  
    
    "-node", Arg.Set_string main_node, "specifies the main node";


  		




  43
  43
  
    
    "-init", Arg.Set delay_calculus, "performs an initialisation analysis for Lustre nodes";


  		




  44
  44
  
    
    "-dynamic", Arg.Clear static_mem, "specifies a dynamic allocation scheme for main Lustre node (default: static)";


  		




  45
  
  
    
    "-ansi", Arg.Set ansi, "specifies that generated C code is ansi C90 compliant (default is C99)";


  		




  
  45
  
    
    "-ansi", Arg.Set ansi, "specifies that generated C code is ansi C90 compliant (default: C99)";


  		




  46
  46
  
    
    "-check-access", Arg.Set check, "checks at runtime that array accesses always lie within bounds (default: no check)";


  		




  47
  47
  
    
    "-c-spec", Arg.Set c_spec, 


  		




  48
  48
  
    
    "generates a C encoding of the specification instead of ACSL contracts and annotations. Only meaningful for the C backend";


  		












Also available in:  Unified diff