package frama-c

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

This module defines the previous functions without memoization

val get_automaton : annotations:bool -> Cil_types.kernel_function -> automaton

Get the interpreted automaton for the given kernel_function. Note that the automata construction may lead to the build of new Cil expressions which will be different at each call: you may need to memoize the results of this function.

val build_wto : automaton -> wto

Build the wto for the given automaton (No memoization, use get_wto instead)

val exit_strategy : graph -> vertex Wto.component -> wto

Extract an exit strategy from a component, i.e. a sub-wto where all vertices lead outside the wto without passing through the head.

val output_to_dot : out_channel -> ?labeling:vertex labeling -> ?wto:wto -> automaton -> unit

Output the automaton in dot format

type wto_index_table
val build_wto_index_table : wto -> wto_index_table

Compute the index table from a wto

val get_wto_index : wto_index_table -> vertex -> wto_index
  • returns

    the wto_index for a statement

val wto_index_diff : wto_index -> wto_index -> vertex list * vertex list
  • returns

    the components left and the components entered when going from one index to another

val get_wto_index_diff : wto_index_table -> vertex -> vertex -> vertex list * vertex list
  • returns

    the components left and the components entered when going from one vertex to another

val is_wto_head : wto_index_table -> vertex -> bool
  • returns

    wether v is a component head or not

val is_back_edge : wto_index_table -> (vertex * vertex) -> bool
  • returns

    wether v1,v2 is a back edge of a loop, i.e. if the vertex v1 is a wto head of any component where v2 is included. This assumes that (v1,v2) is actually an edge present in the control flow graph.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet 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