Project

General

Profile

« Previous | Next » 

Revision d2d9d4cb

Added by Pierre-Loïc Garoche about 5 years ago

Missing files

View differences:

Makefile.in
71 71 
	install -m 0755 $(LOCAL_BINDIR)/* ${bindir}
72 72 
	mkdir -p ${includedir}/lustrec
73 73 
	cp include/* ${includedir}/lustrec
74 
	mkdir -p ${datadir}
75 
	install -m 0655 share/FindLustre.cmake ${datadir}
74 
	mkdir -p ${datarootdir}
75 
	install -m 0655 share/FindLustre.cmake ${datarootdir}
76 76 

  		




  77
  77
  
    
.PHONY: all compile-lusi doc dot lustrec lustrec.odocl clean install dist-clean


  		




  78
  78
  
    

  		












  

    
      src/Makefile
    
  





  1
  
  
    
OCAMLBUILD=/usr/bin/ocamlbuild -classic-display -use-ocamlfind -no-links 


  		




  
  1
  
    
OCAMLBUILD=/home/ploc/.opam/4.04.0/bin/ocamlbuild -classic-display -use-ocamlfind -no-links 


  		




  2
  2
  
    

  		




  3
  3
  
    
prefix=/home/ploc/Local


  		




  4
  4
  
    
exec_prefix=${prefix}


  		




  ......




  16
  16
  
    
	@mkdir -p $(LOCAL_BINDIR)


  		




  17
  17
  
    
	@mv _build/main_lustre_compiler.native $(LOCAL_BINDIR)/lustrec


  		




  18
  18
  
    

  		




  
  19
  
    
lustret:


  		




  
  20
  
    
	@echo Compiling binary lustrec


  		




  
  21
  
    
	@$(OCAMLBUILD) main_lustre_compiler.native


  		




  
  22
  
    
	@mkdir -p $(LOCAL_BINDIR)


  		




  
  23
  
    
	@mv _build/main_lustre_compiler.native $(LOCAL_BINDIR)/lustrec


  		




  
  24
  
    

  		




  
  25
  
    

  		




  19
  26
  
    
doc:


  		




  20
  27
  
    
	@echo Generating doc


  		




  21
  28
  
    
	@$(OCAMLBUILD) lustrec.docdir/index.html


  		












  

    
      src/backends/Horn/horn_backend_collecting_sem.ml
    
  





  92
  92
  
    
    (pp_conj (pp_horn_var machine)) main_output


  		




  93
  93
  
    
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next


  		




  94
  94
  
    
    ;


  		




  95
  
  
    
   if !Options.horn_queries then fprintf fmt "(query ERR)@."


  		




  
  95
  
    
   if !Options.horn_query then fprintf fmt "(query ERR)@."


  		




  96
  96
  
    

  		




  97
  97
  
    

  		




  98
  98
  
    
let cex_computation machines fmt node machine =


  		












  

    
      src/inliner.ml
    
  





  212
  212
  
    
  let inline_pair e1 e2 = 


  		




  213
  213
  
    
    let el', l', eqs', asserts', annots' = inline_tuple [e1;e2] in


  		




  214
  214
  
    
    match el' with


  		




  215
  
  
    
    | [e1'; e2'] -> e1', e2', l', eqs', asserts'


  		




  
  215
  
    
    | [e1'; e2'] -> e1', e2', l', eqs', asserts', annots'


  		




  216
  216
  
    
    | _ -> assert false


  		




  217
  217
  
    
  in


  		




  218
  218
  
    
  let inline_triple e1 e2 e3 = 


  		












  

    
      src/optimize_machine.ml
    
  





  61
  61
  
    

  		




  62
  62
  
    
(* 8th Jan 2016: issues when merging salsa with horn_encoding: The following


  		




  63
  63
  
    
   functions seem unsused. They have to be adapted to the new type for expr


  		




  64
  
  
    

  		




  
  64
  
    
*)


  		




  65
  65
  
    

  		




  66
  66
  
    
let unfold_expr_offset m offset expr =


  		




  67
  67
  
    
  List.fold_left


  		












  

    
      src/plugins/scopes/scopes.ml
    
  





  227
  227
  
    
  }


  		




  228
  228
  
    
    


  		




  229
  229
  
    

  		




  230
  
  
    
module Plugin : PluginType.PluginType =


  		




  
  230
  
    
module Plugin : (


  		




  
  231
  
    
  sig


  		




  
  232
  
    
    include PluginType.PluginType


  		




  
  233
  
    
    val show_scopes: unit -> bool


  		




  
  234
  
    
    end) =


  		




  231
  235
  
    
struct


  		




  232
  236
  
    
  let name = "scopes"


  		




  233
  237
  
    
  let is_active () = 


  		












Also available in:  Unified diff