package mopsa

  1. Overview
  2. Docs
package mopsa
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Pointer_sentinel.Domain

Domain header

*****************

include sig ... end
val id : unit Mopsa_analyzer__Framework__Core__Id.id
val name : string
val debug : ('a, Format.formatter, unit, unit) format4 -> 'a
val scalar : MopsaLib.route
val universal : MopsaLib.route
val checks : 'a list

Auxiliary variables

***********************

type MopsaLib.var_kind +=
  1. | V_c_sentinel_pos of Common.Base.base
  2. | V_c_before_sentinel of Common.Base.base
  3. | V_c_sentinel of Common.Base.base

Registration of a new var kinds for auxiliary variables

val void_ptr : MopsaLib.typ

void* type

Size of a pointer cell

/!\ Currently, sizeof_type is initialized *after* options are parsed. It cannot be used to initialize a constant here

let ptr_size = sizeof_type void_ptr

val mk_sentinel_pos_var : Common.Base.base -> MopsaLib.var

Create the auxiliary variable sentinel(base)

val mk_before_var : Common.Base.base -> MopsaLib.var

Create the auxiliary variable before-sentinel(base)

val mk_sentinel_var : Common.Base.base -> MopsaLib.var

Create the auxiliary variable at-sentinel(base)

val before_cases : exists:('a Core.Flow.flow -> ('a, 'b) Core.Cases.cases) -> empty:('a Core.Flow.flow -> ('a, 'b) Core.Cases.cases) -> MopsaLib.expr -> Mopsa_utils.Core.Location.range -> ('a, 'c) Framework.Core.Manager.man -> 'a Core.Flow.flow -> ('a, 'b) Core.Cases.cases
val sentinel_cases : exists:('a Core.Flow.flow -> ('a, 'b) Core.Cases.cases) -> empty:('a Core.Flow.flow -> ('a, 'b) Core.Cases.cases) -> MopsaLib.expr -> MopsaLib.expr -> Mopsa_utils.Core.Location.range -> ('a, 'c) Framework.Core.Manager.man -> 'a Core.Flow.flow -> ('a, 'b) Core.Cases.cases

Initialization procedure

****************************

val init : 'a -> 'b -> 'c -> 'd option

Abstract transformers

*************************

val eval_pointed_base_offset : MopsaLib.expr -> 'a -> ('b, 'c) MopsaLib.man -> 'b Core.Flow.flow -> ('b, (Common.Base.base * MopsaLib.expr * MopsaLib.mode option) option) Mopsa_analyzer.MopsaLib.Cases.cases

Get the base and offset pointed by ptr. Since we do not track invalid dereferences, we ignore invalid pointers.

val is_scalar_base : Common.Base.base -> bool
val is_interesting_base : Common.Base.base -> bool

Predicate defining interesting bases for which the domain will track the sentinel position.

val is_sentinel_expr : MopsaLib.expr -> ('a, 'b) MopsaLib.man -> 'a Core.Flow.flow -> ('a, bool) Mopsa_analyzer.MopsaLib.Cases.cases

Partition flow depending whether e is a sentinel or not

Add a base to the domain's dimensions

Remove the auxiliary variables of a base

Rename the auxiliary variables associated to a base

Expand the auxiliary variables of a base

Fold the auxiliary variables of a set of bases

Forget the value of auxiliary variables of a base

Declaration of a C variable

Cases of the abstract transformer for 𝕊⟦ *p = rval; ⟧

Assignment abstract transformer

Transformers entry point

Abstract evaluations

************************

Cases of the abstraction evaluations

Abstract evaluation of a dereference

Cases of the transfer function of quantified tests 𝕊⟦ ∀i ∈ lo,hi: *(base + i) op q ⟧

val assume_exists_ne : 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j Core.Flow.flow -> 'j Mopsa_analyzer.MopsaLib.Post.post
val assume_exists_eq : 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j Core.Flow.flow -> 'j Mopsa_analyzer.MopsaLib.Post.post
val assume_forall_ne : 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j Core.Flow.flow -> 'j Mopsa_analyzer.MopsaLib.Post.post

Evaluations entry point

Query handler

*****************

val ask : 'a -> 'b -> 'c -> 'd option

Pretty printer

******************

val print_expr : 'a -> 'b -> 'c -> 'd -> unit