Frama-C API - Scalar
include Frama_c_kernel.Datatype.S_with_collections
include Frama_c_kernel.Datatype.S
include Frama_c_kernel.Datatype.S_no_copy
val descr : t Frama_c_kernel.Descr.tDatatype descriptor.
val packed_descr : Frama_c_kernel.Structural_descr.packPacked version of the descriptor.
val reprs : t listList of representants of the descriptor.
val hash : t -> intHash function: same spec than Hashtbl.hash.
val pretty : Stdlib.Format.formatter -> t -> unitPretty print each value in an user-friendly way.
val mem_project : (Frama_c_kernel.Project_skeleton.t -> bool) -> t -> boolmem_project f x must return true iff there is a value p of type Project.t in x such that f p returns true.
module Set : Frama_c_kernel.Datatype.Set with type elt = tmodule Map : Frama_c_kernel.Datatype.Map with type key = tmodule Hashtbl : Frama_c_kernel.Datatype.Hashtbl with type key = ttype scalar = tUseful constants in the field.
Two is provided for users that model floating point computations using abstractions over the field.
val zero : scalarval one : scalarval two : scalarval pos_inf : scalarval neg_inf : scalarScalar validity.
If the using type may produce invalid scalars, like NaNs for instance, it might be required to check scalar's validity.
val is_valid : scalar -> boolConstructors interacting with standard OCaml types.
val of_int : int -> scalarval of_float : float -> scalarval to_float : scalar -> floatval of_string : string -> scalarRound to a valid number in a given floating point format.
val represents : scalar:scalar -> in_format:'f Frama_c_kernel.Typed_float.format -> scalarStandard arithmetic unary operations.
Standard arithmetic binary operations.
Standard arithmetic relational operations.
Other arithmetic operations.
val pow2 : int -> scalarpow2 e computes the scalar 2 ^ e.
val log2 : scalar -> int Frama_c_kernel.Field.boundslog2 f computes the integer l and u such as l = floor(log₂ f) and u = ceiling(log₂ f).
val sqrt : scalar -> scalar Frama_c_kernel.Field.boundssqrt f computes bounds of the square root of f.