Up – Package index » frama-c » Library numerors » Numerors » DomainModule Numerors.Domain Source Numerors' abstract domain, which computes a sound overapproximation of the floating-point semantic through the whole program. The domain's memory model is for now based on the <Simple_memory> functor provided by Eva. A reduced product with the Cvalue domain is performed at each step. For more details, one can look at M. Jacquemin's thesis.
frama-c Library Pdg_types Library crowbar_utils Library frama-c-acsl-importer.core Library frama-c-alias.core Library frama-c-aorai.core Library frama-c-api_generator.core Library frama-c-callgraph.core Library frama-c-constant_propagation.core Library frama-c-dive.core Library frama-c-e-acsl.core Library frama-c-eva.core Library frama-c-eva.numerors Library frama-c-eva.server_api Library frama-c-from.core Library frama-c-impact.core Library frama-c-inout.core Library frama-c-instantiate.core Library frama-c-loop-analysis.core Library frama-c-markdown-report.core Library frama-c-markdown-report.eva-info Library frama-c-metrics.core Library frama-c-nonterm.core Library frama-c-obfuscator.core Library frama-c-occurrence.core Library frama-c-pdg.core Library frama-c-pdg.types Library frama-c-reduc.core Library frama-c-region.core Library frama-c-report.core Library frama-c-rtegen.core Library frama-c-scope.core Library frama-c-security_slicing.core Library frama-c-server.core Library frama-c-slicing.core Library frama-c-sparecode.core Library frama-c-studia.core Library frama-c-volatile.core Library frama-c-wp.core Library frama-c.analysis-scripts Library frama-c.boot Library frama-c.fc_internal_z Library frama-c.init Library frama-c.kernel Library markdown_report_eva_info Library numerors Library ppx_z_literals Library qed Sources Source val registered : Eva__.Abstractions.Domain.registered