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 (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-30.0-Zinc.tar.gz

sha256=3ac0f995261ec829a7bd042bf70fc29ac6379029eb9df30bcc044748eb4d2a56

doc/frama-c-eva.core/Eva/Eva_ast/index.html

Module `Eva.Eva_ast`

Eva Syntax Tree.

type origin =

| Lval of Frama_c_kernel.Cil_types.lval
| Exp of Frama_c_kernel.Cil_types.exp
| Term of Frama_c_kernel.Cil_types.identified_term
| Built

type 'a tag = private {

node : 'a;
typ : Frama_c_kernel.Cil_types.typ;
origin : origin;

}

type typ = Frama_c_kernel.Cil_types.typ

type varinfo = Frama_c_kernel.Cil_types.varinfo

type exp = exp_node tag

and exp_node =

| Const of constant
| Lval of lval
| UnOp of unop * exp * typ
| BinOp of binop * exp * exp * typ
| CastE of typ * exp
| AddrOf of lval
| StartOf of lval

and constant =

| CTopInt of ikind
| CInt64 of Frama_c_kernel.Integer.t * ikind * string option
| CString of Frama_c_kernel.Base.t
| CChr of char
| CReal of float * fkind * string option
| CEnum of Frama_c_kernel.Cil_types.enumitem * exp

Constants

and lval = lval_node tag

and lval_node = lhost * offset

and lhost =

| Var of varinfo
| Mem of exp

and offset =

| NoOffset
| Field of Frama_c_kernel.Cil_types.fieldinfo * offset
| Index of exp * offset

and ikind = Frama_c_kernel.Cil_types.ikind

and fkind = Frama_c_kernel.Cil_types.fkind

and unop =

| Neg
| BNot
| LNot

and binop =

| PlusA
| PlusPI
| MinusA
| MinusPI
| MinusPP
| Mult
| Div
| Mod
| Shiftlt
| Shiftrt
| Lt
| Gt
| Le
| Ge
| Eq
| Ne
| BAnd
| BXor
| BOr
| LAnd
| LOr

type init =

| SingleInit of exp * Frama_c_kernel.Cil_types.location
| CompoundInit of typ * (offset * init) list

Structural comparaison and equality functions, generated by ppx deriving. Equivalent to the functions provided by Cil_datatype.ConstantStrict and Cil_datatype.ExpStructEqStrict.

val compare_constant : constant -> constant -> int

val equal_constant : constant -> constant -> bool

val compare_exp : exp -> exp -> int

val equal_exp : exp -> exp -> bool

val compare_lval : lval -> lval -> int

val equal_lval : lval -> lval -> bool

val compare_lhost : lhost -> lhost -> int

val equal_lhost : lhost -> lhost -> bool

val compare_offset : offset -> offset -> int

val equal_offset : offset -> offset -> bool

val mk_tag : 
  node:'a ->
  typ:Frama_c_kernel.Cil_types.typ ->
  origin:origin ->
  'a tag

Tag builder for Eva_ast_builder only.

alert eva_ast_builder For internal use only; use mk_exp and mk_lval builders instead.

val type_of_exp_node : 
  Eva__.Eva_ast_types.exp_node ->
  Frama_c_kernel.Cil_types.typ

val type_of_lval_node : 
  (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) ->
  Frama_c_kernel.Cil_types.typ

val type_of_lhost : Eva__.Eva_ast_types.lhost -> Frama_c_kernel.Cil_types.typ

val pp_lval : 
  Stdlib.Format.formatter ->
  (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset)
    Eva__.Eva_ast_types.tag ->
  unit

val pp_offset : Stdlib.Format.formatter -> Eva__.Eva_ast_types.offset -> unit

val pp_exp : 
  Stdlib.Format.formatter ->
  Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag ->
  unit

val pp_constant : 
  Stdlib.Format.formatter ->
  Eva__.Eva_ast_types.constant ->
  unit

val pp_unop : Stdlib.Format.formatter -> Eva__.Eva_ast_types.unop -> unit

val pp_binop : Stdlib.Format.formatter -> Eva__.Eva_ast_types.binop -> unit

module Lhost : 
  Frama_c_kernel.Datatype.S_with_collections
    with type t = Eva__.Eva_ast_types.lhost

module Offset : 
  Frama_c_kernel.Datatype.S_with_collections
    with type t = Eva__.Eva_ast_types.offset

module Lval : 
  Frama_c_kernel.Datatype.S_with_collections
    with type t =
           (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset)
             Eva__.Eva_ast_types.tag

module Exp : 
  Frama_c_kernel.Datatype.S_with_collections
    with type t = Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag

module Constant : 
  Frama_c_kernel.Datatype.S_with_collections
    with type t = Eva__.Eva_ast_types.constant

val mk_exp : 
  Eva__.Eva_ast_types.exp_node ->
  Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag

val mk_lval : 
  (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) ->
  (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset)
    Eva__.Eva_ast_types.tag

val translate_exp : 
  Frama_c_kernel.Cil_types.exp ->
  Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag

val translate_lval : 
  Frama_c_kernel.Cil_types.lval ->
  (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset)
    Eva__.Eva_ast_types.tag

val translate_offset : 
  Frama_c_kernel.Cil_types.offset ->
  Eva__.Eva_ast_types.offset

val translate_unop : Frama_c_kernel.Cil_types.unop -> Eva__.Eva_ast_types.unop

val translate_binop : 
  Frama_c_kernel.Cil_types.binop ->
  Eva__.Eva_ast_types.binop

val translate_init : Frama_c_kernel.Cil_types.init -> Eva__.Eva_ast_types.init

val invert_relation : Eva__.Eva_ast_types.binop -> Eva__.Eva_ast_types.binop

Inverse a relation, op must be a comparison operator

val conv_relation : 
  Eva__.Eva_ast_types.binop ->
  Frama_c_kernel.Abstract_interp.Comp.t

Convert a relation to Abstract_interp.Comp, op must be a comparison operator

val normalize_condition : 
  Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag ->
  bool ->
  Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag

normalize_condition e positive returns the expression corresponding to e != 0 when positive is true, and e == 0 otherwise. The resulting expression will always have a comparison operation at its root.

val add_offset : 
  (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset)
    Eva__.Eva_ast_types.tag ->
  Eva__.Eva_ast_types.offset ->
  (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset)
    Eva__.Eva_ast_types.tag

module Build : sig ... end

Conversion to Cil

val to_cil_exp : 
  Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag ->
  Frama_c_kernel.Cil_types.exp

val to_cil_lval : 
  (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset)
    Eva__.Eva_ast_types.tag ->
  Frama_c_kernel.Cil_types.lval

Queries

val is_mutable : 
  (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset)
    Eva__.Eva_ast_types.tag ->
  bool

Cf Cil.is_mutable_or_initialized.

val is_initialized : 
  (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset)
    Eva__.Eva_ast_types.tag ->
  bool

Expressions/Lvalue heights

val height_exp : Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag -> int

Computes the height of an expression, that is the maximum number of nested operations in this expression.

val height_lval : 
  (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset)
    Eva__.Eva_ast_types.tag ->
  int

Computes the height of an lvalue.

Specialized visitors

val exp_contains_volatile : 
  Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag ->
  bool

exp_contains_volatile e (resp. lval_contains_volatile lv is true whenever one l-value contained inside the expression e (resp. the lvalue lv) has volatile qualifier. Relational analyses should not learn anything on such values.

val lval_contains_volatile : 
  (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset)
    Eva__.Eva_ast_types.tag ->
  bool

val vars_in_exp : 
  Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag ->
  Frama_c_kernel.Cil_datatype.Varinfo.Set.t

Returns the set of variables that syntactically appear in an expression or lvalue.

val vars_in_lval : 
  (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset)
    Eva__.Eva_ast_types.tag ->
  Frama_c_kernel.Cil_datatype.Varinfo.Set.t

Dependences of expressions and lvalues.

val zone_of_exp : 
  ((Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset)
     Eva__.Eva_ast_types.tag ->
    Frama_c_kernel.Precise_locs.precise_location) ->
  Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag ->
  Frama_c_kernel.Locations.Zone.t

Given a function computing the location of lvalues, computes the memory zone on which the value of an expression depends.

val zone_of_lval : 
  ((Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset)
     Eva__.Eva_ast_types.tag ->
    Frama_c_kernel.Precise_locs.precise_location) ->
  (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset)
    Eva__.Eva_ast_types.tag ->
  Frama_c_kernel.Locations.Zone.t

Given a function computing the location of lvalues, computes the memory zone on which the value of an lvalue depends.

val indirect_zone_of_lval : 
  ((Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset)
     Eva__.Eva_ast_types.tag ->
    Frama_c_kernel.Precise_locs.precise_location) ->
  (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset)
    Eva__.Eva_ast_types.tag ->
  Frama_c_kernel.Locations.Zone.t

Given a function computing the location of lvalues, computes the memory zone on which the offset and the pointer expression (if any) of an lvalue depend.

val deps_of_exp : 
  ((Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset)
     Eva__.Eva_ast_types.tag ->
    Frama_c_kernel.Precise_locs.precise_location) ->
  Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag ->
  Deps.t

Given a function computing the location of lvalues, computes the memory dependencies of an expression.

val deps_of_lval : 
  ((Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset)
     Eva__.Eva_ast_types.tag ->
    Frama_c_kernel.Precise_locs.precise_location) ->
  (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset)
    Eva__.Eva_ast_types.tag ->
  Deps.t

Given a function computing the location of lvalues, computes the memory dependencies of an lvalue.

Constant conversion and folding.

val const_fold : 
  Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag ->
  Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag

val fold_to_integer : 
  Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag ->
  Frama_c_kernel.Integer.t option

val is_zero_ptr : Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag -> bool

Offsets

val last_offset : Eva__.Eva_ast_types.offset -> Eva__.Eva_ast_types.offset

Returns the last offset in the chain.

val is_bitfield : 
  (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset)
    Eva__.Eva_ast_types.tag ->
  bool

Is an lvalue a bitfield?

module Rewrite : sig ... end

Folding visitor

module Fold : sig ... end