Module Jasmin.Ct_checker_forwardSource

Sourceval is_ct_op1 : Expr.sop1 -> bool
Sourceval is_ct_op2 : Expr.sop2 -> bool
Sourceval is_ct_opN : Expr.opN -> bool
Sourceval is_ct_sopn : ('asm -> bool) -> 'asm Sopn.sopn -> bool
Sourcetype signature

Security type of a function

Sourceval pp_signature : (_, _) Prog.prog -> Format.formatter -> (Prog.funname * signature) -> unit

Human-readable form of a signature

Sourceval ty_prog : ('asm -> bool) -> infer:bool -> (_, 'asm) Prog.prog -> Jasmin.Prog.Name.t list -> (Prog.funname * signature) list * (Jasmin.Prog.L.t * (Format.formatter -> unit)) option

Type-check (for constant-time) a list of functions in the given program (defaults to all functions if the list is empty).

Returns the signature of all functions that have been successfully type-checked and an optional error message in case of failure (type-checking aborts after the first error).

When infer is false, checking of export functions fails unless they are correctly annotated.