package libsail

  1. Overview
  2. Docs
package libsail
Legend:
Library
Module
Module type
Parameter
Class
Class type

The Config module specifies static configuration for compiling Sail into Jib. We have to provide a conversion function from Sail types into Jib types, as well as a function that optimizes ANF expressions (which can just be the identity function)

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 specialize_calls : bool

If false, function arguments must match the function type exactly. If true, they can be more specific.

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 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