Project

General

Profile

« Previous | Next » 

Revision c02d255e

Added by Pierre-Loïc Garoche almost 9 years ago

Solved some bugs in the lustre printer
Generation of a witness with both the main node and hte inlined main node
Test script modified to check consistency of the inlining process

View differences:

src/options.ml
33 33 
let java = ref false
34 34 
let dest_dir = ref ""
35 35 
let verbose_level = ref 1
36 
let global_inline = ref false
37 
let witnesses = ref false
36 38 

  		




  37
  39
  
    
let options =


  		




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


  		




  ......




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


  		




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


  		




  47
  49
  
    
    "-java", Arg.Set java, "generates Java output instead of C";


  		




  
  50
  
    
    "-inline", Arg.Set global_inline, "inline all node calls (require a main node)";


  		




  
  51
  
    
    "-witnesses", Arg.Set witnesses, "enable production of witnesses during compilation";


  		




  48
  52
  
    
    "-print_types", Arg.Set print_types, "prints node types";


  		




  49
  53
  
    
    "-print_clocks", Arg.Set print_clocks, "prints node clocks";


  		




  50
  54
  
    
    "-verbose", Arg.Set_int verbose_level, " changes verbose level <default: 1>";


  		












Also available in:  Unified diff