package libsail

  1. Overview
  2. Docs
package libsail
Legend:
Library
Module
Module type
Parameter
Class
Class type
val convert_typ : ctx -> Ast.typ -> Jib.ctyp
val optimize_anf : ctx -> Ast.typ Anf.aexp -> Ast.typ Anf.aexp
val unroll_loops : int option

Unroll all for loops a bounded number of times. Used for SMT generation.

val make_call_precise : ctx -> Ast.id -> bool

A call is precise if the function arguments match the function type exactly. Leaving functions imprecise can allow later passes to specialize implementations.

val ignore_64 : bool

If false, will ensure that fixed size bitvectors are specifically less that 64-bits. If true this restriction will be ignored.

val struct_value : bool

If false we won't generate any V_struct values

val tuple_value : bool

If false we won't generate any V_tuple values

val use_real : bool

Allow real literals

val branch_coverage : Stdlib.out_channel option

Insert branch coverage operations

val track_throw : bool

If true track the location of the last exception thrown, useful for debugging C but we want to turn it off for SMT generation where we can't use strings