package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

Parameters

module X : sig ... end

Signature

val narrow : t -> t -> t

Over-approximation of the intersection of abstract values, without considering (bitwise) reinterpretations. In particular, values with equivalent representations (e.g. -1 and 0xFF on 8 bits) may be considered different, leading to empty intersections. This may result in unsound results; the function narrow_reinterpret below should be preferred in general.

val narrow_reinterpret : t -> t -> t

Variant of the function above that bitwise-reinterprets values before performing the intersection (in order to get normal forms). This may lead to situations where the result is not included in the arguments, but this function should be preferred to narrow.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct