Project

General

Profile

« Previous | Next » 

Revision 43aa67ec

Added by Teme Kahsai over 8 years ago

Fixed horn backend to make query for properties. More work needed for cex

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

View differences:

src/options.ml
37 37 
let witnesses = ref false
38 38 
let optimization = ref 2
39 39 
let horntraces = ref false
40 
let horn_queries = ref false
40 
let horn_cex = ref false
41 

  		




  41
  42
  
    

  		




  42
  43
  
    
let options =


  		




  43
  44
  
    
  [ "-d", Arg.Set_string dest_dir,


  		




  ......




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


  		




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


  		




  56
  57
  
    
    "-horn-traces", Arg.Unit (fun () -> output := "horn"; horntraces:=true), "produce traceability file for Horn backend. Enable the horn backend.";


  		




  57
  
  
    
    "-horn-queries", Arg.Set horn_queries, "add the queries instructions at the end of the generated horn files";


  		




  
  58
  
    
    "-horn-cex", Arg.Set horn_cex, "generate cex enumeration. Enable the horn backend (work in progress)";


  		




  58
  59
  
    
    "-lustre", Arg.Unit (fun () -> output := "lustre"), "generates Lustre output, performing all active optimizations";


  		




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


  		




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


  		




  ......




  74
  75
  
    
	    )


  		




  75
  76
  
    
    with Sys_error _ -> Unix.mkdir dir 0o750


  		




  76
  77
  
    
  in


  		




  77
  
  
    
  dir 


  		




  
  78
  
    
  dir


  		




  78
  79
  
    

  		




  79
  80
  
    
(* Local Variables: *)


  		




  80
  81
  
    
(* compile-command:"make -C .." *)


  		












Also available in:  Unified diff