Module Eva

module Eva: sig .. end

Analysis for values and pointers


module Value_results: sig .. end
module Value_parameters: sig .. end
module Eval_terms: sig .. end
module Unit_tests: sig .. end
module Eva_annotations: sig .. end

Register special annotations to locally guide the partitioning of states performed by an Eva analysis.

module Builtins: sig .. end

Analysis builtins for the cvalue domain, more efficient than the analysis of the C functions.