package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

Normalization of Annotations.

Labels are renamed wrt NormAtLabels and reorganized for use/prove dispatching in CfgCalculus.

type behavior = {
  1. bhv_assumes : WpPropId.pred_info list;
  2. bhv_requires : WpPropId.pred_info list;
  3. bhv_smokes : WpPropId.pred_info list;
  4. bhv_ensures : WpPropId.pred_info list;
  5. bhv_exits : WpPropId.pred_info list;
  6. bhv_post_assigns : WpPropId.assigns_full_info;
  7. bhv_exit_assigns : WpPropId.assigns_full_info;
}
val get_preconditions : goal:bool -> Frama_c_kernel.Cil_types.kernel_function -> WpPropId.pred_info list
val get_behavior_goals : Frama_c_kernel.Cil_types.kernel_function -> ?smoking:bool -> ?exits:bool -> Frama_c_kernel.Cil_types.funbehavior -> behavior
type code_assertion = {
  1. code_admitted : WpPropId.pred_info option;
  2. code_verified : WpPropId.pred_info option;
}
val get_code_assertions : ?smoking:bool -> Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.stmt -> code_assertion list
type loop_hypothesis =
  1. | NoHyp
  2. | Check of WpPropId.prop_id
  3. | Always of WpPropId.prop_id
type loop_invariant = {
  1. loop_hyp : loop_hypothesis;
  2. loop_est : WpPropId.prop_id option;
  3. loop_ind : WpPropId.prop_id option;
  4. loop_pred : Frama_c_kernel.Cil_types.predicate;
}
type loop_contract = {
  1. loop_terminates : Frama_c_kernel.Cil_types.predicate option;
  2. loop_invariants : loop_invariant list;
    (*

    to be proved after loop invariants

    *)
  3. loop_smoke : WpPropId.pred_info list;
    (*

    assigned by loop body

    *)
  4. loop_assigns : WpPropId.assigns_full_info list;
}
type contract = {
  1. contract_cond : WpPropId.pred_info list;
  2. contract_hpre : WpPropId.pred_info list;
  3. contract_post : WpPropId.pred_info list;
  4. contract_exit : WpPropId.pred_info list;
  5. contract_smoke : WpPropId.pred_info list;
  6. contract_assigns : Frama_c_kernel.Cil_types.assigns;
  7. contract_terminates : bool * Frama_c_kernel.Cil_types.predicate;
  8. contract_decreases : Frama_c_kernel.Cil_types.variant option;
}
val clear : unit -> unit
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events Blog Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct