package frama-c

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
method model : Wp__.WpContext.model

Generate VCs for the given Property.

Generate VCs for call preconditions at the given statement.

Generate VCs for all functions matching provided behaviors and property names. For `~bhv` and `~prop` optional arguments, default and empty list means all properties.

method compute_main : ?fct:Wp__.Wp_parameters.functions -> ?bhv:string list -> ?prop:string list -> unit -> t Frama_c_kernel.Bag.t
OCaml

Innovation. Community. Security.