package frama-c-metacsl
MetAcsl plugin of Frama-C for writing pervasives properties
Install
Dune Dependency
Authors
Maintainers
Sources
meta-0.9-beta.tar.bz2
md5=32bd324617144e618a39e0015445effb
sha512=d96bc4fb9e4c9771efeca815aa1d6f2bae0676cce56d9ed227370bacf4fb04c0811d53470cd15981406ae11a0e95af9f16ab31f7cac04ae2a92cbf85233fb496
doc/src/frama-c-metacsl.core/meta_options.ml.html
Source file meta_options.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
(**************************************************************************) (* *) (* This file is part of the Frama-C's MetACSL plug-in. *) (* *) (* Copyright (C) 2018-2025 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) (* you can redistribute it and/or modify it under the terms of the GNU *) (* Lesser General Public License as published by the Free Software *) (* Foundation, version 2.1. *) (* *) (* It is distributed in the hope that it will be useful, *) (* but WITHOUT ANY WARRANTY; without even the implied warranty of *) (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) (* GNU Lesser General Public License for more details. *) (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file LICENSE) *) (* *) (**************************************************************************) let help_msg = "This plugin translates the metaproperties in the code to native ACSL annotations" ^ "that can then be checked." let () = Plugin.is_share_visible() module Self = Plugin.Register (struct let name = "MetAcsl" let shortname = "meta" let help = help_msg end) let () = Parameter_customize.do_not_projectify () module Enabled = Self.False (struct let option_name = "-meta" let help = "Enable translation of metaproperties" end) module Check_External = Self.True (struct let option_name = "-meta-check-ext" let help = "Calls to external functions (such as memcpy) are treated as \ modifying/accessing the state inside the caller's body" end) let () = Parameter_customize.argument_may_be_fundecl() module Check_Callee_Assigns = Self.Kernel_function_set (struct let option_name = "-meta-check-callee-assigns" let arg_name = "f,..." let help = "Reading and writing metaproperties are instantiated for calls \ to listed functions from non-listed ones based on the \ assigns...from clauses of the callee (possibly in addition to \ their instantiation inside the callee when it is in the target set)." end) module Targets = Self.String_set (struct let option_name = "-meta-set" let arg_name = "targets" let help = "Define the set of meta-properties to process. Defaults to \ every meta-property" end) module Simpl = Self.True (struct let option_name = "-meta-simpl" let help = "Discard annotations that are obviously true" end) module Number_assertions = Self.False (struct let option_name = "-meta-number-assertions" let help = "Add an unique number to each instance of a meta-propery." end) module Prefix_meta = Self.True (struct let option_name = "-meta-add-prefix" let help = "Prefix meta: to the name of each generated property." end) module List_targets = Self.False (struct let option_name = "-meta-list-targets" let help = "Detail the list of targets for every meta-property" end) module Keep_proof_files = Self.False (struct let option_name = "-meta-keep-proof-files" let help = "Keep .why files after deduction attempts" end) module Static_bindings = Self.Int (struct let option_name = "-meta-static-bindings" let arg_name = "array_size" let default = 0 let help = "Use static arrays with the given size for bindings instead \ of dynamic arrays" end) module Separate_annots = Self.False (struct let option_name = "-meta-separate-annots" let help = "When set, each generated statement annotation will be tied to its own \ (nop) instruction. Otherwise (default), all annotations generated for \ a given statement will be tied to this statement." end) let () = Parameter_customize.set_negative_option_name "-meta-checks" module Default_to_assert = Self.True (struct let option_name = "-meta-asserts" let help = "Default to using assertions instead of checks when translating, \ unless specified otherwise in a meta-property" end) let unknown_func_wkey = Self.register_warn_category "unknown-func" let () = Self.set_warn_status unknown_func_wkey Log.Wabort type meta_flags = { check_external : bool; check_callee_assigns: Kernel_function.Set.t; simpl : bool; static_bindings : int option; target_set : Meta_utils.StrSet.t option; number_assertions : bool; prefix_meta : bool; list_targets : bool; keep_proof_files : bool; default_to_assert : bool; }
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>