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-e-acsl.core/E_ACSL/Exit_points/index.html

Module `E_ACSL.Exit_points`

E-ACSL tracks a local variable by injecting:

a call to __e_acsl_store_block at the beginning of its scope, and
a call to __e_acsl_delete_block at the end of the scope. This is not always sufficient to track variables because execution may exit a scope early (for instance via a goto or a break statement). This module computes program points at which extra delete_block statements need to be added to handle such early scope exits.

val generate : Frama_c_kernel.Cil_types.fundec -> unit

Visit a function and populate data structures used to compute exit points

val clear : unit -> unit

Clear all gathered data

val delete_vars : 
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_datatype.Varinfo.Set.t

Given a statement which potentially leads to an early scope exit (such as goto, break or continue) return the list of local variables which need to be removed from tracking before that statement is executed. Before calling this function generate need to be executed.

val store_vars : 
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_datatype.Varinfo.Set.t

Compute variables that should be re-recorded before a labelled statement to which some goto jumps.