frama-c

API

Library Pdg_types

• Pdg_types

Library crowbar_utils

• Crowbar_utils

Library frama-c-acsl-importer.core

• Acsl_importer

Library frama-c-alias.core

• Alias Interface for the Alias plug-in.

Library frama-c-aorai.core

• Aorai Aorai plugin (AKA Ltl_to_acsl). No function is directly exported: they are registered in Db.Aorai.

Library frama-c-api_generator.core

• Api_generator

Library frama-c-callgraph.core

• Callgraph Callgraph plugin.

Library frama-c-constant_propagation.core

• Constant_Propagation Constant propagation analysis.

Library frama-c-dive.core

• Dive

Library frama-c-e-acsl.core

• E_ACSL E-ACSL.

Library frama-c-eva.core

• Eva Eva public API.

Library frama-c-eva.numerors

No module.

Library frama-c-eva.server_api

• Server_api

Library frama-c-from.core

• From

Library frama-c-impact.core

• Impact

Library frama-c-inout.core

• Inout

Library frama-c-instantiate.core

• Instantiate

Library frama-c-loop-analysis.core

• LoopAnalysis Loop Analysis plugin.

Library frama-c-markdown-report.core

• Markdown_report

Library frama-c-markdown-report.eva-info

No module.

Library frama-c-metrics.core

• Metrics Metrics plugin.

Library frama-c-nonterm.core

• Nonterm

Library frama-c-obfuscator.core

• Obfuscator Obfuscator plug-in.

Library frama-c-occurrence.core

• Occurrence

Library frama-c-pdg.core

• Pdg Program Dependences Graph.

Library frama-c-pdg.types

No module.

Library frama-c-reduc.core

• Reduc

Library frama-c-region.core

• Region

Library frama-c-report.core

• Report

Library frama-c-rtegen.core

• RteGen Consult internal plug-in documentation for more details

Library frama-c-scope.core

• Scope Scope analysis.

Library frama-c-security_slicing.core

• Security_slicing Security slicing.

Library frama-c-server.core

• Server

Library frama-c-slicing.core

• Slicing

Library frama-c-sparecode.core

• Sparecode Sparecode analysis.

Library frama-c-studia.core

• Studia

Library frama-c-volatile.core

• Volatile

Library frama-c-wp.core

• Wp This the API of the WP plug-in

Library frama-c.analysis-scripts

• Analysis_scripts

Library frama-c.boot

• Frama_c_boot

Library frama-c.fc_internal_z

• Fc_internal_z This module/library is used to avoid shadowing Z from Zarith in our own Z module.

Library frama-c.init

• Frama_c_very_first

Library frama-c.kernel

• Frama_c_kernel

Library markdown_report_eva_info

• Markdown_report_eva_info

Library numerors

• Numerors

Library ppx_z_literals

• Ppx_z_literals

Library qed

• Qed