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

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

Operations on (natural) loops.

val is_natural : Cil_types.kernel_function -> Cil_types.stmt -> bool

val get_naturals : 
  Cil_types.kernel_function ->
  Cil_types.stmt list Cil_datatype.Stmt.Map.t

val is_non_natural : Cil_types.kernel_function -> Cil_types.stmt -> bool

val get_non_naturals : Cil_types.kernel_function -> Cil_datatype.Stmt.Set.t

val back_edges : 
  Cil_types.kernel_function ->
  Cil_types.stmt ->
  Cil_types.stmt list

Statements that are the origin of a back-edge to a natural loop.