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 (23)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c-wp.core/Wp/StmtSemantics/Make/index.html

Module `StmtSemantics.Make`Source

Parameters

module Compiler : Sigs.Compiler

Signature

Sourcemodule Cfg : CfgCompiler.Cfg with module S = Compiler.M.Sigma

Sourcetype node = Cfg.node

Sourcetype goal = {

goal_pred : Cfg.P.t;
goal_prop : WpPropId.prop_id;

}

Sourcetype cfg = Cfg.cfg

Sourcetype paths = {

paths_cfg : cfg;
paths_goals : goal Frama_c_kernel.Bag.t;

}

Sourceval goals_nodes : goal Frama_c_kernel.Bag.t -> Cfg.Node.Set.t

Sourceexception LabelNotFound of Clabels.c_label

Compilation environment

Sourcetype env

Sourceval empty_env : Frama_c_kernel.Kernel_function.t -> env

Sourceval bind : Clabels.c_label -> node -> env -> env

Sourceval result : env -> Lang.F.var

Sourceval (@^) : paths -> paths -> paths

Same as Cfg.concat

Sourceval (@*) : env -> (Clabels.c_label * node) list -> env

fold bind

Sourceval (@:) : env -> Clabels.c_label -> node

LabelMap.find with refined excpetion.

raises LabelNotFound
instead of Not_found

Sourceval (@-) : env -> (Clabels.c_label -> bool) -> env

Sourceval sequence : (env -> 'a -> paths) -> env -> 'a list -> paths

Chain compiler by introducing fresh nodes between each element of the list. For each consecutive x;y elements, a fresh node n is created, and x is compiled with Next:n and y is compiled with Here:n.

Source

val choice : 
  ?pre:Clabels.c_label ->
  ?post:Clabels.c_label ->
  (env -> 'a -> paths) ->
  env ->
  'a list ->
  paths

Chain compiler in parallel, between labels ~pre and ~post, which defaults to resp. here and next. The list of eventualities is exhastive, hence an either assumption is also inserted.

Source

val parallel : 
  ?pre:Clabels.c_label ->
  ?post:Clabels.c_label ->
  (env -> 'a -> Cfg.C.t * paths) ->
  env ->
  'a list ->
  paths

Chain compiler in parallel, between labels ~pre and ~post, which defaults to resp. here and next. The list of eventualities is exhastive, hence an either assumption is also inserted.

Instructions Compilation

Each instruction or statement is typically compiled between Here and Next nodes in the flow. Pre, Post and Exit are reserved for the entry and exit points of current function. in flow are used when needed such as Break and Continue and should be added before calling.

Source

val set : 
  env ->
  Frama_c_kernel.Cil_types.lval ->
  Frama_c_kernel.Cil_types.exp ->
  paths

Sourceval scope : env -> Sigs.scope -> Frama_c_kernel.Cil_types.varinfo list -> paths

Sourceval instr : env -> Frama_c_kernel.Cil_types.instr -> paths

Sourceval return : env -> Frama_c_kernel.Cil_types.exp option -> paths

Sourceval assume : Cfg.P.t -> paths

Source

val call_kf : 
  env ->
  Frama_c_kernel.Cil_types.lval option ->
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.exp list ->
  paths

Source

val call : 
  env ->
  Frama_c_kernel.Cil_types.lval option ->
  Frama_c_kernel.Cil_types.exp ->
  Frama_c_kernel.Cil_types.exp list ->
  paths

ACSL Compilation

Sourceval spec : env -> Frama_c_kernel.Cil_types.spec -> paths

Source

val assume_ : 
  env ->
  Sigs.polarity ->
  Frama_c_kernel.Cil_types.predicate ->
  paths

Sourceval assigns : env -> Frama_c_kernel.Cil_types.assigns -> paths

Sourceval froms : env -> Frama_c_kernel.Cil_types.from list -> paths

Automata Compilation

Sourceval automaton : env -> Frama_c_kernel.Interpreted_automata.automaton -> paths

Sourceval init : is_pre_main:bool -> env -> paths

Sourceval compute_kf : Frama_c_kernel.Kernel_function.t -> paths * node

Full Compilation

Returns the set of all paths for the function, with all proof obligations. The returned node corresponds to the Init label.

On This Page

Parameters
Signature

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-wp.core/Wp/StmtSemantics/Make/index.html

Module StmtSemantics.MakeSource

Parameters

Signature

Instructions Compilation

ACSL Compilation

Automata Compilation

Module `StmtSemantics.Make`Source