package mopsa

  1. Overview
  2. Docs
MOPSA: A Modular and Open Platform for Static Analysis using Abstract Interpretation

Install 

dune-project
 Dependency

mopsa.lip6.fr Readme Changelog Edit opam file Versions (3)

Authors

  1. A
    Antoine Miné
  2. A
    Abdelraouf Ouadjaout
  3. M
    Matthieu Journault
  4. A
    Aymeric Fromherz
  5. R
    Raphaël Monat
  6. F
    Francesco Parolini
  7. M
    Marco Milanese
  8. J
    Jérôme Boillot

Maintainers

  1. A
    Antoine Miné <antoine.mine@lip6.fr>
  2. A
    Abdelraouf Ouadjaout <ouadjaout@gmail.com>
  3. R
    Raphaël Monat <raphael.monat@inria.fr>

Sources

mopsa-analyzer-v1.2.tar.gz
md5=37966e98ffeebcedc09bd6e9b2b81f69
sha512=40d4d826c25f680766c07eccbabdf5e8a4fa023016e8a164e4e4f6b3781c8484dc4df437055721dfd19b9db8fb7fe3b61236c4833186d346fc7204a68d01eaaa

doc/mopsa.mopsa_analyzer/Mopsa_analyzer/Languages/C/Memory/Smashing/Domain/index.html

Module Smashing.Domain

Domain header

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

val scalar : MopsaLib.route
val checks : 'a list

Smashes

***********

type styp =
  1. | Int of Lang.Ast.c_integer_type
  2. | Float of Lang.Ast.c_float_type
  3. | Ptr

Types of smashed elements

type smash = {
  1. base : Common.Base.base;
    (*

    smashed memory container

    *)
  2. styp : styp;
    (*

    type of the smashed elements

    *)
}

Smashes

val pp_styp : Format.formatter -> styp -> unit
val pp_smash : Format.formatter -> smash -> unit
val compare_styp : styp -> styp -> int
val compare_smash : smash -> smash -> int
val styp_of_typ : MopsaLib.typ -> styp
val typ_of_styp : styp -> MopsaLib.typ
val sizeof_styp : styp -> 'a Mopsa_analyzer.MopsaLib.Flow.flow -> Z.t
val rangeof_styp : styp -> 'a Mopsa_analyzer.MopsaLib.Flow.flow -> Z.t * Z.t
val mk_smash : Common.Base.base -> MopsaLib.typ -> smash

Abstract state

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

module STypeSet : sig ... end
module Init : sig ... end

Initialization state with shortcut states to avoid useless tests on `uninit`

module State : sig ... end
type t = State.t
include sig ... end
val id : t Mopsa_analyzer__Framework__Core__Id.id
val name : string
val debug : ('a, Format.formatter, unit, unit) format4 -> 'a

Smash variables

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

type MopsaLib.var_kind +=
  1. | V_c_smash of smash
val mk_smash_var : smash -> MopsaLib.var

Create a variable from a smash

val mk_smash_expr : smash -> ?typ:MopsaLib.typ option -> ?mode:Framework.Core.Ast.Var.mode option -> Mopsa_utils.Core.Location.range -> MopsaLib.expr

Functions for managing smash variables

Offset of the first uninitialized element

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

type MopsaLib.var_kind +=
  1. | V_c_uninit of Common.Base.base
val mk_uninit_var : Common.Base.base -> MopsaLib.var

Functions for managing uninit variables

Unification

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

Synthesis function of integer smashes

phi s r m f synthesizes the value of smash s when existing smashes in the same base exist

val unify_range : MopsaLib.range

Singleton unification range

val unify : ('s, State.t) MopsaLib.man -> 's Framework.Core.Context.ctx -> (t * 's) -> (t * 's) -> 's * 's

Lattice operators

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

val bottom : State.t
val top : State.t
val is_bottom : 'a -> bool
val subset : ('a, State.t) MopsaLib.man -> 'a Framework.Core.Context.ctx -> (t * 'a) -> (t * 'a) -> bool * 'a * 'a
val join : ('a, State.t) MopsaLib.man -> 'a Framework.Core.Context.ctx -> (t * 'a) -> (t * 'a) -> State.t * 'a * 'a
val meet : ('a, State.t) MopsaLib.man -> 'a Framework.Core.Context.ctx -> (t * 'a) -> (t * 'a) -> State.t * 'a * 'a
val widen : ('a, State.t) MopsaLib.man -> 'a Framework.Core.Context.ctx -> (t * 'a) -> (t * 'a) -> State.t * 'a * 'a * bool
val merge : 'a -> 'b -> 'c -> 'd

Pretty printer

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

val print_state : MopsaLib.printer -> t -> unit
val print_expr : 'a -> 'b -> 'c -> 'd -> unit

Initialization procedure

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

val init : 'a -> ('b, State.t) Framework.Core.Manager.man -> 'b Core.Flow.flow -> 'b Core.Post.post option

Utility functions

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

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) Mopsa_analyzer.MopsaLib.Cases.cases

Get the base and offset pointed by ptr

val is_interesting_base : Common.Base.base -> bool

Predicate defining interesting bases to smash

Fold an exec transfer function over a set of stypes

Fold an exec transfer function smashes of a base

Execute a transfer when a uninit variable exists

Environment transfer functions

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

𝕊⟦ add(base); ⟧

val exec_declare_variable : MopsaLib.var -> 'a -> 'b -> ('c, State.t) Framework.Core.Manager.man -> 'c Core.Flow.flow -> 'c Mopsa_analyzer.MopsaLib.Post.post

𝕊⟦ type v; ⟧

𝕊⟦ remove(base); ⟧

𝕊⟦ rename(base1,base2);

𝕊⟦ expand(base, bases); ⟧

𝕊⟦ fold(base, bases); ⟧

𝕊⟦ forget(lval) ⟧

𝕊⟦ ∀i ∈ lo,hi: forget( *(p + i) ) ⟧

Assignment transfer function

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

𝕊⟦ lval = rval; ⟧

Exec entry point

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

Abstract evaluations

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

Abstract evaluation of a dereference

Quantified tests transfer functions

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

𝕊⟦ ∀i ∈ lo,hi : *(p + i) ? e ⟧

𝕊⟦ ∀i ∈ lo,hi : *(p + i) == *(q + i) ⟧

val assume_exists_compare : 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l Core.Flow.flow -> 'l Mopsa_analyzer.MopsaLib.Post.post
val assume_exists_ne2 : 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n -> 'o -> 'p Core.Flow.flow -> 'p Mopsa_analyzer.MopsaLib.Post.post

Evaluations entry point

Query handler

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

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