Frama-C:
Plug-ins:
Libraries:

Frama-C API - Main_values

Main numeric values of Eva that can be used by abstract domains.

module CVal : Abstract_value.Leaf with type t = Frama_c_kernel.Cvalue.V.t and type context = unit

Main abstract values built over Cvalue.V, used by most domains.

module Interval : Abstract_value.Leaf with type t = Frama_c_kernel.Ival.t option and type context = unit

Dummy intervals: no forward nor backward propagations, only used as a reduced product with CVal above. None is top.

module Sign : Abstract_value.Leaf with type t = Sign_value.t and type context = unit

Simple sign values, used by the sign domain.