package jasmin

You can search for identifiers within the package.

in-package search v0.2.0

Compiler for High-Assurance and High-Speed Cryptography

Install

dune-project

Dependency

github.com Readme Edit opam file Versions (18)

Authors

J

Jasmin authors and contributors

Maintainers

J

Jean-Christophe Léchenet <jean-christophe.lechenet@inria.fr>

Sources

jasmin-compiler-v2025.06.2.tar.bz2

sha256=aa0d21f532c1560a0939244cfd1c8414ba2b42c9d1403960f458500446cb1ebb

doc/jasmin.linter/Linter/Annotation/index.html

Module `Linter.Annotation`

type 'domain annotation =

| Empty
| Annotation of 'domain

Annotation type. Used to wrap domain with a minimal Empty value.

val pp : 
  (Format.formatter -> (Jasmin.Location.i_loc * 'domain) -> unit) ->
  Format.formatter ->
  (Jasmin.Location.i_loc * 'domain annotation) ->
  unit

Pretty printer wraper function for the annotation type following Jasmin.Printer.pp_iprog interface.

val merge : 
  'domain annotation ->
  'domain annotation ->
  ('domain -> 'domain -> 'domain) ->
  'domain annotation

Wrapper for domain merge functions. merge a Empty f

val included : 
  'domain annotation ->
  'domain annotation ->
  ('domain -> 'domain -> bool) ->
  bool

Inclusion test for annotations. included a b f return :

true if a is Empty
false if b is Empty and a is not Empty
true if inner domain a is included in inner domain b according to the function f otherwise

val bind : 
  'domain annotation ->
  ('domain -> 'domain annotation) ->
  'domain annotation

bind a f applies the function f to the value contained in the annotation a and return a new annotation. If a is Empty, it returns Empty.

val unwrap : 'domain annotation -> 'domain

Unwrapping function for annotation. It should only be used on annotations that are not Empty. It will otherwise raise an Invalid_argument exception.

val map : 'a annotation -> ('a -> 'b) -> 'b annotation

map a f applies the function f to the value contained in the annotation a. If a is Empty, it returns Empty.