package codex

You can search for identifiers within the package.

in-package search v0.2.0

The Codex library for building static analysers based on abstract interpretation

Install

dune-project

Dependency

codex.top Edit opam file Versions (1)

Authors

Maintainers

M

Matthieu Lemerre <matthieu.lemerre@cea.fr>

Sources

1.0-rc4.tar.gz

md5=bc7266a140c6886add673ede90e335d3

sha512=8da42c0ff2c1098c5f9cb2b5b43b306faf7ac93b8f5ae00c176918cee761f249ff45b29309f31a05bbcf6312304f86a0d5a000eb3f1094d3d3c2b9b4c7f5c386

doc/codex.domains/Domains/Overflow_checks/index.html

Module `Domains.Overflow_checks`Source

Adds checks for overflows around bitvector operation. Assumes no overflow occurs and optionaly raise alarms if overflows are possible.

Source

module Make
  (Sub : Sig.BASE_WITH_INTEGER) : 
  Sig.BASE_WITH_INTEGER
    with type boolean = Sub.boolean
     and type binary = Sub.binary
     and type integer = Sub.integer
     and type enum = Sub.enum

This functor adds overflow checks to bitvector operations. I.E. for a biadd with ~size=32 it first performs the addition on 33 bits, then checks if the result fits in 32 bits (Checking signedness according to the various flags). Similarly, it adds guards to bisub, bimul, and bisdiv (dividing min_int by -1 underflows). There are no overflow guards on shifts as of yet.