Frama-C API - `Cvalue_domain`

Main domain of the Value Analysis.

module State : Abstract_domain.Leaf with type value = Main_values.CVal.t and type location = Main_locations.PLoc.location and type state = Frama_c_kernel.Cvalue.Model.t * Locals_scoping.clobbered_set

val registered : Abstractions.Domain.registered

Specific functions for partitioning optimizations.

type prefix

module Subpart : Frama_c_kernel.Hashtbl.HashedType

val distinct_subpart : State.t -> State.t -> (prefix * Subpart.t * Subpart.t) option

val find_subpart : State.t -> prefix -> Subpart.t option

Special getters.

module type Getters = sig ... end

module Getters (Dom : Abstract.Domain.External) : Getters with type t := Dom.t

Frama-C API - Cvalue_domain

Frama-C API - `Cvalue_domain`