forked from cil-project/cil
-
Notifications
You must be signed in to change notification settings - Fork 20
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Remove dynlink and findlib dependencies from goblint-cil library
- Loading branch information
Showing
6 changed files
with
185 additions
and
113 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,122 @@ | ||
| (* | ||
| Copyright (c) 2013 | ||
| Gabriel Kerneis <gabriel@kerneis.info> | ||
| All rights reserved. | ||
| Redistribution and use in source and binary forms, with or without | ||
| modification, are permitted provided that the following conditions are | ||
| met: | ||
| 1. Redistributions of source code must retain the above copyright | ||
| notice, this list of conditions and the following disclaimer. | ||
| 2. Redistributions in binary form must reproduce the above copyright | ||
| notice, this list of conditions and the following disclaimer in the | ||
| documentation and/or other materials provided with the distribution. | ||
| 3. The names of the contributors may not be used to endorse or promote | ||
| products derived from this software without specific prior written | ||
| permission. | ||
| THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS | ||
| IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED | ||
| TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A | ||
| PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER | ||
| OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, | ||
| EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, | ||
| PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR | ||
| PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF | ||
| LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING | ||
| NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS | ||
| SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. | ||
| *) | ||
|
|
||
| open GoblintCil | ||
|
|
||
| module E = Errormsg | ||
| module D = Dynlink | ||
| module F = Findlib | ||
|
|
||
| (** Dynamic linking *) | ||
|
|
||
| let load s = | ||
| try | ||
| D.allow_unsafe_modules true; | ||
| D.loadfile s | ||
| with D.Error e -> E.s (E.error "%s" (D.error_message e)) | ||
|
|
||
| (** Findlib magic *) | ||
|
|
||
| let initialized = ref false | ||
| let init () = | ||
| if not !initialized then begin | ||
| F.init (); | ||
| initialized := true | ||
| end | ||
|
|
||
| let adapt_filename f = try | ||
| D.adapt_filename f | ||
| with _ -> f | ||
|
|
||
| let findlib_lookup pkg = | ||
| try | ||
| let preds = [ if D.is_native then "native" else "byte"; "plugin" ] in | ||
| let cil_deps = F.package_deep_ancestors preds ["goblint-cil"] in | ||
| let deps = F.package_deep_ancestors preds [pkg] in | ||
| let deps = List.filter (fun x -> not (List.mem x cil_deps)) deps in | ||
| let find_modules pkg = | ||
| let base = F.package_directory pkg in | ||
| let archives = | ||
| try F.package_property preds pkg "archive" | ||
| (* some packages have dependencies but no archive *) | ||
| with Not_found -> "" in | ||
| let modules = List.filter ((<>) "") (Str.split (Str.regexp "[ ,]+") archives) in | ||
| List.map (fun m -> F.resolve_path ~base (adapt_filename m)) modules in | ||
| let files = List.map find_modules deps in | ||
| List.flatten files | ||
| with | ||
| | F.No_such_package (pkg, msg) -> | ||
| E.s (E.error "findlib: no such package %s.\n%s" pkg msg) | ||
| | F.Package_loop pkg -> | ||
| E.s (E.error "findlib: package loop for %s." pkg) | ||
|
|
||
| let find_plugin s = | ||
| if s = "" then E.s (E.error "missing module name") else | ||
| let s_resolve = adapt_filename (try F.resolve_path s with _ -> s) in | ||
| if Sys.file_exists s_resolve && not (Sys.is_directory s_resolve) then [s_resolve] | ||
| else findlib_lookup s | ||
|
|
||
| (** List of loaded modules *) | ||
| let plugins = ref [] | ||
|
|
||
| (** Add a single plugin, except if we have added it already *) | ||
| let add_plugin path = | ||
| if not (List.mem path !plugins) then | ||
| load path; | ||
| plugins := path :: !plugins | ||
|
|
||
| (** Look for plugin and dependencies and add them *) | ||
| let loadWithDeps s = | ||
| let paths = find_plugin s in | ||
| List.iter add_plugin paths | ||
|
|
||
| (** Parse only {switch} command-line option, ignoring every error raised by other, unparsed | ||
| options. Return the list of plugins to load. *) | ||
| let loadFromArgv switch = | ||
| let spec = [ | ||
| switch, Arg.String loadWithDeps, ""; | ||
| (* ignore --help at this stage *) | ||
| "--help", Arg.Unit ignore, ""; "-help", Arg.Unit ignore, "" ] in | ||
| let idx = ref 0 in | ||
| let rec aux () = | ||
| try | ||
| Arg.parse_argv ~current:idx Sys.argv spec ignore "" | ||
| with Arg.Bad _ | Arg.Help _ -> aux () | ||
| in init (); aux () | ||
|
|
||
| let loadFromEnv name default = | ||
| let plugins = | ||
| try Str.split (Str.regexp "[ ,]+") (Sys.getenv name) | ||
| with Not_found -> default in | ||
| List.iter loadWithDeps plugins |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,57 @@ | ||
| (* | ||
| Copyright (c) 2013 | ||
| Gabriel Kerneis <gabriel@kerneis.info> | ||
| All rights reserved. | ||
| Redistribution and use in source and binary forms, with or without | ||
| modification, are permitted provided that the following conditions are | ||
| met: | ||
| 1. Redistributions of source code must retain the above copyright | ||
| notice, this list of conditions and the following disclaimer. | ||
| 2. Redistributions in binary form must reproduce the above copyright | ||
| notice, this list of conditions and the following disclaimer in the | ||
| documentation and/or other materials provided with the distribution. | ||
| 3. The names of the contributors may not be used to endorse or promote | ||
| products derived from this software without specific prior written | ||
| permission. | ||
| THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS | ||
| IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED | ||
| TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A | ||
| PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER | ||
| OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, | ||
| EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, | ||
| PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR | ||
| PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF | ||
| LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING | ||
| NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS | ||
| SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. | ||
| *) | ||
|
|
||
| (** Extending CIL with external features *) | ||
|
|
||
| (** {1 Internal}*) | ||
|
|
||
| (** Initialize the module. This needs to be called before {!loadWithDeps} is | ||
| used. Called automatically by {!loadFromArgv}. *) | ||
| val init : unit -> unit | ||
|
|
||
| (** Find and dynamically links a module. The name should be either a path to a | ||
| cmo, cma or cmxs file, or the name of a findlib package. In the latter case, | ||
| package dependencies are loaded automatically. Each file is loaded at most | ||
| one. The loaded module must call {!register} to make its features | ||
| available to CIL. *) | ||
| val loadWithDeps : string -> unit | ||
|
|
||
| (** [loadFromArgv switch] searches {!Sys.argv} for the command-line option | ||
| [switch], and loads the modules passed as parameters. Ignores every other | ||
| {!Sys.argv} element. *) | ||
| val loadFromArgv : string -> unit | ||
|
|
||
| (** [loadFromEnv name default] loads coma-separated module names stored in the | ||
| environment variable [name], or [default] if it is not defined. *) | ||
| val loadFromEnv : string -> string list -> unit |