
{2 Presentation}

The WP plugin is dedicated to formally prove ACSL annotations
and contracts by {i Weakest Precondition Calculus}.

Dynamically registered API is now deprecated and replaced by
a full featured OCaml interface. To use it, simply add
[PLUGIN_DEPENDENCIES+=Wp] in your Plug-in Makefile.

{2 Plugin API}

 - {{:../wp/Wp.html}OCaml API}
 - {{:../dynamic_plugins/Dynamic_plugins.Wp.html}Dynamic API} ({b deprecated})


{2 API Documentation}

The Wp API is dynamically registered.

 - {{:../index.html}Frama-C} complete kernel API
 - {{:../html/Dynamic.html}Dynamic} kernel registry for plugins' API
 - {{:../dynamic_plugins/Dynamic_plugins.html} Dynamically registered plugins} API index

{2 Plugin Internal Documentation}

 - {{:modules.svg}Wp} architecture (SVG format)
 - Index of {{:index_modules.html}Modules}
 - Index of {{:index_types.html}Types}
 - Index of {{:index_values.html}Values}
 - Index of {{:index_exceptions.html}Exceptions}

