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.kernel/Frama_c_kernel/Interpreted_automata/Compute/index.html

Module `Interpreted_automata.Compute`

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.