package goblint-cil
A front-end for the C programming language that facilitates program analysis and transformation
Install
Dune Dependency
Authors
Maintainers
Sources
goblint-cil-2.0.1.tbz
sha256=5f81cb3f25c09770e77b5eb4092e6621e456122b6d1219dcc304c062075f9572
sha512=31bb753031e0ef321a2ef065373009270881b1cce7f23167b378845188aed9cb49f18a165edd2e11f751f2c7a7b84ab5ac1da50ba1f5cb975e6e8a97157838ed
doc/src/goblint-cil/feature.ml.html
Source file feature.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156
(* 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 Cil module E = Errormsg module D = Dynlink module F = Findlib type t = { mutable fd_enabled: bool; fd_name: string; fd_description: string; fd_extraopt: (string * Arg.spec * string) list; fd_doit: (file -> unit); fd_post_check: bool; } let features = ref [] let same_name s f = s = f.fd_name let register f = if List.exists (same_name f.fd_name) !features then E.s (E.error "Feature %s is already registered" f.fd_name) else features := !features @ [f] let list_registered () = !features let find s = List.find (same_name s) !features let registered s = try ignore(find s); true with Not_found -> false let enabled s = try (find s).fd_enabled with Not_found -> false let enable s = try let f = find s in f.fd_enabled <- true with Not_found -> E.s (E.error "cannot enable feature %s: not found" s) (** 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
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>