Module Abstract_value

module Abstract_value: sig .. end

Abstract numeric values of the analysis.


type 'v truth = [ `False | `True | `TrueReduced of 'v | `Unknown of 'v | `Unreachable ] 

Type for the truth value of an assertion in a value abstraction. The two last tags should be used only for a product of value abstractions.

type bound_kind = Alarms.bound_kind = 
| Lower_bound
| Upper_bound
type bound = 
| Int of Integer.t
| Float of float * Cil_types.fkind
type pointer_comparison = 
| Equality
| Relation
| Subtraction
module type S = sig .. end

Signature of abstract numerical values.

Key and structure for values. See , and where the mechanism is explained in detail.

type 'a key = 'a Structure.Key_Value.k 
type 'a structure = 'a Structure.Key_Value.structure 
module type Internal = sig .. end
module type External = sig .. end