From d2d9d4cbf6b833f7784bec09282825316ed890da Mon Sep 17 00:00:00 2001
From: ploc <ploc@garoche.net>
Date: Wed, 26 Apr 2017 23:25:47 +0200
Subject: [PATCH] Missing files
---
Makefile.in | 4 ++--
src/Makefile | 9 ++++++++-
src/backends/Horn/horn_backend_collecting_sem.ml | 2 +-
src/inliner.ml | 2 +-
src/optimize_machine.ml | 2 +-
src/plugins/scopes/scopes.ml | 6 +++++-
6 files changed, 18 insertions(+), 7 deletions(-)
diff --git a/Makefile.in b/Makefile.in
index 38766be5..f8bed493 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -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
diff --git a/src/Makefile b/src/Makefile
index 822ecdf6..9c9f5e86 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -1,4 +1,4 @@
-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
diff --git a/src/backends/Horn/horn_backend_collecting_sem.ml b/src/backends/Horn/horn_backend_collecting_sem.ml
index e401527c..f6393bcb 100644
--- a/src/backends/Horn/horn_backend_collecting_sem.ml
+++ b/src/backends/Horn/horn_backend_collecting_sem.ml
@@ -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 =
diff --git a/src/inliner.ml b/src/inliner.ml
index a8fc5902..167131ca 100644
--- a/src/inliner.ml
+++ b/src/inliner.ml
@@ -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 =
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index 4c30aa2a..7e0ce0de 100644
--- a/src/optimize_machine.ml
+++ b/src/optimize_machine.ml
@@ -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
diff --git a/src/plugins/scopes/scopes.ml b/src/plugins/scopes/scopes.ml
index 829f9ea9..dd934ecf 100644
--- a/src/plugins/scopes/scopes.ml
+++ b/src/plugins/scopes/scopes.ml
@@ -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 () =
--
GitLab