Parameters (frama-c-eva.Eva.Parameters)

module Eva : Frama_c_kernel.Parameter_sig.Bool

module Precision : Frama_c_kernel.Parameter_sig.Int

Meta-option

Domains

module Domains : Frama_c_kernel.Parameter_sig.String_set

module DomainsFunction : 
  Frama_c_kernel.Parameter_sig.Multiple_map
    with type key = string
     and type value = Frama_c_kernel.Kernel_function.t * Eva__.Domain_mode.mode

module EqualityCall : Frama_c_kernel.Parameter_sig.String

module EqualityCallFunction : 
  Frama_c_kernel.Parameter_sig.Map
    with type key = Frama_c_kernel.Cil_types.kernel_function
     and type value = string

module OctagonCall : Frama_c_kernel.Parameter_sig.Bool

module MultidimSegmentLimit : Frama_c_kernel.Parameter_sig.Int

module MultidimDisjunctiveInvariants : Frama_c_kernel.Parameter_sig.Bool

module MultidimFastImprecise : Frama_c_kernel.Parameter_sig.Bool

module TaintAuto : Frama_c_kernel.Parameter_sig.Bool

module TaintSingletons : Frama_c_kernel.Parameter_sig.Bool

module SecureFlow : Frama_c_kernel.Parameter_sig.Bool

module NumerorsInteraction : Frama_c_kernel.Parameter_sig.String

module TracesUnrollLoop : Frama_c_kernel.Parameter_sig.Bool

module TracesUnifyLoop : Frama_c_kernel.Parameter_sig.Bool

module TracesDot : Frama_c_kernel.Parameter_sig.Filepath

module TracesProject : Frama_c_kernel.Parameter_sig.Bool

Precision

module WideningDelay : Frama_c_kernel.Parameter_sig.Int

module WideningPeriod : Frama_c_kernel.Parameter_sig.Int

module ArrayPrecisionLevel : Frama_c_kernel.Parameter_sig.Int

module SubdivideNonLinear : Frama_c_kernel.Parameter_sig.Int

module SubdivideNonLinearFunction : 
  Frama_c_kernel.Parameter_sig.Map
    with type key = Frama_c_kernel.Cil_types.kernel_function
     and type value = int

module EnumerateCond : Frama_c_kernel.Parameter_sig.Bool

module OracleDepth : Frama_c_kernel.Parameter_sig.Int

module ReductionDepth : Frama_c_kernel.Parameter_sig.Int

State partitioning

module MinLoopUnroll : Frama_c_kernel.Parameter_sig.Int

module AutoLoopUnroll : Frama_c_kernel.Parameter_sig.Int

module DefaultLoopUnroll : Frama_c_kernel.Parameter_sig.Int

module HistoryPartitioning : Frama_c_kernel.Parameter_sig.Int

module HistoryPartitioningFunction : 
  Frama_c_kernel.Parameter_sig.Map
    with type key = Frama_c_kernel.Cil_types.kernel_function
     and type value = int

module ValuePartitioning : Frama_c_kernel.Parameter_sig.String_set

module SplitLimit : Frama_c_kernel.Parameter_sig.Int

module InterproceduralSplits : Frama_c_kernel.Parameter_sig.Bool

module InterproceduralHistory : Frama_c_kernel.Parameter_sig.Bool

module SLevel : Frama_c_kernel.Parameter_sig.Int

module SlevelFunction : 
  Frama_c_kernel.Parameter_sig.Map
    with type key = Frama_c_kernel.Cil_types.kernel_function
     and type value = int

module SlevelMergeAfterLoop : Frama_c_kernel.Parameter_sig.Kernel_function_set

module SplitReturnFunction : 
  Frama_c_kernel.Parameter_sig.Map
    with type key = Frama_c_kernel.Cil_types.kernel_function
     and type value = Eva__.Split_strategy.split_strategy

module SplitReturn : 
  Frama_c_kernel.Parameter_sig.Custom
    with type t = Eva__.Split_strategy.split_strategy

Performance

module NoResultsDomain : Frama_c_kernel.Parameter_sig.String_set

module NoResultsFunction : Frama_c_kernel.Parameter_sig.Fundec_set

module ResultsAll : Frama_c_kernel.Parameter_sig.Bool

module JoinResults : Frama_c_kernel.Parameter_sig.Bool

module Memexec : Frama_c_kernel.Parameter_sig.Bool

Initial context of the analysis

module ContextDepth : Frama_c_kernel.Parameter_sig.Int

module ContextWidth : Frama_c_kernel.Parameter_sig.Int

module ContextValidPointers : Frama_c_kernel.Parameter_sig.Bool

module InitializationPaddingGlobals : 
  Frama_c_kernel.Parameter_sig.S
    with type t = [ `Initialized | `Uninitialized | `MaybeInitialized ]

Builtins

module BuiltinsOverrides : 
  Frama_c_kernel.Parameter_sig.Map
    with type key = Frama_c_kernel.Cil_types.kernel_function
     and type value = string

module BuiltinsAuto : Frama_c_kernel.Parameter_sig.Bool

module BuiltinsList : Frama_c_kernel.Parameter_sig.Bool

module AllocBuiltin : Frama_c_kernel.Parameter_sig.String

module AllocFunctions : Frama_c_kernel.Parameter_sig.String_set

module AllocReturnsNull : Frama_c_kernel.Parameter_sig.Bool

module MallocLevel : Frama_c_kernel.Parameter_sig.Int

Analysis behavior

module UseSpec : Frama_c_kernel.Parameter_sig.Kernel_function_set

module SkipLibcSpecs : Frama_c_kernel.Parameter_sig.Bool

module RecursiveUnroll : Frama_c_kernel.Parameter_sig.Int

module RmAssert : Frama_c_kernel.Parameter_sig.Bool

module InterpreterMode : Frama_c_kernel.Parameter_sig.Bool

module StopAtNthAlarm : Frama_c_kernel.Parameter_sig.Int

Non standard alarms

module WarnCopyIndeterminate : Frama_c_kernel.Parameter_sig.Kernel_function_set

module WarnSignedConvertedDowncast : Frama_c_kernel.Parameter_sig.Bool

module WarnPointerSubtraction : Frama_c_kernel.Parameter_sig.Bool

module WarnPointerComparison : 
  Frama_c_kernel.Parameter_sig.S with type t = [ `All | `Pointer | `None ]

module UndefinedPointerComparisonPropagateAll : 
  Frama_c_kernel.Parameter_sig.Bool

module InitializedLocals : Frama_c_kernel.Parameter_sig.Bool

Verbosity and outputs

module Verbose : Frama_c_kernel.Parameter_sig.Int

module ShowPerf : Frama_c_kernel.Parameter_sig.Bool

module ShowSlevel : Frama_c_kernel.Parameter_sig.Int

module PrintCallstacks : Frama_c_kernel.Parameter_sig.Bool

module Flamegraph : Frama_c_kernel.Parameter_sig.Filepath

module StatisticsFile : Frama_c_kernel.Parameter_sig.Filepath

module ReportRedStatuses : Frama_c_kernel.Parameter_sig.Filepath

module Annot : Frama_c_kernel.Parameter_sig.Kernel_function_set

Experimental

module ReduceOnLogicAlarms : Frama_c_kernel.Parameter_sig.Bool

module AllRoundingModesConstants : Frama_c_kernel.Parameter_sig.Bool

type descending_strategy =

| NoIteration
| FullIteration
| ExitIteration

module DescendingIteration : 
  Frama_c_kernel.Parameter_sig.S with type t = descending_strategy

module HierarchicalConvergence : Frama_c_kernel.Parameter_sig.Bool

Utility functions

val enabled_domains : unit -> (string * string) list

Returns the list (name, descr) of currently enabled abstract domains.

val use_builtin : Frama_c_kernel.Cil_types.kernel_function -> string -> unit

use_builtin kf name instructs the analysis to use the builtin name to interpret calls to function kf. Raises Not_found if there is no builtin of name name.

val use_global_value_partitioning : Frama_c_kernel.Cil_types.varinfo -> unit

use_global_value_partitioning vi instructs the analysis to use value partitioning on the global variable vi.

val change_correctness : unit -> unit

This function should be called whenever the correctness of the analysis is externally changed through the Eva API, to ensure that the property statuses emitted by Eva are properly reset.

Internal use only

val configure_precision : unit -> unit

val parameters_correctness : Frama_c_kernel.Typed_parameter.t list

List of parameters having an impact on the correctness of the analysis.

val parameters_tuning : Frama_c_kernel.Typed_parameter.t list

List of parameters having an impact only on the analysis precision.

val register_builtin : string -> unit

Registers available cvalue builtins for the -eva-builtin option.

val unregister_builtin : string -> unit

Unregister a cvalue builtin.

val register_domain : name:string -> descr:string -> priority:int -> unit

Registers available domain names for the -eva-domains option.