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-wp.core/Wp/RegionAnnot/index.html

Module `Wp.RegionAnnot`Source

Sourcetype lrange =

| R_index of Frama_c_kernel.Cil_types.term
| R_range of Frama_c_kernel.Cil_types.term option * Frama_c_kernel.Cil_types.term option

Sourcetype lpath = {

loc : Frama_c_kernel.Cil_types.location;
lnode : lnode;
ltype : Frama_c_kernel.Cil_types.typ;

}

Sourceand lnode =

| L_var of Frama_c_kernel.Cil_types.varinfo
| L_region of string
| L_addr of lpath
| L_star of Frama_c_kernel.Cil_types.typ * lpath
| L_shift of lpath * Frama_c_kernel.Cil_types.typ * lrange
| L_index of lpath * Frama_c_kernel.Cil_types.typ * lrange
| L_field of lpath * Frama_c_kernel.Cil_types.fieldinfo list
| L_cast of Frama_c_kernel.Cil_types.typ * lpath

Sourcemodule Lpath : sig ... end

Sourcetype region_pattern =

| FREE
| PVAR
| PREF
| PMEM
| PVECTOR
| PMATRIX

Sourcetype region_spec = {

region_name : string option;
region_pattern : region_pattern;
region_lpath : lpath list;

}

Sourceval p_name : region_pattern -> string

Sourceval of_extension : Frama_c_kernel.Cil_types.acsl_extension -> region_spec list

Sourceval of_behavior : Frama_c_kernel.Cil_types.behavior -> region_spec list

Sourceval register : unit -> unit

Auto when `-wp-region`