Module `Scope.Datascope`Source

Source

val get_data_scope_at_stmt : 
  Frama_c_kernel.Kernel_function.t ->
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.lval ->
  Frama_c_kernel.Cil_datatype.Stmt.Hptset.t
  * (Frama_c_kernel.Cil_datatype.Stmt.Hptset.t
     * Frama_c_kernel.Cil_datatype.Stmt.Hptset.t)

raises Kernel_function.No_Definition
if kf has no definition.

returns
3 statement sets related to the value of lval before stmt :
- the forward selection,
- the both way selection,
- the backward selection.

Source

val get_prop_scope_at_stmt : 
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.code_annotation ->
  Frama_c_kernel.Cil_datatype.Stmt.Hptset.t
  * Frama_c_kernel.Cil_types.code_annotation list

compute the set of statements where the given annotation has the same value as before the given stmt. Also returns the eventual code annotations that are implied by the one given as argument.

Sourceval check_asserts : unit -> Frama_c_kernel.Cil_types.code_annotation list

Print how many assertions could be removed based on the previous analysis (get_prop_scope_at_stmt) and return the annotations that can be removed.

Sourceval rm_asserts : unit -> unit

Same analysis than check_asserts but mark the assertions as proven.

module R : Frama_c_kernel.Plugin.General_services

for internal use

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-scope.core/Scope/Datascope/index.html

Module `Scope.Datascope`Source

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-scope.core/Scope/Datascope/index.html

Module Scope.DatascopeSource

Module `Scope.Datascope`Source