package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-31.0-Gallium.tar.gz

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

doc/frama-c-wp.core/Wp/Pcond/class-engine/index.html

Class `Pcond.engine`Source

method name : env -> Wp__.Lang.F.term -> string

Printer Components

Generate a name for marked term

method mark : Wp__.Lang.F.marks -> Wp__.Conditions.step -> unit

Marks terms to share in step

method pp_clause : string Qed.Plib.printer

Default: "@{<wp:clause>...}"

method pp_stmt : string Qed.Plib.printer

Default: "@{<wp:stmt>...}"

method pp_comment : string Qed.Plib.printer

Default: "@{<wp:comment>(* ... *)}"

method pp_property : Frama_c_kernel.Property.t Qed.Plib.printer

Default: "@{<wp:property>(* ... *)}"

method pp_warning : Wp__.Warning.t Qed.Plib.printer

Default: "@{<wp:warning>Warning}..."

method pp_name : string Qed.Plib.printer

Default: Format.pp_print_string

method pp_core : Wp__.Lang.F.term Qed.Plib.printer

Default: plang#pp_sort

method pp_definition : Stdlib.Format.formatter ->
  string ->
  Wp__.Lang.F.term ->
  unit

method pp_intro : clause:string ->
  ?dot:string ->
  Wp__.Lang.F.pred Qed.Plib.printer

method pp_probe : Stdlib.Format.formatter ->
  Wp__.Probe.t ->
  Wp__.Lang.F.term ->
  unit

method pp_condition : Wp__.Conditions.step Qed.Plib.printer

method pp_block : clause:string -> Wp__.Conditions.sequence Qed.Plib.printer

method pp_goal : Wp__.Lang.F.pred Qed.Plib.printer

method pp_step : Wp__.Conditions.step Qed.Plib.printer

Assumes an "<hv>" box is opened.

method pp_block : clause:string -> Wp__.Conditions.sequence Qed.Plib.printer

Assumes an "<hv>" box is opened and all variables are named.

method pp_sequence : clause:string -> Wp__.Conditions.sequence Qed.Plib.printer

Assumes an "<hv>" box is opened and all variables are declared. (recursively used)

method pp_sequent : Wp__.Conditions.sequent Qed.Plib.printer

Print the sequent in global environment.

method pp_esequent : env -> Wp__.Conditions.sequent Qed.Plib.printer

Print the sequent in the given environment. The environment is enriched with the shared terms.

method get_ce_mode : bool

method set_ce_mode : bool -> unit

method update_ce_models : (Wp__.VCS.prover, Wp__.VCS.model) Stdlib.Hashtbl.t ->
  unit