Source file meta_options.ml

(**************************************************************************)
(*                                                                        *)
(*  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;
}