From 331305cd4a42f15d18a263386789c88986631871 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 27 Sep 2022 14:02:10 +0200
Subject: [PATCH] [deduction] ensure run.pl stays executable in dune-governed
install
---
{share => deduce}/SETLOG_LICENSE | 0
{share => deduce}/model.slog | 0
{share => deduce}/run.pl | 0
{share => deduce}/setlog.pl | 0
{share => deduce}/setlog_rules.pl | 0
{share => deduce}/setloglib.slog | 0
dune | 22 ++++++++++++----------
meta_deduce.ml | 9 ++++++---
8 files changed, 18 insertions(+), 13 deletions(-)
rename {share => deduce}/SETLOG_LICENSE (100%)
rename {share => deduce}/model.slog (100%)
rename {share => deduce}/run.pl (100%)
rename {share => deduce}/setlog.pl (100%)
rename {share => deduce}/setlog_rules.pl (100%)
rename {share => deduce}/setloglib.slog (100%)
diff --git a/share/SETLOG_LICENSE b/deduce/SETLOG_LICENSE
similarity index 100%
rename from share/SETLOG_LICENSE
rename to deduce/SETLOG_LICENSE
diff --git a/share/model.slog b/deduce/model.slog
similarity index 100%
rename from share/model.slog
rename to deduce/model.slog
diff --git a/share/run.pl b/deduce/run.pl
similarity index 100%
rename from share/run.pl
rename to deduce/run.pl
diff --git a/share/setlog.pl b/deduce/setlog.pl
similarity index 100%
rename from share/setlog.pl
rename to deduce/setlog.pl
diff --git a/share/setlog_rules.pl b/deduce/setlog_rules.pl
similarity index 100%
rename from share/setlog_rules.pl
rename to deduce/setlog_rules.pl
diff --git a/share/setloglib.slog b/deduce/setloglib.slog
similarity index 100%
rename from share/setloglib.slog
rename to deduce/setloglib.slog
diff --git a/dune b/dune
index b397dcf..c32ca87 100644
--- a/dune
+++ b/dune
@@ -42,7 +42,7 @@
(name MetAcsl)
(public_name frama-c-metacsl.core)
(flags -open Frama_c_kernel :standard -w -9 -warn-error -20-26-27)
- (libraries frama-c.kernel frama-c-callgraph.core)
+ (libraries findlib frama-c.kernel frama-c-callgraph.core)
)
(plugin
@@ -57,17 +57,19 @@
(install
(package frama-c-metacsl)
- (section
- (site
- (frama-c share)))
+ (section lib)
(files
- (share/model.slog as meta/model.slog)
- (share/run.pl as meta/run.pl)
- (share/setloglib.slog as meta/setloglib.slog)
- (share/SETLOG_LICENSE as meta/SETLOG_LICENSE)
- (share/setlog.pl as meta/setlog.pl)
- (share/setlog_rules.pl as meta/setlog_rules.pl)
+ (deduce/model.slog as deduce/model.slog)
+ (deduce/setloglib.slog as deduce/setloglib.slog)
+ (deduce/SETLOG_LICENSE as deduce/SETLOG_LICENSE)
+ (deduce/setlog.pl as deduce/setlog.pl)
+ (deduce/setlog_rules.pl as deduce/setlog_rules.pl)
)
)
+(install
+ (package frama-c-metacsl)
+ (section libexec)
+ (files (deduce/run.pl as deduce/run.pl))
+)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
diff --git a/meta_deduce.ml b/meta_deduce.ml
index d0250a6..d5664f8 100644
--- a/meta_deduce.ml
+++ b/meta_deduce.ml
@@ -376,9 +376,12 @@ go :- %a
output_string oc (Buffer.contents buffer);
close_out oc;
(* Locate where the Prolog model is and go to it *)
- let sharedir = Format.asprintf "%a"
- Filepath.Normalized.pp_abs (Self.Share.get_dir ".") in
- Sys.chdir sharedir;
+ let dir =
+ try Findlib.package_directory "frama-c-metacsl"
+ with Findlib.No_such_package(_,err) ->
+ Self.fatal "Could not locate my own directory: %s" err
+ in
+ Sys.chdir (dir ^ "/deduce");
(* Run the Prolog model on our file, with a 30s timeout *)
let command = Format.asprintf "./run.pl prove %s 30 > /dev/null" filename in
let max_attempts = 8 in
--
GitLab