Skip to content
Snippets Groups Projects
Commit d2d9d4cb authored by Pierre Loic Garoche's avatar Pierre Loic Garoche
Browse files

Missing files

parent 85da3a4b
No related branches found
No related tags found
No related merge requests found
......@@ -71,8 +71,8 @@ install: clean-lusic compile-lusi compile-mpfr-lusi
install -m 0755 $(LOCAL_BINDIR)/* ${bindir}
mkdir -p ${includedir}/lustrec
cp include/* ${includedir}/lustrec
mkdir -p ${datadir}
install -m 0655 share/FindLustre.cmake ${datadir}
mkdir -p ${datarootdir}
install -m 0655 share/FindLustre.cmake ${datarootdir}
.PHONY: all compile-lusi doc dot lustrec lustrec.odocl clean install dist-clean
OCAMLBUILD=/usr/bin/ocamlbuild -classic-display -use-ocamlfind -no-links
OCAMLBUILD=/home/ploc/.opam/4.04.0/bin/ocamlbuild -classic-display -use-ocamlfind -no-links
prefix=/home/ploc/Local
exec_prefix=${prefix}
......@@ -16,6 +16,13 @@ lustrec:
@mkdir -p $(LOCAL_BINDIR)
@mv _build/main_lustre_compiler.native $(LOCAL_BINDIR)/lustrec
lustret:
@echo Compiling binary lustrec
@$(OCAMLBUILD) main_lustre_compiler.native
@mkdir -p $(LOCAL_BINDIR)
@mv _build/main_lustre_compiler.native $(LOCAL_BINDIR)/lustrec
doc:
@echo Generating doc
@$(OCAMLBUILD) lustrec.docdir/index.html
......
......@@ -92,7 +92,7 @@ let check_prop machines fmt node machine =
(pp_conj (pp_horn_var machine)) main_output
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next
;
if !Options.horn_queries then fprintf fmt "(query ERR)@."
if !Options.horn_query then fprintf fmt "(query ERR)@."
let cex_computation machines fmt node machine =
......
......@@ -212,7 +212,7 @@ let rec inline_expr ?(selection_on_annotation=false) expr locals node nodes =
let inline_pair e1 e2 =
let el', l', eqs', asserts', annots' = inline_tuple [e1;e2] in
match el' with
| [e1'; e2'] -> e1', e2', l', eqs', asserts'
| [e1'; e2'] -> e1', e2', l', eqs', asserts', annots'
| _ -> assert false
in
let inline_triple e1 e2 e3 =
......
......@@ -61,7 +61,7 @@ let eliminate_dim elim dim =
(* 8th Jan 2016: issues when merging salsa with horn_encoding: The following
functions seem unsused. They have to be adapted to the new type for expr
*)
let unfold_expr_offset m offset expr =
List.fold_left
......
......@@ -227,7 +227,11 @@ let update_machine machine =
}
module Plugin : PluginType.PluginType =
module Plugin : (
sig
include PluginType.PluginType
val show_scopes: unit -> bool
end) =
struct
let name = "scopes"
let is_active () =
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment