Source file options.ml

(**************************************************************************)
(*                                                                        *)
(*  SPDX-License-Identifier LGPL-2.1                                      *)
(*  Copyright (C)                                                         *)
(*  CEA (Commissariat à l'énergie atomique et aux énergies alternatives)  *)
(*                                                                        *)
(**************************************************************************)

let help_msg = "generates annotations for runtime error checking"

include Plugin.Register
    (struct
      let name = "RteGen"
      let shortname = "rte"
      let help = help_msg
    end)

(* enabling/disabling plugin *)
module Enabled =
  False
    (struct
      let option_name = "-rte"
      let help = "when on (off by default), " ^ help_msg
    end)

(* annotates division by zero (undefined behavior) *)
module DoDivMod =
  True
    (struct
      let option_name = "-rte-div"
      let help = "when on (default), annotate for modulo and division by zero"
    end)

(* annotates left and right shifts (undefined behavior) *)
module DoShift =
  True
    (struct
      let option_name = "-rte-shift"
      let help = "when on (default), annotate for left and right shifts by a value out of bounds"
    end)

(* annotates casts from floating-point to integer (undefined behavior) *)
module DoFloatToInt =
  True
    (struct
      let option_name = "-rte-float-to-int"
      let help = "when on (default), annotate casts from floating-point to \
                  integer"
    end)

(* annotates local variables and pointers read (aside from globals) initialization *)
module DoInitialized =
  Kernel_function_set
    (struct
      let option_name = "-rte-initialized"
      let arg_name = "fct"
      let help = "for each function in 'fct', annotates reads of non struct or \
                  union values from local variables and pointers with \
                  initialization tests, see documentation for more details"
    end)

(* annotates invalid memory access (undefined behavior) *)
module DoMemAccess =
  True
    (struct
      let option_name = "-rte-mem"
      let help = "when on (default), annotate for valid pointer or \
                  array access"
    end)

(* annotates calls through pointers *)
module DoPointerCall =
  True
    (struct
      let option_name = "-rte-pointer-call"
      let help = "when on, annotate functions calls through pointers"
    end)

(* uses results of basic constant propagation in order to check
   validity / invalidity of generated assertions, emitting a status if possible.
   Notice that annotations that can be considered valid from syntactical rules
   are also considered as trivial.
*)
module Trivial =
  False
    (struct
      let option_name = "-rte-trivial-annotations"
      let help = "generate all annotations even if they trivially hold \
                  (from evaluation of constant expressions, syntactical rules...)"
      (* if on, evaluates constants in order to check if assertions
         are trivially true / false *)
    end)

(* emits a warning when an assertion generated by rte is clearly invalid
   (using constant folding, see ConstFold *)
module Warn =
  True
    (struct
      let option_name = "-rte-warn"
      let help = "when on (default), emits warning on broken asserts"
    end)

(* this option allows the user to select a set of functions on which
   the plug-in performs its jobs (and only those).
   By default all functions are annotated *)
module FunctionSelection =
  Kernel_function_set
    (struct
      let option_name = "-rte-select"
      let arg_name = "fun"
      let help = "select <fun> for analysis (default all functions)"
    end)

let dkey_annot =
  register_category "annot" ~default:true
    ~help:"message about function annotations"

let () =
  if not Eva_analysis.is_available
  then Parameter_customize.is_invisible ()

module UseEvaResults =
  Bool
    (struct
      let option_name  = "-rte-use-eva-results"
      let default = Eva_analysis.is_available
      let help =
        "When enabled, do not emit annotations on functions analyzed by Eva"
    end)

let use_eva_results () =
  if UseEvaResults.get () && not Eva_analysis.is_available then
    warning ~once:true
      "-rte-use-eva-results is set while Eva is not available, ignoring" ;
  UseEvaResults.get ()