Abstract_interp (p.frama-c.28.0.doc.frama-c.kernel.Frama_c_kernel.Abstract

frama-c
- README
- Library Pdg_types
  - Pdg_types
- Library frama-c-alias.core
  - Alias
- Library frama-c-aorai.core
  - Aorai
- Library frama-c-api-generator.core
  - Api_generator
- Library frama-c-callgraph.core
  - Callgraph
- Library frama-c-constant_propagation.core
  - Constant_Propagation
- Library frama-c-dive.core
  - Dive
- Library frama-c-e-acsl.core
  - E_ACSL
- Library frama-c-eva.core
  - Eva
- Library frama-c-eva.gui
  - Eva_gui
- Library frama-c-from.core
  - From
- Library frama-c-from.gui
  - From_gui
- Library frama-c-impact.core
  - Impact
- Library frama-c-impact.gui
  - Impact_gui
- Library frama-c-inout.core
  - Inout
- Library frama-c-instantiate.core
  - Instantiate
- Library frama-c-loop-analysis.core
  - LoopAnalysis
- Library frama-c-markdown-report.core
  - Markdown_report
- Library frama-c-markdown-report.eva-info
- Library frama-c-metrics.core
  - Metrics
- Library frama-c-metrics.gui
  - Metrics_gui
- Library frama-c-nonterm.core
  - Nonterm
- Library frama-c-obfuscator.core
  - Obfuscator
- Library frama-c-occurrence.core
  - Occurrence
- Library frama-c-occurrence.gui
  - Occurrence_gui
- Library frama-c-pdg.core
  - Pdg
- Library frama-c-pdg.types
- Library frama-c-postdominators.core
  - Postdominators
- Library frama-c-reduc.core
  - Reduc
- Library frama-c-report.core
  - Report
- Library frama-c-rtegen.core
  - RteGen
- Library frama-c-rtegen.gui
  - Rtegen_gui
- Library frama-c-scope.core
  - Scope
- Library frama-c-scope.gui
  - Scope_gui
- Library frama-c-security_slicing.core
  - Security_slicing
- Library frama-c-security_slicing.gui
  - Security_slicing_gui
- Library frama-c-server.core
  - Server
- Library frama-c-slicing.core
  - Slicing
- Library frama-c-slicing.gui
  - Slicing_gui
- Library frama-c-sparecode.core
  - Sparecode
- Library frama-c-studia.core
  - Studia
- Library frama-c-studia.gui
  - Studia_gui
- Library frama-c-users.core
  - Users
- Library frama-c-variadic.core
  - Variadic
- Library frama-c-wp.core
  - Wp
- Library frama-c-wp.gui
  - Wp_gui
- Library frama-c.analysis-scripts
  - Analysis_scripts
- Library frama-c.boot
  - Frama_c_boot
- Library frama-c.gui
  - Frama_c_gui
- Library frama-c.init
- Library frama-c.kernel
  - Frama_c_kernel
- Library frama_c_very_first_cmdline
- Library frama_c_very_first_gui
- Library markdown_report_eva_info
  - Markdown_report_eva_info
- Library qed
  - Qed
- Sources

exception Error_Top

Raised by some functions when encountering a top value.

exception Error_Bottom

Raised by Lattice_Base.project.

exception Not_less_than

Raised by Lattice.cardinal_less_than.

exception Can_not_subdiv

Used by other modules e.g. Fval.subdiv_float_interval.

type truth =

| True
| False
| Unknown
(*
Truth values with a possibility for 'Unknown'
*)

val inv_truth : truth -> truth

module Comp : sig ... end

Signatures for comparison operators ==, !=, <, >, <=, >=.

module Int : sig ... end

module Rel : sig ... end

"Relative" integers. They are subtraction between two absolute integers

module Bool : sig ... end

module Make_Lattice_Base
  (V : Lattice_type.Lattice_Value) : 
  Lattice_type.Lattice_Base with type l = V.t

module Make_Lattice_Set
  (V : Datatype.S)
  (Set : Lattice_type.Hptset with type elt = V.t) : 
  Lattice_type.Lattice_Set with module O = Set

module Make_Hashconsed_Lattice_Set
  (V : Hptmap.Id_Datatype)
  (Set : Hptset.S with type elt = V.t) : 
  Lattice_type.Lattice_Set with module O = Set

See e.g. base.ml and locations.ml to see how this functor should be applied. The O module passed as argument is the same as O in the result. It is passed here to avoid having multiple modules calling Hptset.Make on the same argument (which is forbidden by the datatype library, and would cause hashconsing problems)

module type Collapse = sig ... end

module Make_Lattice_Product
  (L1 : Lattice_type.AI_Lattice_with_cardinal_one)
  (L2 : Lattice_type.AI_Lattice_with_cardinal_one)
  (_ : Collapse) : 
  Lattice_type.Lattice_Product with type t1 = L1.t and type t2 = L2.t

If C.collapse then L1.bottom,_ = _,L2.bottom = bottom

module Make_Lattice_UProduct
  (L1 : Lattice_type.AI_Lattice_with_cardinal_one)
  (L2 : Lattice_type.AI_Lattice_with_cardinal_one) : 
  Lattice_type.Lattice_UProduct with type t1 = L1.t and type t2 = L2.t

Uncollapsed product. Literally the set of (e1, e2) ordered pairs equipped with the order (e1, e2) < (d1, d2) <==> e1 < d1 && e2 < d2.

module Make_Lattice_Sum
  (L1 : Lattice_type.AI_Lattice_with_cardinal_one)
  (L2 : Lattice_type.AI_Lattice_with_cardinal_one) : 
  Lattice_type.Lattice_Sum with type t1 = L1.t and type t2 = L2.t