Frama-C:
Plug-ins:
Libraries:

Frama-C API - Make

Parameters

module Field : Field.S

Signature

module Linear : sig ... end
type ('n, 'm) filter
val create : state:('n Nat.succ, 'n Nat.succ) Linear.matrix -> input:('n Nat.succ, 'm Nat.succ) Linear.matrix -> center:'n Nat.succ Linear.vector -> measure:'m Nat.succ Linear.vector -> ('n Nat.succ, 'm Nat.succ) filter
val pretty : Stdlib.Format.formatter -> ('n, 'm) filter -> unit
type 'n invariant
val lower : 'n Finite.finite -> 'n invariant -> Field.scalar
val upper : 'n Finite.finite -> 'n invariant -> Field.scalar
val invariant : ('n, 'm) filter -> int -> 'n invariant option