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 b397dcf07b89389b3200191ad6d594f759694e7f..c32ca8780a4558d0bc26c4d9b14da8988edf7149 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 d0250a65f727ae453b6b20b262616176965fa8ff..d5664f8890a1a5370e1d1ffb47e81ab1bc55b09c 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