Project

General

Profile

« Previous | Next » 

Revision f6923c9e

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

Initial copy of the horn output version. Not really working yet

View differences:

src/options.ml
30 30 
let ansi = ref false
31 31 
let check = ref false
32 32 
let c_spec = ref false
33 
let java = ref false
33 
let output = ref "C"
34 34 
let dest_dir = ref ""
35 35 
let verbose_level = ref 1
36 36 

  		




  ......




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


  		




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


  		




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


  		




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


  		




  
  47
  
    
    "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C";


  		




  
  48
  
    
    "-horn", Arg.Unit (fun () -> output := "horn"), "generates Horn clauses encoding output instead of C";


  		




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


  		




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


  		




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


  		












Also available in:  Unified diff