package goblint

  1. Overview
  2. Docs
package goblint
Legend:
Library
Module
Module type
Parameter
Class
Class type
include module type of struct include All end
include module type of Batteries with module Format := Batteries.Format
module Legacy = All.Legacy
module Array = All.Array
module Buffer = All.Buffer
module Bytes = All.Bytes
type bytes = Bytes.t
module Char = All.Char
module Complex = All.Complex
module Digest = All.Digest
module Either = All.Either
module Gc = All.Gc
module Genlex = All.Genlex
module Hashtbl = All.Hashtbl
module Int32 = All.Int32
module Int64 = All.Int64
module Lexing = All.Lexing
module List = All.List
module Map = All.Map
module Marshal = All.Marshal
module Nativeint = All.Nativeint
module Printexc = All.Printexc
module Printf = All.Printf
module Queue = All.Queue
module Random = All.Random
module Scanf = All.Scanf
module Set = All.Set
module Stack = All.Stack
module Stream = All.Stream
module String = All.String
module Sys = All.Sys
module Unix = All.Unix
module Big_int = All.Big_int
module Num = All.Num
module Bigarray = All.Bigarray
module Base64 = All.Base64
module BitSet = All.BitSet
module Bit_set = All.Bit_set
module Dllist = All.Dllist
module DynArray = All.DynArray
module Enum = All.Enum
module File = All.File
module Global = All.Global
module IO = All.IO
module LazyList = All.LazyList
module MultiPMap = All.MultiPMap
module Option = All.Option
module RefList = All.RefList
module Ref = All.Ref
module Cache = All.Cache
module CharParser = All.CharParser
module Deque = All.Deque
module Hashcons = All.Hashcons
module Heap = All.Heap
module FingerTree = All.FingerTree
module Logger = All.Logger
module MultiMap = All.MultiMap
module ParserCo = All.ParserCo
module Result = All.Result
module Return = All.Return
module Seq = All.Seq
module Substring = All.Substring
module Tuple = All.Tuple
module Tuple2 = All.Tuple2
module Tuple3 = All.Tuple3
module Tuple4 = All.Tuple4
module Tuple5 = All.Tuple5
module Vect = All.Vect
module ISet = All.ISet
module IMap = All.IMap
module Splay = All.Splay
module Uref = All.Uref
module UChar = All.UChar
module UTF8 = All.UTF8
module Text = All.Text
module Concurrent = All.Concurrent
module Interfaces = All.Interfaces
module Number = All.Number
module Float = All.Float
module Int = All.Int
module Bool = All.Bool
module Unit = All.Unit
module Filename = All.Filename
module Incubator = All.Incubator
include module type of Pervasives with type ('a, 'b) result := ('a, 'b) Pervasives.result and type 'a ref = 'a Pervasives.ref and type fpclass = Pervasives.fpclass and type in_channel = Pervasives.in_channel and type out_channel = Pervasives.out_channel and type open_flag = Pervasives.open_flag and type ('a, 'b, 'c, 'd, 'e, 'f) format6 = ('a, 'b, 'c, 'd, 'e, 'f) Pervasives.format6 and type ('a, 'b, 'c, 'd) format4 = ('a, 'b, 'c, 'd) Pervasives.format4 and type ('a, 'b, 'c) format = ('a, 'b, 'c) Pervasives.format
  • deprecated Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims
val raise : exn -> 'a
val raise_notrace : exn -> 'a
val invalid_arg : string -> 'a
val failwith : string -> 'a
exception Exit
val (=) : 'a -> 'a -> bool
val (<>) : 'a -> 'a -> bool
val (<) : 'a -> 'a -> bool
val (>) : 'a -> 'a -> bool
val (<=) : 'a -> 'a -> bool
val (>=) : 'a -> 'a -> bool
val compare : 'a -> 'a -> int
val min : 'a -> 'a -> 'a
val max : 'a -> 'a -> 'a
val (==) : 'a -> 'a -> bool
val (!=) : 'a -> 'a -> bool
val not : bool -> bool
val (&&) : bool -> bool -> bool
val (&) : bool -> bool -> bool
  • deprecated Use (&&) instead.
val (||) : bool -> bool -> bool
val or : bool -> bool -> bool
  • deprecated Use (||) instead.
val __LOC__ : string
val __FILE__ : string
val __LINE__ : int
val __MODULE__ : string
val __POS__ : string * int * int * int
val __LOC_OF__ : 'a -> string * 'a
val __LINE_OF__ : 'a -> int * 'a
val __POS_OF__ : 'a -> (string * int * int * int) * 'a
val (~-) : int -> int
val (~+) : int -> int
val succ : int -> int
val pred : int -> int
val (+) : int -> int -> int
val (-) : int -> int -> int
val (*) : int -> int -> int
val (/) : int -> int -> int
val (mod) : int -> int -> int
val abs : int -> int
val max_int : int
val min_int : int
val (land) : int -> int -> int
val (lor) : int -> int -> int
val (lxor) : int -> int -> int
val lnot : int -> int
val (lsl) : int -> int -> int
val (lsr) : int -> int -> int
val (asr) : int -> int -> int
val (~-.) : float -> float
val (~+.) : float -> float
val (+.) : float -> float -> float
val (-.) : float -> float -> float
val (*.) : float -> float -> float
val (/.) : float -> float -> float
val (**) : float -> float -> float
val sqrt : float -> float
val exp : float -> float
val log : float -> float
val log10 : float -> float
val expm1 : float -> float
val log1p : float -> float
val cos : float -> float
val sin : float -> float
val tan : float -> float
val acos : float -> float
val asin : float -> float
val atan : float -> float
val atan2 : float -> float -> float
val hypot : float -> float -> float
val cosh : float -> float
val sinh : float -> float
val tanh : float -> float
val ceil : float -> float
val floor : float -> float
val abs_float : float -> float
val copysign : float -> float -> float
val mod_float : float -> float -> float
val frexp : float -> float * int
val ldexp : float -> int -> float
val modf : float -> float * float
val float : int -> float
val float_of_int : int -> float
val truncate : float -> int
val int_of_float : float -> int
val infinity : float
val neg_infinity : float
val nan : float
val max_float : float
val min_float : float
val epsilon_float : float
type nonrec fpclass = Pervasives.fpclass =
  1. | FP_normal
  2. | FP_subnormal
  3. | FP_zero
  4. | FP_infinite
  5. | FP_nan
val classify_float : float -> fpclass
val (^) : string -> string -> string
val int_of_char : char -> int
val char_of_int : int -> char
val ignore : 'a -> unit
val string_of_bool : bool -> string
val bool_of_string : string -> bool
val bool_of_string_opt : string -> bool option
val string_of_int : int -> string
val int_of_string : string -> int
val int_of_string_opt : string -> int option
val string_of_float : float -> string
val float_of_string : string -> float
val float_of_string_opt : string -> float option
val fst : ('a * 'b) -> 'a
val snd : ('a * 'b) -> 'b
type nonrec in_channel = Pervasives.in_channel
type nonrec out_channel = Pervasives.out_channel
val print_char : char -> unit
val print_string : string -> unit
val print_bytes : bytes -> unit
val print_int : int -> unit
val print_float : float -> unit
val print_endline : string -> unit
val print_newline : unit -> unit
val prerr_char : char -> unit
val prerr_string : string -> unit
val prerr_bytes : bytes -> unit
val prerr_int : int -> unit
val prerr_float : float -> unit
val prerr_endline : string -> unit
val prerr_newline : unit -> unit
val read_line : unit -> string
val read_int : unit -> int
val read_int_opt : unit -> int option
val read_float : unit -> float
val read_float_opt : unit -> float option
type nonrec open_flag = Pervasives.open_flag =
  1. | Open_rdonly
  2. | Open_wronly
  3. | Open_append
  4. | Open_creat
  5. | Open_trunc
  6. | Open_excl
  7. | Open_binary
  8. | Open_text
  9. | Open_nonblock
val output_bytes : out_channel -> bytes -> unit
val seek_out : out_channel -> int -> unit
val pos_out : out_channel -> int
val out_channel_length : out_channel -> int
val set_binary_mode_out : out_channel -> bool -> unit
val really_input_string : in_channel -> int -> string
val seek_in : in_channel -> int -> unit
val pos_in : in_channel -> int
val in_channel_length : in_channel -> int
val set_binary_mode_in : in_channel -> bool -> unit
module LargeFile = All.LargeFile
type nonrec 'a ref = 'a Pervasives.ref = {
  1. mutable contents : 'a;
}
val ref : 'a -> 'a ref
val (!) : 'a ref -> 'a
val (:=) : 'a ref -> 'a -> unit
val incr : int ref -> unit
val decr : int ref -> unit
type ('a, 'b, 'c, 'd, 'e, 'f) format6 = ('a, 'b, 'c, 'd, 'e, 'f) Pervasives.format6
type ('a, 'b, 'c, 'd) format4 = ('a, 'b, 'c, 'd) Pervasives.format4
type ('a, 'b, 'c) format = ('a, 'b, 'c) Pervasives.format
val string_of_format : ('a, 'b, 'c, 'd, 'e, 'f) format6 -> string
val format_of_string : ('a, 'b, 'c, 'd, 'e, 'f) format6 -> ('a, 'b, 'c, 'd, 'e, 'f) format6
val (^^) : ('a, 'b, 'c, 'd, 'e, 'f) format6 -> ('f, 'b, 'c, 'e, 'g, 'h) format6 -> ('a, 'b, 'c, 'd, 'g, 'h) format6
val exit : int -> 'a
val at_exit : (unit -> unit) -> unit
val valid_float_lexem : string -> string
val do_at_exit : unit -> unit
include module type of struct include BatPervasives end
Additional functions.
  • author Xavier Leroy (Base module)
  • author Nicolas Cannasse
  • author David Teller
  • author Zheng Li

The initially opened module.

This module provides the basic operations over the built-in types (numbers, booleans, strings, exceptions, references, lists, arrays, input-output channels, ...)

This module is automatically opened at the beginning of each compilation. All components of this module can therefore be referred by their short name, without prefixing them by BatPervasives.

  • author Xavier Leroy (Base module)
  • author Nicolas Cannasse
  • author David Teller
  • author Zheng Li
val input_lines : Pervasives.in_channel -> string BatEnum.t

Returns an enumeration over lines of an input channel, as read by the input_line function.

val input_chars : Pervasives.in_channel -> char BatEnum.t

Returns an enumeration over characters of an input channel.

val input_list : Pervasives.in_channel -> string list

Returns the list of lines read from an input channel.

val input_all : Pervasives.in_channel -> string

Return the whole contents of an input channel as a single string.

val dump : 'a -> string

Attempt to convert a value to a string.

Works well for a lot of cases such as non-empty lists, algebraic datatype, and records.

However, since types are lost at compile-time, the representation might not match your type. (0, 1) will be printed as expected, but (1, 0) and 1 have the same representation and will get printed in the same way. The result of dump is unspecified and may change in future versions, so you should only use it for debugging and never have program behavior depend on the output.

Here is a list of some of the surprising corner cases of the current implementation:

  • (3, 0) is printed 3, (0.5, 0) is printed 0.5, etc.
  • None, false and are printed 0

dump may fail for ill-formed values, such as obtained from a faulty C binding or crazy uses of Obj.set_tag.

val print_any : 'b BatIO.output -> 'a -> unit

Attempt to print a value to an output.

Uses dump to convert the value to a string and prints that string to the output.

List operations

More list operations are provided in module List.

val (@) : 'a list -> 'a list -> 'a list

List concatenation.

Input/output

This section only contains the most common input/output operations. More operations may be found in modules BatIO and File.

val stdin : BatIO.input

Standard input, as per Unix/Windows conventions (by default, keyboard).

Use this input to read what the user is writing on the keyboard.

val stdout : unit BatIO.output

Standard output, as per Unix/Windows conventions (by default, console).

Use this output to display regular messages.

val stderr : unit BatIO.output

Standard error output, as per Unix/Windows conventions.

Use this output to display warnings and error messages.

val stdnull : unit BatIO.output

An output which discards everything written to it.

Use this output to ignore messages.

val flush_all : unit -> unit

Write all pending data to output channels, ignore all errors.

It is normally not necessary to call this function, as all pending data is written when an output channel is closed or when the program itself terminates, either normally or because of an uncaught exception. However, this function is useful for debugging, as it forces pending data to be written immediately.

Output functions on standard output
val print_bool : bool -> unit

Print a boolean on standard output.

val print_guess : 'a BatIO.output -> 'b -> unit

Attempt to print the representation of a runtime value on the standard output. See remarks for dump. This function is useful mostly for debugging. As a general rule, it should not be used in production code.

val print_all : BatIO.input -> unit

Print the contents of an input to the standard output.

Output functions on standard error
val prerr_bool : bool -> unit

Print a boolean to stderr.

val prerr_guess : 'a -> unit

Attempt to print the representation of a runtime value on the error output. See remarks for dump. This function is useful mostly for debugging.

val prerr_all : BatIO.input -> unit

Print the contents of an input to the error output.

General output functions
val output_file : filename:string -> text:string -> unit

creates a filename, write text into it and close it.

val open_out : ?mode:BatFile.open_out_flag list -> ?perm:BatFile.permission -> string -> unit BatIO.output

Open the named file for writing, and return a new output channel on that file. You will need to close the file once you have finished using it.

You may use optional argument mode to decide whether the output will overwrite the contents of the file (by default) or to add things at the end of the file, whether the file should be created if it does not exist yet (the default) or not, whether this operation should proceed if the file exists already (the default) or not, whether the file should be opened as text (the default) or as binary, and whether the file should be opened for non-blocking operations.

You may use optional argument perm to specify the permissions of the file, as per Unix conventions. By default, files are created with default permissions (which depend on your setup).

  • raises Sys_error

    if the file could not be opened.

val open_out_bin : string -> unit BatIO.output

Same as open_out, but the file is opened in binary mode, so that no translation takes place during writes. On operating systems that do not distinguish between text mode and binary mode, this function behaves like open_out without any mode or perm.

val open_out_gen : open_flag list -> int -> string -> unit BatIO.output

open_out_gen mode perm filename opens the named file for writing, as described above. The extra argument mode specifies the opening mode. The extra argument perm specifies the file permissions, in case the file must be created.

  • deprecated

    Use open_outinstead

val flush : unit BatIO.output -> unit

Flush the buffer associated with the given output, performing all pending writes on that channel. Interactive programs must be careful about flushing standard output and standard error at the right time.

val output_char : unit BatIO.output -> char -> unit

Write the character on the given output channel.

val output_string : unit BatIO.output -> string -> unit

Write the string on the given output channel.

val output : unit BatIO.output -> Bytes.t -> int -> int -> unit

output oc buf pos len writes len characters from byte sequence buf, starting at offset pos, to the given output channel oc.

  • raises Invalid_argument

    if pos and len do not designate a valid subsequence of buf.

val output_substring : unit BatIO.output -> string -> int -> int -> unit

output_substring oc buf pos len writes len characters from string buf, starting at offset pos, to the given output channel oc.

  • raises Invalid_argument

    if pos and len do not designate a valid substring of buf.

val output_byte : unit BatIO.output -> int -> unit

Write one 8-bit integer (as the single character with that code) on the given output channel. The given integer is taken modulo 256.

val output_binary_int : unit BatIO.output -> int -> unit

Write one integer in binary format (4 bytes, big-endian) on the given output channel. The given integer is taken modulo 232. The only reliable way to read it back is through the Pervasives.input_binary_int function. The format is compatible across all machines for a given version of OCaml.

val output_binary_float : unit BatIO.output -> float -> unit

Write one float in binary format (8 bytes, IEEE 754 double format) on the given output channel. The only reliable way to read it back is through the Pervasives.input_binary_float function. The format is compatible across all machines for a given version of OCaml.

val output_value : unit BatIO.output -> 'a -> unit

Write the representation of a structured value of any type to a channel. Circularities and sharing inside the value are detected and preserved. The object can be read back, by the function input_value. See the description of module Marshal for more information. output_value is equivalent to Marshal.output with an empty list of flags.

val close_out : unit BatIO.output -> unit

Close the given channel, flushing all buffered write operations. Output functions raise a Sys_error exception when they are applied to a closed output channel, except close_out and flush, which do nothing when applied to an already closed channel.

  • raises Sys_error

    if the operating system signals an error when flushing or closing.

val close_out_noerr : unit BatIO.output -> unit

Same as close_out, but ignore all errors.

General input functions
val input_file : ?bin:bool -> string -> string

returns the data of a given filename.

val open_in : ?mode:BatFile.open_in_flag list -> ?perm:BatFile.permission -> string -> BatIO.input

Open the named file for reading. You will need to close the file once you have finished using it.

You may use optional argument mode to decide whether the opening should fail if the file doesn't exist yet (by default) or whether the file should be created if it doesn't exist yet, whether the opening should fail if the file already exists or not (by default), whether the file should be read as binary (by default) or as text, and whether reading should be non-blocking.

You may use optional argument perm to specify the permissions of the file, should it be created, as per Unix conventions. By default, files are created with default permissions (which depend on your setup).

  • raises Sys_error

    if the file could not be opened.

val open_in_bin : string -> BatIO.input

Same as Pervasives.open_in, but the file is opened in binary mode, so that no translation takes place during reads. On operating systems that do not distinguish between text mode and binary mode, this function behaves like Pervasives.open_in.

val open_in_gen : open_flag list -> int -> string -> BatIO.input

open_in_gen mode perm filename opens the named file for reading, as described above. The extra arguments mode and perm specify the opening mode and file permissions. Pervasives.open_in and Pervasives.open_in_bin are special cases of this function.

  • deprecated

    Use open_ininstead

val input_char : BatIO.input -> char

Read one character from the given input channel.

  • raises End_of_file

    if there are no more characters to read.

val input_line : BatIO.input -> string

Read characters from the given input channel, until a newline character is encountered. Return the string of all characters read, without the newline character at the end.

  • raises End_of_file

    if the end of the file is reached at the beginning of line.

val input : BatIO.input -> Bytes.t -> int -> int -> int

input ic buf pos len reads up to len characters from the given channel ic, storing them in byte sequence buf, starting at character number pos. It returns the actual number of characters read, between 0 and len (inclusive). A return value of 0 means that the end of file was reached. A return value between 0 and len exclusive means that not all requested len characters were read, either because no more characters were available at that time, or because the implementation found it convenient to do a partial read; input must be called again to read the remaining characters, if desired. (See also Pervasives.really_input for reading exactly len characters.)

  • raises Invalid_argument

    if pos and len do not designate a valid subsequence of buf.

val really_input : BatIO.input -> Bytes.t -> int -> int -> unit

really_input ic buf pos len reads len characters from channel ic, storing them in byte sequence buf, starting at character number pos.

  • raises End_of_file

    if the end of file is reached before len characters have been read.

  • raises Invalid_argument

    if pos and len do not designate a valid subsequence of buf.

val input_byte : BatIO.input -> int

Same as Pervasives.input_char, but return the 8-bit integer representing the character.

val input_binary_int : BatIO.input -> int

Read an integer encoded in binary format (4 bytes, big-endian) from the given input channel. See Pervasives.output_binary_int.

  • raises End_of_file

    if an end of file was reached while reading the integer.

val input_binary_float : BatIO.input -> float

Read a float encoded in binary format (8 bytes, IEEE 754 double format) from the given input channel. See Pervasives.output_binary_float.

  • raises End_of_file

    if an end of file was reached while reading the float.

val input_value : BatIO.input -> 'a

Read the representation of a structured value, as produced by output_value, and return the corresponding value. This function is identical to Marshal.input; see the description of module Marshal for more information, in particular concerning the lack of type safety.

val close_in : BatIO.input -> unit

Close the given channel. Input functions raise a Sys_error exception when they are applied to a closed input channel, except close_in, which does nothing when applied to an already closed channel.

  • raises Sys_error

    if the operating system signals an error.

val close_in_noerr : BatIO.input -> unit

Same as close_in, but ignore all errors.

Fundamental functions and operators
val identity : 'a -> 'a

The identity function.

val undefined : ?message:string -> 'a -> 'b

The undefined function.

Evaluating undefined x always fails and raises an exception "Undefined". Optional argument message permits the customization of the error message.

val (@@) : ('a -> 'b) -> 'a -> 'b

Function application. f @@ x is equivalent to f x. However, it binds less tightly (between :: and =,<,>,etc) and is right-associative, which makes it useful for composing sequences of function calls without too many parentheses. It is similar to Haskell's $. Note that it replaces pre-2.0 **> and <|.

val (%) : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b

Function composition: the mathematical o operator. f % g is fun x -> f (g x). It is similar to Haskell's ..

Examples: the following are equivalent: f (g (h x)), f @@ g @@ h x, f % g % h @@ x.

val (|>) : 'a -> ('a -> 'b) -> 'b

The "pipe": function application. x |> f is equivalent to f x.

This operator is commonly used to write a function composition by order of evaluation (the order used in object-oriented programming) rather than by inverse order (the order typically used in functional programming).

For instance, g (f x) means "apply f to x, then apply g to the result." The corresponding notation in most object-oriented programming languages would be somewhere along the lines of x.f.g.h(), or "starting from x, apply f, then apply g." In OCaml, using the ( |> ) operator, this is written x |> f |> g |> h.

This operator may also be useful for composing sequences of function calls without too many parentheses.

val (%>) : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c

Piping function composition. f %> g is fun x -> g (f x). Whereas f % g applies g first and f second, f %> g applies f, then g. Note that it plays well with pipes, so for instance x |> f %> g %> h |> i %> j yields the expected result... but in such cases it's still recommended to use |> only. Note that it replaces pre-2.0 |-, which didn't integrate with pipes.

val (|?) : 'a option -> 'a -> 'a

Like BatOption.default, with the arguments reversed. None |? 10 returns 10, while Some "foo" |? "bar" returns "foo".

Note This operator does not short circuit like ( || ) and ( && ). Both arguments will be evaluated.

  • since 2.0
val flip : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c

Argument flipping.

flip f x y is f y x. Don't abuse this function, it may shorten considerably your code but it also has the nasty habit of making it harder to read.

val curry : (('a * 'b) -> 'c) -> 'a -> 'b -> 'c

Convert a function which accepts a pair of arguments into a function which accepts two arguments.

curry f is fun x y -> f (x,y)

val uncurry : ('a -> 'b -> 'c) -> ('a * 'b) -> 'c

Convert a function which accepts two arguments into a function which accepts a pair of arguments.

uncurry f is fun (x, y) -> f x y

val neg : ('a -> bool) -> 'a -> bool

neg p returns a new predicate that is the negation of the given predicate. That is, the new predicate returns false when the input predicate returns true and vice versa. This is for predicates with one argument.

neg p is fun x -> not (p x)

val neg2 : ('a -> 'b -> bool) -> 'a -> 'b -> bool

as neg but for predicates with two arguments

val const : 'a -> _ -> 'a

Ignore its second argument.

const x is the function which always returns x.

val unique : unit -> int

Returns an unique identifier every time it is called.

Note This is thread-safe.

val tap : ('a -> unit) -> 'a -> 'a

Allows application of a function in the middle of a pipe sequence without disturbing the sequence. x |> tap f evaluates to x, but has the side effect of f x. Useful for debugging.

val finally : (unit -> unit) -> ('a -> 'b) -> 'a -> 'b

finally fend f x calls f x and then fend() even if f x raised an exception.

val with_dispose : dispose:('a -> unit) -> ('a -> 'b) -> 'a -> 'b

with_dispose dispose f x invokes f on x, calling dispose x when f terminates (either with a return value or an exception).

val forever : ('a -> 'b) -> 'a -> unit

forever f x invokes f on x repeatedly (until an exception occurs).

val ignore_exceptions : ('a -> 'b) -> 'a -> unit

ignore_exceptions f x invokes f on x, ignoring both the returned value and the exceptions that may be raised.

val verify_arg : bool -> string -> unit

verify_arg condition message will raise Invalid_argument message if condition is false, otherwise it does nothing.

  • since 2.0
val args : unit -> string BatEnum.t

An enumeration of the arguments passed to this program through the command line.

args () is given by the elements of Sys.argv, minus the first element.

val exe : string

The name of the current executable.

exe is given by the first argument of Sys.argv

Enumerations

In OCaml Batteries Included, all data structures are enumerable, which means that they support a number of standard operations, transformations, etc. The general manner of enumerating the contents of a data structure is to invoke the enum function of your data structure.

For instance, you may use the foreach loop to apply a function f to all the consecutive elements of a string s. For this purpose, you may write either foreach (String.enum s) f or open String in foreach (enum s) f. Either possibility states that you are enumerating through a character string s. Should you prefer your enumeration to proceed from the end of the string to the beginning, you may replace String.enum with String.backwards. Therefore, either foreach (String.backwards s) f or open String in foreach (backwards s) f will apply f to all the consecutive elements of string s, from the last to the first.

Similarly, you may use List.enum instead of String.enum to visit the elements of a list in the usual order, or List.backwards instead of String.backwards to visit them in the opposite order, or Hashtbl.enum for hash tables, etc.

More operations on enumerations are defined in module BatEnum, including the necessary constructors to make your own structures enumerable.

The various kinds of loops are detailed further in this documentation.

val foreach : 'a BatEnum.t -> ('a -> unit) -> unit

Imperative loop on an enumeration.

foreach e f applies function f to each successive element of e. For instance, foreach (1 -- 10) print_int invokes function print_int on 1, 2, ..., 10, printing 12345678910.

Note This function is one of the many loops available on enumerations. Other commonly used loops are iter (same usage scenario as foreach, but with different notations), map (convert an enumeration to another enumeration) or fold (flatten an enumeration by applying an operation to each element).

General-purpose loops

opic loops

The following functions are the three main general-purpose loops available in OCaml. By opposition to the loops available in imperative languages, OCaml loops are regular functions, which may be passed, composed, currified, etc. In particular, each of these loops may be considered either as a manner of applying a function to a data structure or as transforming a function into another function which will act on a whole data structure.

For instance, if f is a function operating on one value, you may lift this function to operate on all values of an enumeration (and consequently on all values of any data structure of OCaml Batteries Included) by applying iter, map or fold to this function.

val iter : ('a -> unit) -> 'a BatEnum.t -> unit

Imperative loop on an enumeration. This loop is typically used to lift a function with an effect but no meaningful result and get it to work on enumerations.

If f is a function iter f is a function which behaves as f but acts upon enumerations rather than individual elements. As indicated in the type of iter, f must produce values of type unit (i.e. f has no meaningful result) the resulting function produces no meaningful result either.

In other words, iter f is a function which, when applied upon an enumeration e, calls f with each element of e in turn.

For instance, iter f (1 -- 10) invokes function f on 1, 2, ..., 10 and produces value ().

val map : ('a -> 'b) -> 'a BatEnum.t -> 'b BatEnum.t

Transformation loop on an enumeration, used to build an enumeration from another enumeration. This loop is typically used to transform an enumeration into another enumeration with the same number of elements, in the same order.

If f is a function, map f e is a function which behaves as f but acts upon enumerations rather than individual elements -- and builds a new enumeration from the results of each application.

In other words, map f is a function which, when applied upon an enumeration containing elements e0, e1, ..., produces enumeration f e0, f e1, ...

For instance, if odd is the function which returns true when applied to an odd number or false when applied to an even number, map odd (1 -- 10) produces enumeration true, false, true, ..., false.

Similarly, if square is the function fun x -> x * x, map square (1 -- 10) produces the enumeration of the square numbers of all numbers between 1 and 10.

val filter_map : ('a -> 'b option) -> 'a BatEnum.t -> 'b BatEnum.t

Similar to a map, except that you can skip over some items of the incoming enumeration by returning None instead of Some value. Think of it as a filter combined with a map.

val reduce : ('a -> 'a -> 'a) -> 'a BatEnum.t -> 'a

Transformation loop on an enumeration, used to build a single value from an enumeration.

If f is a function and e is an enumeration, reduce f e applies function f to the first two elements of e, then to the result of this expression and to the third element of e, then to the result of this new expression and to the fourth element of e...

In other words, reduce f e returns a0 if e contains only one element a0, otherwise f (... (f (f a0) a1) ...) aN where a0,a1..aN are the elements of e.

  • raises Not_found

    if e is empty.

    For instance, if add is the function fun x y -> x + y, reduce add is the function which computes the sum of the elements of an enumeration -- and doesn't work on empty enumerations. Therefore, reduce add (1 -- 10) produces result 55.

val fold : ('b -> 'a -> 'b) -> 'b -> 'a BatEnum.t -> 'b

Transformation loop on an enumeration, used to build a single value from an enumeration. This is the most powerful general-purpose loop and also the most complex.

If f is a function, fold f v e applies f v to the first element of e, then, calling acc_1 the result of this operation, applies f acc_1 to the second element of e, then, calling acc_2 the result of this operation, applies f acc_2 to the third element of e...

In other words, fold f v e returns v if e is empty, otherwise f (... (f (f v a0) a1) ...) aN where a0,a1..aN are the elements of e.

For instance, if add is the function fun x y -> x + y, fold add 0 is the function which computes the sum of the elements of an enumeration. Therefore, fold add 0 (1 -- 10) produces result 55.

val scanl : ('b -> 'a -> 'b) -> 'b -> 'a BatEnum.t -> 'b BatEnum.t

Functional loop on an enumeration, used to build an enumeration from both an enumeration and an initial value. This function may be seen as a variant of fold which returns not only the final result of fold but the enumeration of all the intermediate results of fold.

If f is a function, scanl f v e is applies f v to the first element of e, then, calling acc_1 the result of this operation, applies f acc_1 to the second element of e, then, calling acc_2 the result of this operation, applies f acc_2 to the third element of e...

For instance, if add is the function fun x y -> x + y, scanl add 0 is the function which computes the sum of the elements of an enumeration. Therefore, scanl add 0 (1 -- 10) produces result the enumeration with elements 0, 1, 3, 6, 10, 15, 21, 28, 36, 45, 55.

val (/@) : 'a BatEnum.t -> ('a -> 'b) -> 'b BatEnum.t
val (@/) : ('a -> 'b) -> 'a BatEnum.t -> 'b BatEnum.t

Mapping operators.

These operators have the same meaning as function map but are sometimes more readable than this function, when chaining several transformations in a row.

val (//@) : 'a BatEnum.t -> ('a -> 'b option) -> 'b BatEnum.t
val (@//) : ('a -> 'b option) -> 'a BatEnum.t -> 'b BatEnum.t

Map combined with filter. Same as filter_map.

Other operations on enumerations
val exists : ('a -> bool) -> 'a BatEnum.t -> bool

exists f e returns true if there is some x in e such that f x

val for_all : ('a -> bool) -> 'a BatEnum.t -> bool

for_all f e returns true if for every x in e, f x is true

val find : ('a -> bool) -> 'a BatEnum.t -> 'a

find f e returns the first element x of e such that f x returns true, consuming the enumeration up to and including the found element, or, raises Not_found if no such element exists in the enumeration, consuming the whole enumeration in the search.

Since find consumes a prefix of the enumeration, it can be used several times on the same enumeration to find the next element.

  • raises Not_found

    if no element in the whole enumeration satisfies the predicate

val peek : 'a BatEnum.t -> 'a option

peek e returns None if e is empty or Some x where x is the next element of e. The element is not removed from the enumeration.

val get : 'a BatEnum.t -> 'a option

get e returns None if e is empty or Some x where x is the next element of e, in which case the element is removed from the enumeration.

val push : 'a BatEnum.t -> 'a -> unit

push e x will add x at the beginning of e.

val junk : 'a BatEnum.t -> unit

junk e removes the first element from the enumeration, if any.

val filter : ('a -> bool) -> 'a BatEnum.t -> 'a BatEnum.t

filter f e returns an enumeration over all elements x of e such as f x returns true.

val (//) : 'a BatEnum.t -> ('a -> bool) -> 'a BatEnum.t

Filtering (pronounce this operator name "such that").

For instance, (1 -- 37) // odd is the enumeration of all odd numbers between 1 and 37.

val (--) : int -> int -> int BatEnum.t

Enumerate numbers.

5 -- 10 is the enumeration 5,6,7,8,9,10. 10 -- 5 is the empty enumeration

val (--^) : int -> int -> int BatEnum.t

Enumerate numbers, without the right endpoint

5 -- 10 is the enumeration 5,6,7,8,9.

val (--.) : (float * float) -> float -> float BatEnum.t

(a, step) --. b) creates a float enumeration from a to b with an increment of step between elements.

(5.0, 1.0) --. 10.0 is the enumeration 5.0,6.0,7.0,8.0,9.0,10.0. (10.0, -1.0) --. 5.0 is the enumeration 10.0,9.0,8.0,7.0,6.0,5.0. (10.0, 1.0) --. 1.0 is the empty enumeration.

val (---) : int -> int -> int BatEnum.t

As --, but accepts enumerations in reverse order.

5 --- 10 is the enumeration 5,6,7,8,9,10. 10 --- 5 is the enumeration 10,9,8,7,6,5.

val (--~) : char -> char -> char BatEnum.t

As ( -- ), but for characters.

val print : ?first:string -> ?last:string -> ?sep:string -> ('a BatInnerIO.output -> 'b -> unit) -> 'a BatInnerIO.output -> 'b BatEnum.t -> unit

Print and consume the contents of an enumeration.

Results
type ('a, 'e) result = ('a, 'e) BatInnerPervasives.result =
  1. | Ok of 'a
  2. | Error of 'e
    (*

    The result of a computation - either an Ok with the normal result or a Error with some value (often an exception) containing failure information

    *)

This type represents the outcome of a function which has the possibility of failure. Normal results of type 'a are marked with Ok, while failure values of type 'b are marked with Error.

This is intended to be a safer alternative to functions raising exceptions to signal failure. It is safer in that the possibility of failure has to be handled before the result of that computation can be used.

For more functions related to this type, see the BatResult module.

val ignore_ok : ('a, exn) result -> unit

ignore_ok (f x) ignores the result of f x if it's ok, but throws the exception contained if Error is returned.

val ok : ('a, exn) result -> 'a

f x |> ok unwraps the Ok result of f x and returns it, or throws the exception contained if Error is returned.

val wrap : ('a -> 'b) -> 'a -> ('b, exn) result

wrap f x wraps a function that would normally throw an exception on failure such that it now returns a result with either the Ok return value or the Error exception.

Thread-safety internals

Unless you are attempting to adapt Batteries Included to a new model of concurrency, you probably won't need this.

A lock used to synchronize internal operations.

By default, this is BatConcurrent.nolock. However, if you're using a version of Batteries compiled in threaded mode, this uses BatMutex. If you're attempting to use Batteries with another concurrency model, set the lock appropriately.

module Format = All.Format
val comp2 : ('a -> 'a -> 'b) -> ('c -> 'a) -> 'c -> 'c -> 'b
val compareBy : ?cmp:('a -> 'a -> int) -> ('b -> 'a) -> 'b -> 'b -> int
val flat_map : ('a -> 'b list) -> 'a list -> 'b list
val str_remove : string -> string -> string
val try_opt : ('a -> 'b) -> 'a -> 'b option
val split_time : unit -> int * int * int * int
val string_of_time : unit -> string
val localtime : unit -> string
include module type of struct include Cil end
val initCIL : unit -> unit

Call this function to perform some initialization. Call if after you have * set Cil.msvcMode.

val cilVersion : string

These are the CIL version numbers. A CIL version is a number of the form * M.m.r (major, minor and release)

val cilVersionMajor : int
val cilVersionMinor : int
val cilVersionRevision : int

This module defines the abstract syntax of CIL. It also provides utility * functions for traversing the CIL data structures, and pretty-printing * them. The parser for both the GCC and MSVC front-ends can be invoked as * Frontc.parse: string -> unit -> Cil.file. This function must be given * the name of a preprocessed C file and will return the top-level data * structure that describes a whole source file. By default the parsing and * elaboration into CIL is done as for GCC source. If you want to use MSVC * source you must set the Cil.msvcMode to true and must also invoke the * function Frontc.setMSVCMode: unit -> unit.

The Abstract Syntax of CIL

The top-level representation of a CIL source file (and the result of the * parsing and elaboration). Its main contents is the list of global * declarations and definitions. You can iterate over the globals in a * Cil.file using the following iterators: Cil.mapGlobals, * Cil.iterGlobals and Cil.foldGlobals. You can also use the * Cil.dummyFile when you need a Cil.file as a placeholder. For each * global item CIL stores the source location where it appears (using the * type Cil.location)

type file = Cil.file = {
  1. mutable fileName : string;
    (*

    The complete file name

    *)
  2. mutable globals : global list;
    (*

    List of globals as they will appear in the printed file

    *)
  3. mutable globinit : fundec option;
    (*

    An optional global initializer function. This is a function where * you can put stuff that must be executed before the program is * started. This function is conceptually at the end of the file, * although it is not part of the globals list. Use Cil.getGlobInit * to create/get one.

    *)
  4. mutable globinitcalled : bool;
    (*

    Whether the global initialization function is called in main. This * should always be false if there is no global initializer. When you * create a global initialization CIL will try to insert code in main * to call it. This will not happen if your file does not contain a * function called "main"

    *)
}

Top-level representation of a C source file

and comment = location * string

Globals. The main type for representing global declarations and * definitions. A list of these form a CIL file. The order of globals in the * file is generally important.

and global = Cil.global =
  1. | GType of typeinfo * location
    (*

    A typedef. All uses of type names (through the TNamed constructor) must be preceded in the file by a definition of the name. The string is the defined name and always not-empty.

    *)
  2. | GCompTag of compinfo * location
    (*

    Defines a struct/union tag with some fields. There must be one of these for each struct/union tag that you use (through the TComp constructor) since this is the only context in which the fields are printed. Consequently nested structure tag definitions must be broken into individual definitions with the innermost structure defined first.

    *)
  3. | GCompTagDecl of compinfo * location
    (*

    Declares a struct/union tag. Use as a forward declaration. This is * printed without the fields.

    *)
  4. | GEnumTag of enuminfo * location
    (*

    Declares an enumeration tag with some fields. There must be one of these for each enumeration tag that you use (through the TEnum constructor) since this is the only context in which the items are printed.

    *)
  5. | GEnumTagDecl of enuminfo * location
    (*

    Declares an enumeration tag. Use as a forward declaration. This is * printed without the items.

    *)
  6. | GVarDecl of varinfo * location
    (*

    A variable declaration (not a definition). If the variable has a function type then this is a prototype. There can be several declarations and at most one definition for a given variable. If both forms appear then they must share the same varinfo structure. A prototype shares the varinfo with the fundec of the definition. Either has storage Extern or there must be a definition in this file

    *)
  7. | GVar of varinfo * initinfo * location
    (*

    A variable definition. Can have an initializer. The initializer is * updateable so that you can change it without requiring to recreate * the list of globals. There can be at most one definition for a * variable in an entire program. Cannot have storage Extern or function * type. Note: the initializer field is kept for backwards compatibility, * but it is now also available directly in the varinfo.

    *)
  8. | GFun of fundec * location
    (*

    A function definition.

    *)
  9. | GAsm of string * location
    (*

    Global asm statement. These ones can contain only a template

    *)
  10. | GPragma of attribute * location
    (*

    Pragmas at top level. Use the same syntax as attributes

    *)
  11. | GText of string
    (*

    Some text (printed verbatim) at top level. E.g., this way you can put comments in the output.

    *)

A global declaration or definition

Types. A C type is represented in CIL using the type Cil.typ. * Among types we differentiate the integral types (with different kinds * denoting the sign and precision), floating point types, enumeration types, * array and pointer types, and function types. Every type is associated with * a list of attributes, which are always kept in sorted order. Use * Cil.addAttribute and Cil.addAttributes to construct list of * attributes. If you want to inspect a type, you should use * Cil.unrollType or Cil.unrollTypeDeep to see through the uses of * named types.

CIL is configured at build-time with the sizes and alignments of the * underlying compiler (GCC or MSVC). CIL contains functions that can compute * the size of a type (in bits) Cil.bitsSizeOf, the alignment of a type * (in bytes) Cil.alignOf_int, and can convert an offset into a start and * width (both in bits) using the function Cil.bitsOffset. At the moment * these functions do not take into account the packed attributes and * pragmas.

and typ = Cil.typ =
  1. | TVoid of attributes
    (*

    Void type. Also predefined as Cil.voidType

    *)
  2. | TInt of ikind * attributes
    (*

    An integer type. The kind specifies the sign and width. Several * useful variants are predefined as Cil.intType, Cil.uintType, * Cil.longType, Cil.charType.

    *)
  3. | TFloat of fkind * attributes
    (*

    A floating-point type. The kind specifies the precision. You can * also use the predefined constant Cil.doubleType.

    *)
  4. | TPtr of typ * attributes
    (*

    Pointer type. Several useful variants are predefined as * Cil.charPtrType, Cil.charConstPtrType (pointer to a * constant character), Cil.voidPtrType, * Cil.intPtrType

    *)
  5. | TArray of typ * exp option * attributes
    (*

    Array type. It indicates the base type and the array length.

    *)
  6. | TFun of typ * (string * typ * attributes) list option * bool * attributes
    (*

    Function type. Indicates the type of the result, the name, type * and name attributes of the formal arguments (None if no * arguments were specified, as in a function whose definition or * prototype we have not seen; Some [] means void). Use * Cil.argsToList to obtain a list of arguments. The boolean * indicates if it is a variable-argument function. If this is the * type of a varinfo for which we have a function declaration then * the information for the formals must match that in the * function's sformals. Use Cil.setFormals, or * Cil.setFunctionType, or Cil.makeFormalVar for this * purpose.

    *)
  7. | TNamed of typeinfo * attributes
    (*

    The use of a named type. Each such type name must be preceded * in the file by a GType global. This is printed as just the * type name. The actual referred type is not printed here and is * carried only to simplify processing. To see through a sequence * of named type references, use Cil.unrollType or * Cil.unrollTypeDeep. The attributes are in addition to those * given when the type name was defined.

    *)
  8. | TComp of compinfo * attributes
    (*

    The most delicate issue for C types is that recursion that is possible by * using structures and pointers. To address this issue we have a more * complex representation for structured types (struct and union). Each such * type is represented using the Cil.compinfo type. For each composite * type the Cil.compinfo structure must be declared at top level using * GCompTag and all references to it must share the same copy of the * structure. The attributes given are those pertaining to this use of the * type and are in addition to the attributes that were given at the * definition of the type and which are stored in the Cil.compinfo.

    *)
  9. | TEnum of enuminfo * attributes
    (*

    A reference to an enumeration type. All such references must share the enuminfo among them and with a GEnumTag global that precedes all uses. The attributes refer to this use of the enumeration and are in addition to the attributes of the enumeration itself, which are stored inside the enuminfo

    *)
  10. | TBuiltin_va_list of attributes
    (*

    This is the same as the gcc's type with the same name

    *)

There are a number of functions for querying the kind of a type. These are Cil.isIntegralType, Cil.isArithmeticType, Cil.isPointerType, Cil.isScalarType, Cil.isFunctionType, Cil.isArrayType.

There are two easy ways to scan a type. First, you can use the Cil.existsType to return a boolean answer about a type. This function is controlled by a user-provided function that is queried for each type that is used to construct the current type. The function can specify whether to terminate the scan with a boolean result or to continue the scan for the nested types.

The other method for scanning types is provided by the visitor interface (see Cil.cilVisitor).

If you want to compare types (or to use them as hash-values) then you should use instead type signatures (represented as Cil.typsig). These contain the same information as types but canonicalized such that simple Ocaml structural equality will tell whether two types are equal. Use Cil.typeSig to compute the signature of a type. If you want to ignore certain type attributes then use Cil.typeSigWithAttrs.

and ikind = Cil.ikind =
  1. | IChar
    (*

    char

    *)
  2. | ISChar
    (*

    signed char

    *)
  3. | IUChar
    (*

    unsigned char

    *)
  4. | IBool
    (*

    _Bool (C99)

    *)
  5. | IInt
    (*

    int

    *)
  6. | IUInt
    (*

    unsigned int

    *)
  7. | IShort
    (*

    short

    *)
  8. | IUShort
    (*

    unsigned short

    *)
  9. | ILong
    (*

    long

    *)
  10. | IULong
    (*

    unsigned long

    *)
  11. | ILongLong
    (*

    long long (or _int64 on Microsoft Visual C)

    *)
  12. | IULongLong
    (*

    unsigned long long (or unsigned _int64 on Microsoft Visual C)

    *)
  13. | IInt128
    (*

    __int128

    *)
  14. | IUInt128
    (*

    unsigned __int128

    *)

Various kinds of integers

and fkind = Cil.fkind =
  1. | FFloat
    (*

    float

    *)
  2. | FDouble
    (*

    double

    *)
  3. | FLongDouble
    (*

    long double

    *)
  4. | FComplexFloat
    (*

    float _Complex

    *)
  5. | FComplexDouble
    (*

    double _Complex

    *)
  6. | FComplexLongDouble
    (*

    long double _Complex

    *)

Various kinds of floating-point numbers

Attributes.

and attribute = Cil.attribute =
  1. | Attr of string * attrparam list
    (*

    An attribute has a name and some optional parameters. The name should not * start or end with underscore. When CIL parses attribute names it will * strip leading and ending underscores (to ensure that the multitude of GCC * attributes such as const, __const and __const__ all mean the same thing.)

    *)
and attributes = attribute list

Attributes are lists sorted by the attribute name. Use the functions * Cil.addAttribute and Cil.addAttributes to insert attributes in an * attribute list and maintain the sortedness.

and attrparam = Cil.attrparam =
  1. | AInt of int
    (*

    An integer constant

    *)
  2. | AStr of string
    (*

    A string constant

    *)
  3. | ACons of string * attrparam list
    (*

    Constructed attributes. These are printed foo(a1,a2,...,an). The list of parameters can be empty and in that case the parentheses are not printed.

    *)
  4. | ASizeOf of typ
    (*

    A way to talk about types

    *)
  5. | ASizeOfE of attrparam
  6. | ASizeOfS of typsig
    (*

    Replacement for ASizeOf in type signatures. Only used for attributes inside typsigs.

    *)
  7. | AAlignOf of typ
  8. | AAlignOfE of attrparam
  9. | AAlignOfS of typsig
  10. | AUnOp of unop * attrparam
  11. | ABinOp of binop * attrparam * attrparam
  12. | ADot of attrparam * string
    (*

    a.foo *

    *)
  13. | AStar of attrparam
    (*

    * a

    *)
  14. | AAddrOf of attrparam
    (*

    & a *

    *)
  15. | AIndex of attrparam * attrparam
    (*

    a1a2

    *)
  16. | AQuestion of attrparam * attrparam * attrparam
    (*

    a1 ? a2 : a3 *

    *)

The type of parameters of attributes

Structures. The Cil.compinfo describes the definition of a * structure or union type. Each such Cil.compinfo must be defined at the * top-level using the GCompTag constructor and must be shared by all * references to this type (using either the TComp type constructor or from * the definition of the fields.

If all you need is to scan the definition of each * composite type once, you can do that by scanning all top-level GCompTag.

* Constructing a Cil.compinfo can be tricky since it must contain fields * that might refer to the host Cil.compinfo and furthermore the type of * the field might need to refer to the Cil.compinfo for recursive types. * Use the Cil.mkCompInfo function to create a Cil.compinfo. You can * easily fetch the Cil.fieldinfo for a given field in a structure with * Cil.getCompField.

and compinfo = Cil.compinfo = {
  1. mutable cstruct : bool;
    (*

    True if struct, False if union

    *)
  2. mutable cname : string;
    (*

    The name. Always non-empty. Use Cil.compFullName to get the full * name of a comp (along with the struct or union)

    *)
  3. mutable ckey : int;
    (*

    A unique integer. This is assigned by Cil.mkCompInfo using a * global variable in the Cil module. Thus two identical structs in two * different files might have different keys. Use Cil.copyCompInfo to * copy structures so that a new key is assigned.

    *)
  4. mutable cfields : fieldinfo list;
    (*

    Information about the fields. Notice that each fieldinfo has a * pointer back to the host compinfo. This means that you should not * share fieldinfo's between two compinfo's

    *)
  5. mutable cattr : attributes;
    (*

    The attributes that are defined at the same time as the composite * type. These attributes can be supplemented individually at each * reference to this compinfo using the TComp type constructor.

    *)
  6. mutable cdefined : bool;
    (*

    This boolean flag can be used to distinguish between structures that have not been defined and those that have been defined but have no fields (such things are allowed in gcc).

    *)
  7. mutable creferenced : bool;
    (*

    True if used. Initially set to false.

    *)
}

The definition of a structure or union type. Use Cil.mkCompInfo to * make one and use Cil.copyCompInfo to copy one (this ensures that a new * key is assigned and that the fields have the right pointers to parents.).

Structure fields. The Cil.fieldinfo structure is used to describe * a structure or union field. Fields, just like variables, can have * attributes associated with the field itself or associated with the type of * the field (stored along with the type of the field).

and fieldinfo = Cil.fieldinfo = {
  1. mutable fcomp : compinfo;
    (*

    The host structure that contains this field. There can be only one * compinfo that contains the field.

    *)
  2. mutable fname : string;
    (*

    The name of the field. Might be the value of Cil.missingFieldName * in which case it must be a bitfield and is not printed and it does not * participate in initialization

    *)
  3. mutable ftype : typ;
    (*

    The type

    *)
  4. mutable fbitfield : int option;
    (*

    If a bitfield then ftype should be an integer type and the width of * the bitfield must be 0 or a positive integer smaller or equal to the * width of the integer type. A field of width 0 is used in C to control * the alignment of fields.

    *)
  5. mutable fattr : attributes;
    (*

    The attributes for this field (not for its type)

    *)
  6. mutable floc : location;
    (*

    The location where this field is defined

    *)
}

Information about a struct/union field

Enumerations. Information about an enumeration. This is shared by all * references to an enumeration. Make sure you have a GEnumTag for each of * of these.

and enuminfo = Cil.enuminfo = {
  1. mutable ename : string;
    (*

    The name. Always non-empty.

    *)
  2. mutable eitems : (string * exp * location) list;
    (*

    Items with names and values. This list should be non-empty. The item * values must be compile-time constants.

    *)
  3. mutable eattr : attributes;
    (*

    The attributes that are defined at the same time as the enumeration * type. These attributes can be supplemented individually at each * reference to this enuminfo using the TEnum type constructor.

    *)
  4. mutable ereferenced : bool;
    (*

    True if used. Initially set to false

    *)
  5. mutable ekind : ikind;
    (*

    The integer kind used to represent this enum. Per ANSI-C, this * should always be IInt, but gcc allows other integer kinds

    *)
}

Information about an enumeration

and typeinfo = Cil.typeinfo = {
  1. mutable tname : string;
    (*

    The name. Can be empty only in a GType when introducing a composite * or enumeration tag. If empty cannot be referred to from the file

    *)
  2. mutable ttype : typ;
    (*

    The actual type. This includes the attributes that were present in * the typedef

    *)
  3. mutable treferenced : bool;
    (*

    True if used. Initially set to false

    *)
}

Information about a defined type

Variables. Each local or global variable is represented by a unique Cil.varinfo structure. A global Cil.varinfo can be introduced with the GVarDecl or GVar or GFun globals. A local varinfo can be introduced as part of a function definition Cil.fundec.

All references to a given global or local variable must refer to the same copy of the varinfo. Each varinfo has a globally unique identifier that can be used to index maps and hashtables (the name can also be used for this purpose, except for locals from different functions). This identifier is constructor using a global counter.

It is very important that you construct varinfo structures using only one of the following functions:

A varinfo is also used in a function type to denote the list of formals.

and varinfo = Cil.varinfo = {
  1. mutable vname : string;
    (*

    The name of the variable. Cannot be empty. It is primarily your * responsibility to ensure the uniqueness of a variable name. For local * variables Cil.makeTempVar helps you ensure that the name is unique.

    *)
  2. mutable vtype : typ;
    (*

    The declared type of the variable.

    *)
  3. mutable vattr : attributes;
    (*

    A list of attributes associated with the variable.

    *)
  4. mutable vstorage : storage;
    (*

    The storage-class

    *)
  5. mutable vglob : bool;
    (*

    True if this is a global variable

    *)
  6. mutable vinline : bool;
    (*

    Whether this varinfo is for an inline function.

    *)
  7. mutable vdecl : location;
    (*

    Location of variable declaration.

    *)
  8. vinit : initinfo;
    (*

    Optional initializer. Only used for static and global variables. * Initializers for other types of local variables are turned into * assignments. Not mutable because the init field in initinfo is mutable * already.

    *)
  9. mutable vid : int;
    (*

    A unique integer identifier. This field will be * set for you if you use one of the Cil.makeFormalVar, * Cil.makeLocalVar, Cil.makeTempVar, Cil.makeGlobalVar, or * Cil.copyVarinfo.

    *)
  10. mutable vaddrof : bool;
    (*

    True if the address of this variable is taken. CIL will set these * flags when it parses C, but you should make sure to set the flag * whenever your transformation create AddrOf expression.

    *)
  11. mutable vreferenced : bool;
    (*

    True if this variable is ever referenced. This is computed by * Rmtmps.removeUnusedTemps. It is safe to just initialize this to False

    *)
  12. mutable vdescr : Pretty.doc;
    (*

    For most temporary variables, a description of what the var holds. * (e.g. for temporaries used for function call results, this string * is a representation of the function call.)

    *)
  13. mutable vdescrpure : bool;
    (*

    Indicates whether the vdescr above is a pure expression or call. * Printing a non-pure vdescr more than once may yield incorrect * results.

    *)
  14. mutable vhasdeclinstruction : bool;
    (*

    Indicates whether a VarDecl instruction was generated for this variable. * Only applies to local variables. * Currently, this is relevant for when to print the declaration. If this is * true, it might be incorrect to print the declaration at the beginning of the * function, rather than where the VarDecl instruction is. This was introduced to * handle VLAs.

    *)
}

Information about a variable.

and storage = Cil.storage =
  1. | NoStorage
    (*

    The default storage. Nothing is printed

    *)
  2. | Static
  3. | Register
  4. | Extern

Storage-class information

Expressions. The CIL expression language contains only the side-effect free expressions of C. They are represented as the type Cil.exp. There are several interesting aspects of CIL expressions:

Integer and floating point constants can carry their textual representation. This way the integer 15 can be printed as 0xF if that is how it occurred in the source.

CIL uses 64 bits to represent the integer constants and also stores the width of the integer type. Care must be taken to ensure that the constant is representable with the given width. Use the functions Cil.kinteger, Cil.kinteger64 and Cil.integer to construct constant expressions. CIL predefines the constants Cil.zero, Cil.one and Cil.mone (for -1).

Use the functions Cil.isConstant and Cil.isInteger to test if an expression is a constant and a constant integer respectively.

CIL keeps the type of all unary and binary expressions. You can think of that type qualifying the operator. Furthermore there are different operators for arithmetic and comparisons on arithmetic types and on pointers.

Another unusual aspect of CIL is that the implicit conversion between an expression of array type and one of pointer type is made explicit, using the StartOf expression constructor (which is not printed). If you apply the AddrOf}constructor to an lvalue of type T then you will be getting an expression of type TPtr(T).

You can find the type of an expression with Cil.typeOf.

You can perform constant folding on expressions using the function Cil.constFold.

and exp = Cil.exp =
  1. | Const of constant
    (*

    Constant

    *)
  2. | Lval of lval
    (*

    Lvalue

    *)
  3. | SizeOf of typ
    (*

    sizeof(<type>). Has unsigned int type (ISO 6.5.3.4). This is not * turned into a constant because some transformations might want to * change types

    *)
  4. | Real of exp
    (*

    __real__(<expression>)

    *)
  5. | Imag of exp
    (*

    __imag__(<expression>)

    *)
  6. | SizeOfE of exp
    (*

    sizeof(<expression>)

    *)
  7. | SizeOfStr of string
    (*

    sizeof(string_literal). We separate this case out because this is the * only instance in which a string literal should not be treated as * having type pointer to character.

    *)
  8. | AlignOf of typ
    (*

    This corresponds to the GCC __alignof_. Has unsigned int type

    *)
  9. | AlignOfE of exp
  10. | UnOp of unop * exp * typ
    (*

    Unary operation. Includes the type of the result.

    *)
  11. | BinOp of binop * exp * exp * typ
    (*

    Binary operation. Includes the type of the result. The arithmetic * conversions are made explicit for the arguments.

    *)
  12. | Question of exp * exp * exp * typ
    (*

    (a ? b : c) operation. Includes the type of the result

    *)
  13. | CastE of typ * exp
    (*

    Use Cil.mkCast to make casts.

    *)
  14. | AddrOf of lval
    (*

    Always use Cil.mkAddrOf to construct one of these. Apply to an * lvalue of type T yields an expression of type TPtr(T). Use * Cil.mkAddrOrStartOf to make one of these if you are not sure which * one to use.

    *)
  15. | AddrOfLabel of stmt ref
    (*

    The address of a label, using GCC's label-as-value extension. If you * want to use these, you must set Cil.useComputedGoto.

    *)
  16. | StartOf of lval
    (*

    Conversion from an array to a pointer to the beginning of the array. * Given an lval of type TArray(T) produces an expression of type * TPtr(T). Use Cil.mkAddrOrStartOf to make one of these if you are * not sure which one to use. In C this operation is implicit, the * StartOf operator is not printed. We have it in CIL because it makes * the typing rules simpler.

    *)

Expressions (Side-effect free)

Constants.

and constant = Cil.constant =
  1. | CInt64 of int64 * ikind * string option
    (*

    Integer constant. Give the ikind (see ISO9899 6.1.3.2) and the * textual representation, if available. (This allows us to print a * constant as, for example, 0xF instead of 15.) Use Cil.integer or * Cil.kinteger to create these. Watch out for integers that cannot be * represented on 64 bits. OCAML does not give Overflow exceptions.

    *)
  2. | CStr of string
    (*

    String constant. The escape characters inside the string have been * already interpreted. This constant has pointer to character type! The * only case when you would like a string literal to have an array type * is when it is an argument to sizeof. In that case you should use * SizeOfStr.

    *)
  3. | CWStr of int64 list
    (*

    Wide character string constant. Note that the local interpretation * of such a literal depends on Cil.wcharType and Cil.wcharKind. * Such a constant has type pointer to Cil.wcharType. The * escape characters in the string have not been "interpreted" in * the sense that L"A\xabcd" remains "A\xabcd" rather than being * represented as the wide character list with two elements: 65 and * 43981. That "interpretation" depends on the underlying wide * character type.

    *)
  4. | CChr of char
    (*

    Character constant. This has type int, so use charConstToInt * to read the value in case sign-extension is needed.

    *)
  5. | CReal of float * fkind * string option
    (*

    Floating point constant. Give the fkind (see ISO 6.4.4.2) and also * the textual representation, if available.

    *)
  6. | CEnum of exp * string * enuminfo
    (*

    An enumeration constant with the given value, name, from the given * enuminfo. This is used only if Cil.lowerConstants is true * (default). Use Cil.constFoldVisitor to replace these with integer * constants.

    *)

Literal constants

and unop = Cil.unop =
  1. | Neg
    (*

    Unary minus

    *)
  2. | BNot
    (*

    Bitwise complement (~)

    *)
  3. | LNot
    (*

    Logical Not (!)

    *)

Unary operators

and binop = Cil.binop =
  1. | PlusA
    (*

    arithmetic +

    *)
  2. | PlusPI
    (*

    pointer + integer

    *)
  3. | IndexPI
    (*

    pointer + integer but only when * it arises from an expression * e[i] when e is a pointer and * not an array. This is semantically * the same as PlusPI but CCured uses * this as a hint that the integer is * probably positive.

    *)
  4. | MinusA
    (*

    arithmetic -

    *)
  5. | MinusPI
    (*

    pointer - integer

    *)
  6. | MinusPP
    (*

    pointer - pointer

    *)
  7. | Mult
    (*

    *

    *)
  8. | Div
    (*

    /

    *)
  9. | Mod
    (*

    %

    *)
  10. | Shiftlt
    (*

    shift left

    *)
  11. | Shiftrt
    (*

    shift right

    *)
  12. | Lt
    (*

    < (arithmetic comparison)

    *)
  13. | Gt
    (*

    > (arithmetic comparison)

    *)
  14. | Le
    (*

    <= (arithmetic comparison)

    *)
  15. | Ge
    (*

    > (arithmetic comparison)

    *)
  16. | Eq
    (*

    == (arithmetic comparison)

    *)
  17. | Ne
    (*

    != (arithmetic comparison)

    *)
  18. | BAnd
    (*

    bitwise and

    *)
  19. | BXor
    (*

    exclusive-or

    *)
  20. | BOr
    (*

    inclusive-or

    *)
  21. | LAnd
    (*

    logical and. Unlike other * expressions this one does not * always evaluate both operands. If * you want to use these, you must * set Cil.useLogicalOperators.

    *)
  22. | LOr
    (*

    logical or. Unlike other * expressions this one does not * always evaluate both operands. If * you want to use these, you must * set Cil.useLogicalOperators.

    *)

Binary operations

and lval = lhost * offset

Lvalues. Lvalues are the sublanguage of expressions that can appear at the left of an assignment or as operand to the address-of operator. In C the syntax for lvalues is not always a good indication of the meaning of the lvalue. For example the C value

a[0][1][2]

might involve 1, 2 or 3 memory reads when used in an expression context, depending on the declared type of the variable a. If a has type int [4][4][4] then we have one memory read from somewhere inside the area that stores the array a. On the other hand if a has type int *** then the expression really means * ( * ( * (a + 0) + 1) + 2), in which case it is clear that it involves three separate memory operations.

An lvalue denotes the contents of a range of memory addresses. This range is denoted as a host object along with an offset within the object. The host object can be of two kinds: a local or global variable, or an object whose address is in a pointer expression. We distinguish the two cases so that we can tell quickly whether we are accessing some component of a variable directly or we are accessing a memory location through a pointer. To make it easy to tell what an lvalue means CIL represents lvalues as a host object and an offset (see Cil.lval). The host object (represented as Cil.lhost) can be a local or global variable or can be the object pointed-to by a pointer expression. The offset (represented as Cil.offset) is a sequence of field or array index designators.

Both the typing rules and the meaning of an lvalue is very precisely specified in CIL.

The following are a few useful function for operating on lvalues:

The following equivalences hold 

Mem(AddrOf(Mem a, aoff)), off   = Mem a, aoff + off
Mem(AddrOf(Var v, aoff)), off   = Var v, aoff + off
AddrOf (Mem a, NoOffset)        = a
and lhost = Cil.lhost =
  1. | Var of varinfo
    (*

    The host is a variable.

    *)
  2. | Mem of exp
    (*

    The host is an object of type T when the expression has pointer * TPtr(T).

    *)

The host part of an Cil.lval.

and offset = Cil.offset =
  1. | NoOffset
    (*

    No offset. Can be applied to any lvalue and does * not change either the starting address or the type. * This is used when the lval consists of just a host * or as a terminator in a list of other kinds of * offsets.

    *)
  2. | Field of fieldinfo * offset
    (*

    A field offset. Can be applied only to an lvalue * that denotes a structure or a union that contains * the mentioned field. This advances the offset to the * beginning of the mentioned field and changes the * type to the type of the mentioned field.

    *)
  3. | Index of exp * offset
    (*

    An array index offset. Can be applied only to an * lvalue that denotes an array. This advances the * starting address of the lval to the beginning of the * mentioned array element and changes the denoted type * to be the type of the array element

    *)

The offset part of an Cil.lval. Each offset can be applied to certain * kinds of lvalues and its effect is that it advances the starting address * of the lvalue and changes the denoted type, essentially focusing to some * smaller lvalue that is contained in the original one.

and init = Cil.init =
  1. | SingleInit of exp
    (*

    A single initializer

    *)
  2. | CompoundInit of typ * (offset * init) list
    (*

    Used only for initializers of structures, unions and arrays. The * offsets are all of the form Field(f, NoOffset) or Index(i, * NoOffset) and specify the field or the index being initialized. For * structures all fields must have an initializer (except the unnamed * bitfields), in the proper order. This is necessary since the offsets * are not printed. For unions there must be exactly one initializer. If * the initializer is not for the first field then a field designator is * printed, so you better be on GCC since MSVC does not understand this. * For arrays, however, we allow you to give only a prefix of the * initializers. You can scan an initializer list with * Cil.foldLeftCompound.

    *)

Initializers. A special kind of expressions are those that can appear * as initializers for global variables (initialization of local variables is * turned into assignments). The initializers are represented as type * Cil.init. You can create initializers with Cil.makeZeroInit and you * can conveniently scan compound initializers them with * Cil.foldLeftCompound. * * Initializers for global variables.

and initinfo = Cil.initinfo = {
  1. mutable init : init option;
}

We want to be able to update an initializer in a variable, so we define it * as a mutable field

and fundec = Cil.fundec = {
  1. mutable svar : varinfo;
    (*

    Holds the name and type as a variable, so we can refer to it * easily from the program. All references to this function either * in a function call or in a prototype must point to the same * varinfo.

    *)
  2. mutable sformals : varinfo list;
    (*

    Formals. These must be in the same order and with the same * information as the formal information in the type of the function. * Use Cil.setFormals or * Cil.setFunctionType or Cil.makeFormalVar * to set these formals and ensure that they * are reflected in the function type. Do not make copies of these * because the body refers to them.

    *)
  3. mutable slocals : varinfo list;
    (*

    Locals. Does NOT include the sformals. Do not make copies of * these because the body refers to them.

    *)
  4. mutable smaxid : int;
    (*

    Max local id. Starts at 0. Used for * creating the names of new temporary * variables. Updated by * Cil.makeLocalVar and * Cil.makeTempVar. You can also use * Cil.setMaxId to set it after you * have added the formals and locals.

    *)
  5. mutable sbody : block;
    (*

    The function body.

    *)
  6. mutable smaxstmtid : int option;
    (*

    max id of a (reachable) statement * in this function, if we have * computed it. range = 0 ... * (smaxstmtid-1). This is computed by * Cil.computeCFGInfo.

    *)
  7. mutable sallstmts : stmt list;
    (*

    After you call Cil.computeCFGInfo * this field is set to contain all * statements in the function

    *)
}

Function definitions. A function definition is always introduced with a GFun constructor at the top level. All the information about the function is stored into a Cil.fundec. Some of the information (e.g. its name, type, storage, attributes) is stored as a Cil.varinfo that is a field of the fundec. To refer to the function from the expression language you must use the varinfo.

The function definition contains, in addition to the body, a list of all the local variables and separately a list of the formals. Both kind of variables can be referred to in the body of the function. The formals must also be shared with the formals that appear in the function type. For that reason, to manipulate formals you should use the provided functions Cil.makeFormalVar and Cil.setFormals and Cil.makeFormalVar.

and block = Cil.block = {
  1. mutable battrs : attributes;
    (*

    Attributes for the block

    *)
  2. mutable bstmts : stmt list;
    (*

    The statements comprising the block

    *)
}

A block is a sequence of statements with the control falling through from one element to the next

and stmt = Cil.stmt = {
  1. mutable labels : label list;
    (*

    Whether the statement starts with some labels, case statements or * default statements.

    *)
  2. mutable skind : stmtkind;
    (*

    The kind of statement

    *)
  3. mutable sid : int;
    (*

    A number (>= 0) that is unique in a function. Filled in only after * the CFG is computed.

    *)
  4. mutable succs : stmt list;
    (*

    The successor statements. They can always be computed from the skind * and the context in which this statement appears. Filled in only after * the CFG is computed.

    *)
  5. mutable preds : stmt list;
    (*

    The inverse of the succs function.

    *)
  6. mutable fallthrough : stmt option;
    (*

    The fallthrough successor statement computed from the context of this statement in Cil.computeCFGInto. Useful for the syntactic successor of Goto and Loop.

    *)
}

Statements. CIL statements are the structural elements that make the CFG. They are represented using the type Cil.stmt. Every statement has a (possibly empty) list of labels. The Cil.stmtkind field of a statement indicates what kind of statement it is.

Use Cil.mkStmt to make a statement and the fill-in the fields.

CIL also comes with support for control-flow graphs. The sid field in stmt can be used to give unique numbers to statements, and the succs and preds fields can be used to maintain a list of successors and predecessors for every statement. The CFG information is not computed by default. Instead you must explicitly use the functions Cil.prepareCFG and Cil.computeCFGInfo to do it.

and label = Cil.label =
  1. | Label of string * location * bool
    (*

    A real label. If the bool is "true", the label is from the * input source program. If the bool is "false", the label was * created by CIL or some other transformation

    *)
  2. | Case of exp * location
    (*

    A case statement. This expression * is lowered into a constant if * Cil.lowerConstants is set to * true.

    *)
  3. | CaseRange of exp * exp * location
    (*

    A case statement corresponding to a * range of values (GCC's extension). * Both expressions are lowered into * constants if Cil.lowerConstants is * set to true. If you want to use * these, you must set * Cil.useCaseRange.

    *)
  4. | Default of location
    (*

    A default statement

    *)

Labels

and stmtkind = Cil.stmtkind =
  1. | Instr of instr list
    (*

    A group of instructions that do not contain control flow. Control * implicitly falls through.

    *)
  2. | Return of exp option * location
    (*

    The return statement. This is a leaf in the CFG.

    *)
  3. | Goto of stmt ref * location
    (*

    A goto statement. Appears from actual goto's in the code or from * goto's that have been inserted during elaboration. The reference * points to the statement that is the target of the Goto. This means that * you have to update the reference whenever you replace the target * statement. The target statement MUST have at least a label.

    *)
  4. | ComputedGoto of exp * location
    (*

    A computed goto using GCC's label-as-value extension. If you want to use * these, you must set Cil.useComputedGoto.

    *)
  5. | Break of location
    (*

    A break to the end of the nearest enclosing Loop or Switch

    *)
  6. | Continue of location
    (*

    A continue to the start of the nearest enclosing Loop

    *)
  7. | If of exp * block * block * location
    (*

    A conditional. Two successors, the "then" and the "else" branches. * Both branches fall-through to the successor of the If statement.

    *)
  8. | Switch of exp * block * stmt list * location
    (*

    A switch statement. The statements that implement the cases can be * reached through the provided list. For each such target you can find * among its labels what cases it implements. The statements that * implement the cases are somewhere within the provided block.

    *)
  9. | Loop of block * location * stmt option * stmt option
    (*

    A while(1) loop. The termination test is implemented in the body of * a loop using a Break statement. If prepareCFG has been called, * the first stmt option will point to the stmt containing the continue * label for this loop and the second will point to the stmt containing * the break label for this loop.

    *)
  10. | Block of block
    (*

    Just a block of statements. Use it as a way to keep some block * attributes local

    *)
  11. | TryFinally of block * block * location
    (*

    On MSVC we support structured exception handling. This is what you * might expect. Control can get into the finally block either from the * end of the body block, or if an exception is thrown.

    *)
  12. | TryExcept of block * instr list * exp * block * location
    (*

    On MSVC we support structured exception handling. The try/except * statement is a bit tricky: __try { blk } __except (e) { handler }

    The argument to __except must be an expression. However, we keep a list of instructions AND an expression in case you need to make function calls. We'll print those as a comma expression. The control can get to the __except expression only if an exception is thrown. After that, depending on the value of the expression the control goes to the handler, propagates the exception, or retries the exception !!!

    *)

The various kinds of control-flow statements statements

Instructions. An instruction Cil.instr is a statement that has no local (intraprocedural) control flow. It can be either an assignment, function call, or an inline assembly instruction.

and instr = Cil.instr =
  1. | Set of lval * exp * location
    (*

    An assignment. The type of the expression is guaranteed to be the same * with that of the lvalue

    *)
  2. | VarDecl of varinfo * location
    (*

    "Instruction" in the location where a varinfo was declared. * All varinfos for which such a VarDecl instruction exists have * vhasdeclinstruction set to true. * The motivation for the addition of this instruction was to support VLAs * for which declerations can not be pulled up like CIL used to do.

    *)
  3. | Call of lval option * exp * exp list * location
    (*

    A function call with the (optional) result placed in an lval. It is * possible that the returned type of the function is not identical to * that of the lvalue. In that case a cast is printed. The type of the * actual arguments are identical to those of the declared formals. The * number of arguments is the same as that of the declared formals, except * for vararg functions. This construct is also used to encode a call to * "__builtin_va_arg". In this case the second argument (which should be a * type T) is encoded SizeOf(T)

    *)
  4. | Asm of attributes * string list * (string option * string * lval) list * (string option * string * exp) list * string list * location
    (*

    There are for storing inline assembly. They follow the GCC * specification:

      asm [volatile] ("...template..." "..template.."
                  : "c1" (o1), "c2" (o2), ..., "cN" (oN)
                  : "d1" (i1), "d2" (i2), ..., "dM" (iM)
                  : "r1", "r2", ..., "nL" );

    where the parts are

    • volatile (optional): when present, the assembler instruction cannot be removed, moved, or otherwise optimized
    • template: a sequence of strings, with %0, %1, %2, etc. in the string to refer to the input and output expressions. I think they're numbered consecutively, but the docs don't specify. Each string is printed on a separate line. This is the only part that is present for MSVC inline assembly.
    • "ci" (oi): pairs of constraint-string and output-lval; the constraint specifies that the register used must have some property, like being a floating-point register; the constraint string for outputs also has "=" to indicate it is written, or "+" to indicate it is both read and written; 'oi' is the name of a C lvalue (probably a variable name) to be used as the output destination
    • "dj" (ij): pairs of constraint and input expression; the constraint is similar to the "ci"s. the 'ij' is an arbitrary C expression to be loaded into the corresponding register
    • "rk": registers to be regarded as "clobbered" by the instruction; "memory" may be specified for arbitrary memory effects

    an example (from gcc manual):

      asm volatile ("movc3 %0,%1,%2"
                : /* no outputs */
                : "g" (from), "g" (to), "g" (count)
                : "r0", "r1", "r2", "r3", "r4", "r5");

    Starting with gcc 3.1, the operands may have names:

      asm volatile ("movc3 %[in0],%1,%2"
                : /* no outputs */
                : [in0] "g" (from), "g" (to), "g" (count)
                : "r0", "r1", "r2", "r3", "r4", "r5");
    *)

Instructions.

and location = Cil.location = {
  1. line : int;
    (*

    The line number. -1 means "do not know"

    *)
  2. file : string;
    (*

    The name of the source file

    *)
  3. byte : int;
    (*

    The byte position in the source file

    *)
  4. column : int;
    (*

    The column number

    *)
}

Describes a location in a source file.

and typsig = Cil.typsig =
  1. | TSArray of typsig * int64 option * attribute list
  2. | TSPtr of typsig * attribute list
  3. | TSComp of bool * string * attribute list
  4. | TSFun of typsig * typsig list option * bool * attribute list
  5. | TSEnum of string * attribute list
  6. | TSBase of typ

Type signatures. Two types are identical iff they have identical * signatures. These contain the same information as types but canonicalized. * For example, two function types that are identical except for the name of * the formal arguments are given the same signature. Also, TNamed * constructors are unrolled.

Lowering Options

val lowerConstants : bool ref

Do lower constants (default true)

val insertImplicitCasts : bool ref

Do insert implicit casts (default true)

val compareLoc : location -> location -> int

Comparison function for locations. ** Compares first by filename, then line, then byte

Values for manipulating globals

val emptyFunction : string -> fundec

Make an empty function

val setFormals : fundec -> varinfo list -> unit

Update the formals of a fundec and make sure that the function type has the same information. Will copy the name as well into the type.

val setFunctionType : fundec -> typ -> unit

Set the types of arguments and results as given by the function type * passed as the second argument. Will not copy the names from the function * type to the formals

val setFunctionTypeMakeFormals : fundec -> typ -> unit

Set the type of the function and make formal arguments for them

val setMaxId : fundec -> unit

Update the smaxid after you have populated with locals and formals * (unless you constructed those using Cil.makeLocalVar or * Cil.makeTempVar.

val dummyFunDec : fundec

A dummy function declaration handy when you need one as a placeholder. It * contains inside a dummy varinfo.

val dummyFile : file

A dummy file

val saveBinaryFile : file -> string -> unit

Write a Cil.file in binary form to the filesystem. The file can be * read back in later using Cil.loadBinaryFile, possibly saving parsing * time. The second argument is the name of the file that should be * created.

val saveBinaryFileChannel : file -> out_channel -> unit

Write a Cil.file in binary form to the filesystem. The file can be * read back in later using Cil.loadBinaryFile, possibly saving parsing * time. Does not close the channel.

val loadBinaryFile : string -> file

Read a Cil.file in binary form from the filesystem. The first * argument is the name of a file previously created by * Cil.saveBinaryFile. Because this also reads some global state, * this should be called before any other CIL code is parsed or generated.

val getGlobInit : ?main_name:string -> file -> fundec

Get the global initializer and create one if it does not already exist. * When it creates a global initializer it attempts to place a call to it in * the main function named by the optional argument (default "main")

val iterGlobals : file -> (global -> unit) -> unit

Iterate over all globals, including the global initializer

val foldGlobals : file -> ('a -> global -> 'a) -> 'a -> 'a

Fold over all globals, including the global initializer

val mapGlobals : file -> (global -> global) -> unit

Map over all globals, including the global initializer and change things in place

val findOrCreateFunc : file -> string -> typ -> varinfo

Find a function or function prototype with the given name in the file. * If it does not exist, create a prototype with the given type, and return * the new varinfo. This is useful when you need to call a libc function * whose prototype may or may not already exist in the file. * * Because the new prototype is added to the start of the file, you shouldn't * refer to any struct or union types in the function type.

val new_sid : unit -> int
val prepareCFG : fundec -> unit

Prepare a function for CFG information computation by * Cil.computeCFGInfo. This function converts all Break, Switch, * Default and Continue Cil.stmtkinds and Cil.labels into Ifs * and Gotos, giving the function body a very CFG-like character. This * function modifies its argument in place.

val computeCFGInfo : fundec -> bool -> unit

Compute the CFG information for all statements in a fundec and return a * list of the statements. The input fundec cannot have Break, Switch, * Default, or Continue Cil.stmtkinds or Cil.labels. Use * Cil.prepareCFG to transform them away. The second argument should * be true if you wish a global statement number, false if you wish a * local (per-function) statement numbering. The list of statements is set * in the sallstmts field of a fundec. * * NOTE: unless you want the simpler control-flow graph provided by * prepareCFG, or you need the function's smaxstmtid and sallstmt fields * filled in, we recommend you use Cfg.computeFileCFG instead of this * function to compute control-flow information. * Cfg.computeFileCFG is newer and will handle switch, break, and * continue correctly.

val copyFunction : fundec -> string -> fundec

Create a deep copy of a function. There should be no sharing between the * copy and the original function

val pushGlobal : global -> types:global list ref -> variables:global list ref -> unit

CIL keeps the types at the beginning of the file and the variables at the * end of the file. This function will take a global and add it to the * corresponding stack. Its operation is actually more complicated because if * the global declares a type that contains references to variables (e.g. in * sizeof in an array length) then it will also add declarations for the * variables to the types stack

val invalidStmt : stmt

An empty statement. Used in pretty printing

val builtinFunctions : (string, typ * typ list * bool) Hashtbl.t

A list of the built-in functions for the current compiler (GCC or * MSVC, depending on !msvcMode). Maps the name to the * result and argument types, and whether it is vararg. * Initialized by Cil.initCIL * * This map replaces gccBuiltins and msvcBuiltins in previous * versions of CIL.

val builtinLoc : location

This is used as the location of the prototypes of builtin functions.

Values for manipulating initializers

val makeZeroInit : typ -> init

Make a initializer for zero-ing a data type

val foldLeftCompound : implicit:bool -> doinit:(offset -> init -> typ -> 'a -> 'a) -> ct:typ -> initl:(offset * init) list -> acc:'a -> 'a

Fold over the list of initializers in a Compound (not also the nested * ones). doinit is called on every present initializer, even if it is of * compound type. The parameters of doinit are: the offset in the compound * (this is Field(f,NoOffset) or Index(i,NoOffset)), the initializer * value, expected type of the initializer value, accumulator. In the case of * arrays there might be missing zero-initializers at the end of the list. * These are scanned only if implicit is true. This is much like * List.fold_left except we also pass the type of the initializer.

* This is a good way to use it to scan even nested initializers :

  let rec myInit (lv: lval) (i: init) (acc: 'a) : 'a =
      match i with
        SingleInit e -> ... do something with lv and e and acc ...
      | CompoundInit (ct, initl) ->
         foldLeftCompound ~implicit:false
             ~doinit:(fun off' i' t' acc ->
                        myInit (addOffsetLval lv off') i' acc)
             ~ct:ct
             ~initl:initl
             ~acc:acc

Values for manipulating types

val voidType : typ

void

val isVoidType : typ -> bool

is the given type "void"?

val isVoidPtrType : typ -> bool

is the given type "void *"?

val typeOfRealAndImagComponents : typ -> typ

for numerical __complex types return type of corresponding real part and imaginary parts

val getComplexFkind : fkind -> fkind

for an fkind, return the corresponding complex fkind

val intType : typ

int

val uintType : typ

unsigned int

val longType : typ

long

val ulongType : typ

unsigned long

val charType : typ

char

val charPtrType : typ

char *

val wcharKind : ikind ref

wchar_t (depends on architecture) and is set when you call * Cil.initCIL.

val wcharType : typ ref
val charConstPtrType : typ

char const *

val voidPtrType : typ

void *

val intPtrType : typ

int *

val uintPtrType : typ

unsigned int *

val doubleType : typ

double

val upointType : typ ref

An unsigned integer type that fits pointers. Depends on Cil.msvcMode * and is set when you call Cil.initCIL.

val ptrdiffType : typ ref

An signed integer type that fits pointer difference. Depends on * Cil.msvcMode and is set when you call Cil.initCIL.

val typeOfSizeOf : typ ref

An unsigned integer type that is the type of sizeof. Depends on * Cil.msvcMode and is set when you call Cil.initCIL.

val kindOfSizeOf : ikind ref

The integer kind of Cil.typeOfSizeOf. * Set when you call Cil.initCIL.

val isSigned : ikind -> bool

Returns true if and only if the given integer type is signed.

val mkCompInfo : bool -> string -> (compinfo -> (string * typ * int option * attributes * location) list) -> attributes -> compinfo

Creates a a (potentially recursive) composite type. The arguments are: * (1) a boolean indicating whether it is a struct or a union, (2) the name * (always non-empty), (3) a function that when given a representation of the * structure type constructs the type of the fields recursive type (the first * argument is only useful when some fields need to refer to the type of the * structure itself), and (4) a list of attributes to be associated with the * composite type. The resulting compinfo has the field "cdefined" only if * the list of fields is non-empty.

val copyCompInfo : compinfo -> string -> compinfo

Makes a shallow copy of a Cil.compinfo changing the name and the key.

val missingFieldName : string

This is a constant used as the name of an unnamed bitfield. These fields do not participate in initialization and their name is not printed.

val compFullName : compinfo -> string

Get the full name of a comp

val isCompleteType : typ -> bool

Returns true if this is a complete type. This means that sizeof(t) makes sense. Incomplete types are not yet defined structures and empty arrays.

val unrollType : typ -> typ

Unroll a type until it exposes a non * TNamed. Will collect all attributes appearing in TNamed!!!

val unrollTypeDeep : typ -> typ

Unroll all the TNamed in a type (even under type constructors such as * TPtr, TFun or TArray. Does not unroll the types of fields in TComp * types. Will collect all attributes

val separateStorageModifiers : attribute list -> attribute list * attribute list

Separate out the storage-modifier name attributes

val isIntegralType : typ -> bool

True if the argument is an integral type (i.e. integer or enum)

val isArithmeticType : typ -> bool

True if the argument is an arithmetic type (i.e. integer, enum or floating point

val isPointerType : typ -> bool

True if the argument is a pointer type

val isScalarType : typ -> bool

True if the argument is a scalar type

val isFunctionType : typ -> bool

True if the argument is a function type

val argsToList : (string * typ * attributes) list option -> (string * typ * attributes) list

Obtain the argument list ( if None)

val isArrayType : typ -> bool

True if the argument is an array type

exception LenOfArray

Raised when Cil.lenOfArray fails either because the length is None * or because it is a non-constant expression

val lenOfArray : exp option -> int

Call to compute the array length as present in the array type, to an * integer. Raises Cil.LenOfArray if not able to compute the length, such * as when there is no length or the length is not a constant.

val getCompField : compinfo -> string -> fieldinfo

Return a named fieldinfo in compinfo, or raise Not_found

type existsAction = Cil.existsAction =
  1. | ExistsTrue
    (*

    We have found it

    *)
  2. | ExistsFalse
    (*

    Stop processing this branch

    *)
  3. | ExistsMaybe
    (*

    This node is not what we are * looking for but maybe its * successors are

    *)

A datatype to be used in conjunction with existsType

val existsType : (typ -> existsAction) -> typ -> bool

Scans a type by applying the function on all elements. When the function returns ExistsTrue, the scan stops with true. When the function returns ExistsFalse then the current branch is not scanned anymore. Care is taken to apply the function only once on each composite type, thus avoiding circularity. When the function returns ExistsMaybe then the types that construct the current type are scanned (e.g. the base type for TPtr and TArray, the type of fields for a TComp, etc).

val splitFunctionType : typ -> typ * (string * typ * attributes) list option * bool * attributes

Given a function type split it into return type, * arguments, is_vararg and attributes. An error is raised if the type is not * a function type

val splitFunctionTypeVI : varinfo -> typ * (string * typ * attributes) list option * bool * attributes

Same as Cil.splitFunctionType but takes a varinfo. Prints a nicer * error message if the varinfo is not for a function

Type signatures

Type signatures. Two types are identical iff they have identical * signatures. These contain the same information as types but canonicalized. * For example, two function types that are identical except for the name of * the formal arguments are given the same signature. Also, TNamed * constructors are unrolled.

val d_typsig : unit -> typsig -> Pretty.doc

Print a type signature

val typeSig : typ -> typsig

Compute a type signature

val typeSigWithAttrs : ?ignoreSign:bool -> (attributes -> attributes) -> typ -> typsig

Like Cil.typeSig but customize the incorporation of attributes. Use ~ignoreSign:true to convert all signed integer types to unsigned, so that signed and unsigned will compare the same.

val setTypeSigAttrs : attributes -> typsig -> typsig

Replace the attributes of a signature (only at top level)

val typeSigAttrs : typsig -> attributes

Get the top-level attributes of a signature

Lvalues

val makeVarinfo : bool -> string -> ?init:init -> typ -> varinfo

Make a varinfo. Use this (rarely) to make a raw varinfo. Use other * functions to make locals (Cil.makeLocalVar or Cil.makeFormalVar or * Cil.makeTempVar) and globals (Cil.makeGlobalVar). Note that this * function will assign a new identifier. The first argument specifies * whether the varinfo is for a global.

val makeFormalVar : fundec -> ?where:string -> string -> typ -> varinfo

Make a formal variable for a function. Insert it in both the sformals and the type of the function. You can optionally specify where to insert this one. If where = "^" then it is inserted first. If where = "$" then it is inserted last. Otherwise where must be the name of a formal after which to insert this. By default it is inserted at the end.

val makeLocalVar : fundec -> ?insert:bool -> string -> ?init:init -> typ -> varinfo

Make a local variable and add it to a function's slocals (only if insert = true, which is the default). Make sure you know what you are doing if you set insert=false.

val makeTempVar : fundec -> ?insert:bool -> ?name:string -> ?descr:Pretty.doc -> ?descrpure:bool -> typ -> varinfo

Make a temporary variable and add it to a function's slocals. CIL will ensure that the name of the new variable is unique in this function, and will generate this name by appending a number to the specified string ("__cil_tmp" by default).

The variable will be added to the function's slocals unless you explicitly set insert=false. (Make sure you know what you are doing if you set insert=false.)

Optionally, you can give the variable a description of its contents that will be printed by descriptiveCilPrinter.

val makeGlobalVar : string -> typ -> varinfo

Make a global variable. Your responsibility to make sure that the name is unique

val copyVarinfo : varinfo -> string -> varinfo

Make a shallow copy of a varinfo and assign a new identifier

val newVID : unit -> int

Generate a new variable ID. This will be different than any variable ID * that is generated by Cil.makeLocalVar and friends

val addOffsetLval : offset -> lval -> lval

Add an offset at the end of an lvalue. Make sure the type of the lvalue * and the offset are compatible.

val addOffset : offset -> offset -> offset

addOffset o1 o2 adds o1 to the end of o2.

val removeOffsetLval : lval -> lval * offset

Remove ONE offset from the end of an lvalue. Returns the lvalue with the * trimmed offset and the final offset. If the final offset is NoOffset * then the original lval did not have an offset.

val removeOffset : offset -> offset * offset

Remove ONE offset from the end of an offset sequence. Returns the * trimmed offset and the final offset. If the final offset is NoOffset * then the original lval did not have an offset.

val typeOfLval : lval -> typ

Compute the type of an lvalue

val typeOffset : typ -> offset -> typ

Compute the type of an offset from a base type

Values for manipulating expressions

val zero : exp

0

val one : exp

1

val mone : exp

-1

val kintegerCilint : ikind -> Cilint.cilint -> exp

Construct an integer of a given kind, from a cilint. If needed it * will truncate the integer to be within the representable range for * the given kind.

val kinteger64 : ikind -> int64 -> exp

Construct an integer of a given kind, using OCaml's int64 type. If needed * it will truncate the integer to be within the representable range for the * given kind.

val kinteger : ikind -> int -> exp

Construct an integer of a given kind. Converts the integer to int64 and * then uses kinteger64. This might truncate the value if you use a kind * that cannot represent the given integer. This can only happen for one of * the Char or Short kinds

val integer : int -> exp

Construct an integer of kind IInt. On targets where C's 'int' is 16-bits, the integer may get truncated.

val getInteger : exp -> Cilint.cilint option

If the given expression is an integer constant or a CastE'd integer constant, return that constant's value. Otherwise return None.

val i64_to_int : int64 -> int

Convert a 64-bit int to an OCaml int, or raise an exception if that can't be done.

val cilint_to_int : Cilint.cilint -> int

Convert a cilint int to an OCaml int, or raise an exception if that can't be done.

val isConstant : exp -> bool

True if the expression is a compile-time constant

val isConstantOffset : offset -> bool

True if the given offset contains only field nanmes or constant indices.

val isZero : exp -> bool

True if the given expression is a (possibly cast'ed) integer or character constant with value zero

val isNullPtrConstant : exp -> bool

True if the given expression is a null-pointer constant. As per 6.3.2.3 subsection 3

val charConstToInt : char -> constant

Given the character c in a (CChr c), sign-extend it to 32 bits. (This is the official way of interpreting character constants, according to ISO C 6.4.4.4.10, which says that character constants are chars cast to ints) Returns CInt64(sign-extended c, IInt, None)

val constFold : bool -> exp -> exp

Do constant folding on an expression. If the first argument is true then will also compute compiler-dependent expressions such as sizeof. See also Cil.constFoldVisitor, which will run constFold on all expressions in a given AST node.

val constFoldBinOp : bool -> binop -> exp -> exp -> typ -> exp

Do constant folding on a binary operation. The bulk of the work done by constFold is done here. If the first argument is true then will also compute compiler-dependent expressions such as sizeof

val increm : exp -> int -> exp

Increment an expression. Can be arithmetic or pointer type

val var : varinfo -> lval

Makes an lvalue out of a given variable

val mkAddrOf : lval -> exp

Make an AddrOf. Given an lvalue of type T will give back an expression of type ptr(T). It optimizes somewhat expressions like "& v" and "& v0"

val mkAddrOrStartOf : lval -> exp

Like mkAddrOf except if the type of lval is an array then it uses StartOf. This is the right operation for getting a pointer to the start of the storage denoted by lval.

val mkMem : addr:exp -> off:offset -> lval

Make a Mem, while optimizing AddrOf. The type of the addr must be TPtr(t) and the type of the resulting lval is t. Note that in CIL the implicit conversion between an array and the pointer to the first element does not apply. You must do the conversion yourself using StartOf

val mkString : string -> exp

Make an expression that is a string constant (of pointer type)

val mkCastT : e:exp -> oldt:typ -> newt:typ -> exp

Construct a cast when having the old type of the expression. If the new * type is the same as the old type, then no cast is added.

val mkCast : e:exp -> newt:typ -> exp

Like Cil.mkCastT but uses typeOf to get oldt

val stripCasts : exp -> exp

Removes casts from this expression, but ignores casts within other expression constructs. So we delete the (A) and (B) casts from "(A)(B)(x + (C)y)", but leave the (C) cast.

val typeOf : exp -> typ

Compute the type of an expression

val parseInt : string -> exp

Convert a string representing a C integer literal to an expression. * Handles the prefixes 0x and 0 and the suffixes L, U, UL, LL, ULL

Values for manipulating statements

val mkStmt : stmtkind -> stmt

Construct a statement, given its kind. Initialize the sid field to -1, and labels, succs and preds to the empty list

val mkBlock : stmt list -> block

Construct a block with no attributes, given a list of statements

val mkStmtOneInstr : instr -> stmt

Construct a statement consisting of just one instruction

val compactStmts : stmt list -> stmt list

Try to compress statements so as to get maximal basic blocks. * use this instead of List.@ because you get fewer basic blocks

val mkEmptyStmt : unit -> stmt

Returns an empty statement (of kind Instr)

val dummyInstr : instr

A instr to serve as a placeholder

val dummyStmt : stmt

A statement consisting of just dummyInstr

val mkWhile : guard:exp -> body:stmt list -> stmt list

Make a while loop. Can contain Break or Continue

val mkForIncr : iter:varinfo -> first:exp -> stopat:exp -> incr:exp -> body:stmt list -> stmt list

Make a for loop for(i=start; i<past; i += incr) { ... }. The body can contain Break but not Continue. Can be used with i a pointer or an integer. Start and done must have the same type but incr must be an integer

val mkFor : start:stmt list -> guard:exp -> next:stmt list -> body:stmt list -> stmt list

Make a for loop for(start; guard; next) { ... }. The body can contain Break but not Continue !!!

Values for manipulating attributes

type attributeClass = Cil.attributeClass =
  1. | AttrName of bool
    (*

    Attribute of a name. If argument is true and we are on MSVC then the attribute is printed using __declspec as part of the storage specifier

    *)
  2. | AttrFunType of bool
    (*

    Attribute of a function type. If argument is true and we are on MSVC then the attribute is printed just before the function name

    *)
  3. | AttrType
    (*

    Attribute of a type

    *)

Various classes of attributes

val attributeHash : (string, attributeClass) Hashtbl.t

This table contains the mapping of predefined attributes to classes. Extend this table with more attributes as you need. This table is used to determine how to associate attributes with names or types

val partitionAttributes : default:attributeClass -> attributes -> attribute list * attribute list * attribute list

Partition the attributes into classes:name attributes, function type, and type attributes

val addAttribute : attribute -> attributes -> attributes

Add an attribute. Maintains the attributes in sorted order of the second argument

val addAttributes : attribute list -> attributes -> attributes

Add a list of attributes. Maintains the attributes in sorted order. The second argument must be sorted, but not necessarily the first

val dropAttribute : string -> attributes -> attributes

Remove all attributes with the given name. Maintains the attributes in sorted order.

val dropAttributes : string list -> attributes -> attributes

Remove all attributes with names appearing in the string list. * Maintains the attributes in sorted order

val filterAttributes : string -> attributes -> attributes

Retains attributes with the given name

val hasAttribute : string -> attributes -> bool

True if the named attribute appears in the attribute list. The list of attributes must be sorted.

val typeAttrs : typ -> attribute list

Returns all the attributes contained in a type. This requires a traversal of the type structure, in case of composite, enumeration and named types

val setTypeAttrs : typ -> attributes -> typ
val typeAddAttributes : attribute list -> typ -> typ

Add some attributes to a type

val typeRemoveAttributes : string list -> typ -> typ

Remove all attributes with the given names from a type. Note that this does not remove attributes from typedef and tag definitions, just from their uses

val expToAttrParam : exp -> attrparam

Convert an expression into an attrparam, if possible. Otherwise raise NotAnAttrParam with the offending subexpression

exception NotAnAttrParam of exp

The visitor

type 'a visitAction = 'a Cil.visitAction =
  1. | SkipChildren
    (*

    Do not visit the children. Return the node as it is.

    *)
  2. | DoChildren
    (*

    Continue with the children of this node. Rebuild the node on return if any of the children changes (use == test)

    *)
  3. | ChangeTo of 'a
    (*

    Replace the expression with the given one

    *)
  4. | ChangeDoChildrenPost of 'a * 'a -> 'a
    (*

    First consider that the entire exp is replaced by the first parameter. Then continue with the children. On return rebuild the node if any of the children has changed and then apply the function on the node

    *)

Different visiting actions. 'a will be instantiated with exp, instr, etc.

class type cilVisitor = object ... end

A visitor interface for traversing CIL trees. Create instantiations of * this type by specializing the class Cil.nopCilVisitor. Each of the * specialized visiting functions can also call the queueInstr to specify * that some instructions should be inserted before the current instruction * or statement. Use syntax like self#queueInstr to call a method * associated with the current object.

Default Visitor. Traverses the CIL tree without modifying anything

val visitCilFile : cilVisitor -> file -> unit

Visit a file. This will will re-cons all globals TWICE (so that it is * tail-recursive). Use Cil.visitCilFileSameGlobals if your visitor will * not change the list of globals.

val visitCilFileSameGlobals : cilVisitor -> file -> unit

A visitor for the whole file that does not change the globals (but maybe * changes things inside the globals). Use this function instead of * Cil.visitCilFile whenever appropriate because it is more efficient for * long files.

val visitCilGlobal : cilVisitor -> global -> global list

Visit a global

val visitCilFunction : cilVisitor -> fundec -> fundec

Visit a function definition

val visitCilExpr : cilVisitor -> exp -> exp
val visitCilLval : cilVisitor -> lval -> lval

Visit an lvalue

val visitCilOffset : cilVisitor -> offset -> offset

Visit an lvalue or recursive offset

val visitCilInitOffset : cilVisitor -> offset -> offset

Visit an initializer offset

val visitCilInstr : cilVisitor -> instr -> instr list

Visit an instruction

val visitCilStmt : cilVisitor -> stmt -> stmt

Visit a statement

val visitCilBlock : cilVisitor -> block -> block

Visit a block

val visitCilType : cilVisitor -> typ -> typ

Visit a type

val visitCilVarDecl : cilVisitor -> varinfo -> varinfo

Visit a variable declaration

val visitCilInit : cilVisitor -> varinfo -> offset -> init -> init

Visit an initializer, pass also the variable to which this belongs and the * offset.

val visitCilAttributes : cilVisitor -> attribute list -> attribute list

Visit a list of attributes

Utility functions

val msvcMode : bool ref

Whether the pretty printer should print output for the MS VC compiler. Default is GCC. After you set this function you should call Cil.initCIL.

val makeStaticGlobal : bool ref

Whether to convert local static variables into global static variables

val useLogicalOperators : bool ref

Whether to use the logical operands LAnd and LOr. By default, do not use * them because they are unlike other expressions and do not evaluate both of * their operands

val useComputedGoto : bool ref

Whether to use GCC's computed gotos. By default, do not use them and * replace them by a switch.

val useCaseRange : bool ref

Whether to expand ranges of values in case statements. By default, expand * them and do not use the CaseRange constructor.

val caseRangeFold : label list -> label list

Fold every CaseRange in a list of labels into the corresponding list of * Case labels. Raises Errormsg.Error if one of the ranges cannot be * constant folded.

val oldstyleExternInline : bool ref

Set this to true to get old-style handling of gcc's extern inline C extension: old-style: the extern inline definition is used until the actual definition is seen (as long as optimization is enabled) new-style: the extern inline definition is used only if there is no actual definition (as long as optimization is enabled) Note that CIL assumes that optimization is always enabled ;-)

val constFoldVisitor : bool -> cilVisitor

A visitor that does constant folding. Pass as argument whether you want * machine specific simplifications to be done, or not.

type lineDirectiveStyle = Cil.lineDirectiveStyle =
  1. | LineComment
    (*

    Before every element, print the line * number in comments. This is ignored by * processing tools (thus errors are reproted * in the CIL output), but useful for * visual inspection

    *)
  2. | LineCommentSparse
    (*

    Like LineComment but only print a line * directive for a new source line

    *)
  3. | LinePreprocessorInput
    (*

    Use # nnn directives (in gcc mode)

    *)
  4. | LinePreprocessorOutput
    (*

    Use #line directives

    *)

Styles of printing line directives

val lineDirectiveStyle : lineDirectiveStyle option ref

How to print line directives

val print_CIL_Input : bool ref

Whether we print something that will only be used as input to our own * parser. In that case we are a bit more liberal in what we print

val printCilAsIs : bool ref

Whether to print the CIL as they are, without trying to be smart and * print nicer code. Normally this is false, in which case the pretty * printer will turn the while(1) loops of CIL into nicer loops, will not * print empty "else" blocks, etc. There is one case howewer in which if you * turn this on you will get code that does not compile: if you use varargs * the __builtin_va_arg function will be printed in its internal form.

val lineLength : int ref

The length used when wrapping output lines. Setting this variable to * a large integer will prevent wrapping and make #line directives more * accurate.

val forgcc : string -> string

Return the string 's' if we're printing output for gcc, suppres * it if we're printing for CIL to parse back in. the purpose is to * hide things from gcc that it complains about, but still be able * to do lossless transformations when CIL is the consumer

Debugging support

val currentLoc : location ref

A reference to the current location. If you are careful to set this to * the current location then you can use some built-in logging functions that * will print the location.

val currentGlobal : global ref

A reference to the current global being visited

CIL has a fairly easy to use mechanism for printing error messages. This * mechanism is built on top of the pretty-printer mechanism (see * Pretty.doc) and the error-message modules (see Errormsg.error).

Here is a typical example for printing a log message: 

ignore (Errormsg.log "Expression %a is not positive (at %s:%i)\n"
                        d_exp e loc.file loc.line)

and here is an example of how you print a fatal error message that stop the * execution: 

Errormsg.s (Errormsg.bug "Why am I here?")

Notice that you can use C format strings with some extension. The most useful extension is "%a" that means to consumer the next two argument from the argument list and to apply the first to unit and then to the second and to print the resulting Pretty.doc. For each major type in CIL there is a corresponding function that pretty-prints an element of that type:

val d_loc : unit -> location -> Pretty.doc

Pretty-print a location

val d_thisloc : unit -> Pretty.doc

Pretty-print the Cil.currentLoc

val d_ikind : unit -> ikind -> Pretty.doc

Pretty-print an integer of a given kind

val d_fkind : unit -> fkind -> Pretty.doc

Pretty-print a floating-point kind

val d_storage : unit -> storage -> Pretty.doc

Pretty-print storage-class information

val d_const : unit -> constant -> Pretty.doc

Pretty-print a constant

val derefStarLevel : int
val indexLevel : int
val arrowLevel : int
val addrOfLevel : int
val additiveLevel : int
val comparativeLevel : int
val bitwiseLevel : int
val getParenthLevel : exp -> int

Parentheses level. An expression "a op b" is printed parenthesized if its * parentheses level is >= that that of its context. Identifiers have the * lowest level and weakly binding operators (e.g. |) have the largest level. * The correctness criterion is that a smaller level MUST correspond to a * stronger precedence!

class type cilPrinter = object ... end

A printer interface for CIL trees. Create instantiations of * this type by specializing the class Cil.defaultCilPrinterClass.

val defaultCilPrinter : cilPrinter

These are pretty-printers that will show you more details on the internal * CIL representation, without trying hard to make it look like C

val plainCilPrinter : cilPrinter
class type descriptiveCilPrinter = object ... end

Like defaultCilPrinterClass, but instead of temporary variable names it prints the description that was provided when the temp was created. This is usually better for messages that are printed for end users, although you may want the temporary names for debugging.

val descriptiveCilPrinter : descriptiveCilPrinter
val printerForMaincil : cilPrinter ref

zra: This is the pretty printer that Maincil will use. by default it is set to defaultCilPrinter

val printType : cilPrinter -> unit -> typ -> Pretty.doc

Print a type given a pretty printer

val printExp : cilPrinter -> unit -> exp -> Pretty.doc

Print an expression given a pretty printer

val printLval : cilPrinter -> unit -> lval -> Pretty.doc

Print an lvalue given a pretty printer

val printGlobal : cilPrinter -> unit -> global -> Pretty.doc

Print a global given a pretty printer

val printAttr : cilPrinter -> unit -> attribute -> Pretty.doc

Print an attribute given a pretty printer

val printAttrs : cilPrinter -> unit -> attributes -> Pretty.doc

Print a set of attributes given a pretty printer

val printInstr : cilPrinter -> unit -> instr -> Pretty.doc

Print an instruction given a pretty printer

val printStmt : cilPrinter -> unit -> stmt -> Pretty.doc

Print a statement given a pretty printer. This can take very long * (or even overflow the stack) for huge statements. Use Cil.dumpStmt * instead.

val printBlock : cilPrinter -> unit -> block -> Pretty.doc

Print a block given a pretty printer. This can take very long * (or even overflow the stack) for huge block. Use Cil.dumpBlock * instead.

val dumpStmt : cilPrinter -> out_channel -> int -> stmt -> unit

Dump a statement to a file using a given indentation. Use this instead of * Cil.printStmt whenever possible.

val dumpBlock : cilPrinter -> out_channel -> int -> block -> unit

Dump a block to a file using a given indentation. Use this instead of * Cil.printBlock whenever possible.

val printInit : cilPrinter -> unit -> init -> Pretty.doc

Print an initializer given a pretty printer. This can take very long * (or even overflow the stack) for huge initializers. Use Cil.dumpInit * instead.

val dumpInit : cilPrinter -> out_channel -> int -> init -> unit

Dump an initializer to a file using a given indentation. Use this instead of * Cil.printInit whenever possible.

val d_type : unit -> typ -> Pretty.doc

Pretty-print a type using Cil.defaultCilPrinter

val d_exp : unit -> exp -> Pretty.doc

Pretty-print an expression using Cil.defaultCilPrinter

val d_lval : unit -> lval -> Pretty.doc

Pretty-print an lvalue using Cil.defaultCilPrinter

val d_offset : Pretty.doc -> unit -> offset -> Pretty.doc

Pretty-print an offset using Cil.defaultCilPrinter, given the pretty * printing for the base.

val d_init : unit -> init -> Pretty.doc

Pretty-print an initializer using Cil.defaultCilPrinter. This can be * extremely slow (or even overflow the stack) for huge initializers. Use * Cil.dumpInit instead.

val d_binop : unit -> binop -> Pretty.doc

Pretty-print a binary operator

val d_unop : unit -> unop -> Pretty.doc

Pretty-print a unary operator

val d_attr : unit -> attribute -> Pretty.doc

Pretty-print an attribute using Cil.defaultCilPrinter

val d_attrparam : unit -> attrparam -> Pretty.doc

Pretty-print an argument of an attribute using Cil.defaultCilPrinter

val d_attrlist : unit -> attributes -> Pretty.doc

Pretty-print a list of attributes using Cil.defaultCilPrinter

val d_instr : unit -> instr -> Pretty.doc

Pretty-print an instruction using Cil.defaultCilPrinter

val d_label : unit -> label -> Pretty.doc

Pretty-print a label using Cil.defaultCilPrinter

val d_stmt : unit -> stmt -> Pretty.doc

Pretty-print a statement using Cil.defaultCilPrinter. This can be * extremely slow (or even overflow the stack) for huge statements. Use * Cil.dumpStmt instead.

val d_block : unit -> block -> Pretty.doc

Pretty-print a block using Cil.defaultCilPrinter. This can be * extremely slow (or even overflow the stack) for huge blocks. Use * Cil.dumpBlock instead.

val d_global : unit -> global -> Pretty.doc

Pretty-print the internal representation of a global using * Cil.defaultCilPrinter. This can be extremely slow (or even overflow the * stack) for huge globals (such as arrays with lots of initializers). Use * Cil.dumpGlobal instead.

val dn_exp : unit -> exp -> Pretty.doc

Versions of the above pretty printers, that don't print #line directives

val dn_lval : unit -> lval -> Pretty.doc
val dn_init : unit -> init -> Pretty.doc
val dn_type : unit -> typ -> Pretty.doc
val dn_global : unit -> global -> Pretty.doc
val dn_attrlist : unit -> attributes -> Pretty.doc
val dn_attr : unit -> attribute -> Pretty.doc
val dn_attrparam : unit -> attrparam -> Pretty.doc
val dn_stmt : unit -> stmt -> Pretty.doc
val dn_instr : unit -> instr -> Pretty.doc
val d_shortglobal : unit -> global -> Pretty.doc

Pretty-print a short description of the global. This is useful for error * messages

val dumpGlobal : cilPrinter -> out_channel -> global -> unit

Pretty-print a global. Here you give the channel where the printout * should be sent.

val dumpFile : cilPrinter -> out_channel -> string -> file -> unit

Pretty-print an entire file. Here you give the channel where the printout * should be sent.

the following error message producing functions also print a location in * the code. use Errormsg.bug and Errormsg.unimp if you do not want * that

val bug : ('a, unit, Pretty.doc) format -> 'a

Like Errormsg.bug except that Cil.currentLoc is also printed

val unimp : ('a, unit, Pretty.doc) format -> 'a

Like Errormsg.unimp except that Cil.currentLocis also printed

val error : ('a, unit, Pretty.doc) format -> 'a

Like Errormsg.error except that Cil.currentLoc is also printed

val errorLoc : location -> ('a, unit, Pretty.doc) format -> 'a

Like Cil.error except that it explicitly takes a location argument, * instead of using the Cil.currentLoc

val warn : ('a, unit, Pretty.doc) format -> 'a

Like Errormsg.warn except that Cil.currentLoc is also printed

val warnOpt : ('a, unit, Pretty.doc) format -> 'a

Like Errormsg.warnOpt except that Cil.currentLoc is also printed. * This warning is printed only of Errormsg.warnFlag is set.

val warnContext : ('a, unit, Pretty.doc) format -> 'a

Like Errormsg.warn except that Cil.currentLoc and context is also printed

val warnContextOpt : ('a, unit, Pretty.doc) format -> 'a

Like Errormsg.warn except that Cil.currentLoc and context is also * printed. This warning is printed only of Errormsg.warnFlag is set.

val warnLoc : location -> ('a, unit, Pretty.doc) format -> 'a

Like Cil.warn except that it explicitly takes a location argument, * instead of using the Cil.currentLoc

Sometimes you do not want to see the syntactic sugar that the above * pretty-printing functions add. In that case you can use the following * pretty-printing functions. But note that the output of these functions is * not valid C

val d_plainexp : unit -> exp -> Pretty.doc

Pretty-print the internal representation of an expression

val d_plaininit : unit -> init -> Pretty.doc

Pretty-print the internal representation of an integer

val d_plainlval : unit -> lval -> Pretty.doc

Pretty-print the internal representation of an lvalue

Pretty-print the internal representation of an lvalue offset val d_plainoffset: unit -> offset -> Pretty.doc

val d_plaintype : unit -> typ -> Pretty.doc

Pretty-print the internal representation of a type

val dd_exp : unit -> exp -> Pretty.doc

Pretty-print an expression while printing descriptions rather than names of temporaries.

val dd_lval : unit -> lval -> Pretty.doc

Pretty-print an lvalue on the left side of an assignment. If there is an offset or memory dereference, temporaries will be replaced by descriptions as in dd_exp. If the lval is a temp var, that var will not be replaced by a description; use "dd_exp () (Lval lv)" if that's what you want.

ALPHA conversion has been moved to the Alpha module.

val uniqueVarNames : file -> unit

Assign unique names to local variables. This might be necessary after you * transformed the code and added or renamed some new variables. Names are * not used by CIL internally, but once you print the file out the compiler * downstream might be confused. You might * have added a new global that happens to have the same name as a local in * some function. Rename the local to ensure that there would never be * confusion. Or, viceversa, you might have added a local with a name that * conflicts with a global

Optimization Passes

val peepHole2 : ((instr * instr) -> instr list option) -> stmt list -> unit

A peephole optimizer that processes two adjacent instructions and possibly replaces them both. If some replacement happens, then the new instructions are themselves subject to optimization

val peepHole1 : (instr -> instr list option) -> stmt list -> unit

Similar to peepHole2 except that the optimization window consists of one instruction, not two

Machine dependency

exception SizeOfError of string * typ

Raised when one of the bitsSizeOf functions cannot compute the size of a * type. This can happen because the type contains array-length expressions * that we don't know how to compute or because it is a type whose size is * not defined (e.g. TFun or an undefined compinfo). The string is an * explanation of the error

val unsignedVersionOf : ikind -> ikind

Give the unsigned kind corresponding to any integer kind

val signedVersionOf : ikind -> ikind

Give the signed kind corresponding to any integer kind

val intRank : ikind -> int

Return the integer conversion rank of an integer kind

val commonIntKind : ikind -> ikind -> ikind

Return the common integer kind of the two integer arguments, as defined in ISO C 6.3.1.8 ("Usual arithmetic conversions")

val intKindForSize : int -> bool -> ikind

The signed integer kind for a given size (unsigned if second argument * is true). Raises Not_found if no such kind exists

val floatKindForSize : int -> fkind

The float kind for a given size. Raises Not_found * if no such kind exists

val bytesSizeOfInt : ikind -> int

The size in bytes of the given int kind.

val bitsSizeOf : typ -> int

The size of a type, in bits. Trailing padding is added for structs and * arrays. Raises Cil.SizeOfError when it cannot compute the size. This * function is architecture dependent, so you should only call this after you * call Cil.initCIL. Remember that on GCC sizeof(void) is 1!

val truncateCilint : ikind -> Cilint.cilint -> Cilint.cilint * Cilint.truncation

Represents an integer as for a given kind. Returns a truncation * flag saying that the value fit in the kind (NoTruncation), didn't * fit but no "interesting" bits (all-0 or all-1) were lost * (ValueTruncation) or that bits were lost (BitTruncation). Another * way to look at the ValueTruncation result is that if you had used * the kind of opposite signedness (e.g. IUInt rather than IInt), you * would gave got NoTruncation...

val fitsInInt : ikind -> Cilint.cilint -> bool

True if the integer fits within the kind's range

val intKindForValue : Cilint.cilint -> bool -> ikind

Return the smallest kind that will hold the integer's value. The * kind will be unsigned if the 2nd argument is true, signed * otherwise. Note that if the value doesn't fit in any of the * available types, you will get ILongLong (2nd argument false) or * IULongLong (2nd argument true).

val mkCilint : ikind -> int64 -> Cilint.cilint

Construct a cilint from an integer kind and int64 value. Used for * getting the actual constant value from a CInt64(n, ik, _) * constant.

val sizeOf : typ -> exp

The size of a type, in bytes. Returns a constant expression or a * "sizeof" expression if it cannot compute the size. This function * is architecture dependent, so you should only call this after you * call Cil.initCIL.

val alignOf_int : typ -> int

The minimum alignment (in bytes) for a type. This function is * architecture dependent, so you should only call this after you call * Cil.initCIL.

val bitsOffset : typ -> offset -> int * int

Give a type of a base and an offset, returns the number of bits from the * base address and the width (also expressed in bits) for the subobject * denoted by the offset. Raises Cil.SizeOfError when it cannot compute * the size. This function is architecture dependent, so you should only call * this after you call Cil.initCIL.

val char_is_unsigned : bool ref

Whether "char" is unsigned. Set after you call Cil.initCIL

val little_endian : bool ref

Whether the machine is little endian. Set after you call Cil.initCIL

val underscore_name : bool ref

Whether the compiler generates assembly labels by prepending "_" to the identifier. That is, will function foo() have the label "foo", or "_foo"? Set after you call Cil.initCIL

val locUnknown : location

Represents a location that cannot be determined

val get_instrLoc : instr -> location

Return the location of an instruction

val get_globalLoc : global -> location

Return the location of a global, or locUnknown

val get_stmtLoc : stmtkind -> location

Return the location of a statement, or locUnknown

val dExp : Pretty.doc -> exp

Generate an Cil.exp to be used in case of errors.

val dInstr : Pretty.doc -> location -> instr

Generate an Cil.instr to be used in case of errors.

val dGlobal : Pretty.doc -> location -> global

Generate a Cil.global to be used in case of errors.

val mapNoCopy : ('a -> 'a) -> 'a list -> 'a list

Like map but try not to make a copy of the list

val mapNoCopyList : ('a -> 'a list) -> 'a list -> 'a list

Like map but each call can return a list. Try not to make a copy of the list

val startsWith : string -> string -> bool

sm: return true if the first is a prefix of the second string

val endsWith : string -> string -> bool

return true if the first is a suffix of the second string

val stripUnderscores : string -> string

If string has leading and trailing __, strip them.

An Interpreter for constructing CIL constructs

type formatArg = Cil.formatArg =
  1. | Fe of exp
  2. | Feo of exp option
    (*

    For array lengths

    *)
  3. | Fu of unop
  4. | Fb of binop
  5. | Fk of ikind
  6. | FE of exp list
    (*

    For arguments in a function call

    *)
  7. | Ff of string * typ * attributes
    (*

    For a formal argument

    *)
  8. | FF of (string * typ * attributes) list
    (*

    For formal argument lists

    *)
  9. | Fva of bool
    (*

    For the ellipsis in a function type

    *)
  10. | Fv of varinfo
  11. | Fl of lval
  12. | Flo of lval option
  13. | Fo of offset
  14. | Fc of compinfo
  15. | Fi of instr
  16. | FI of instr list
  17. | Ft of typ
  18. | Fd of int
  19. | Fg of string
  20. | Fs of stmt
  21. | FS of stmt list
  22. | FA of attributes
  23. | Fp of attrparam
  24. | FP of attrparam list
  25. | FX of string

The type of argument for the interpreter

val d_formatarg : unit -> formatArg -> Pretty.doc

Pretty-prints a format arg

val warnTruncate : bool ref

Emit warnings when truncating integer constants (default true)

val envMachine : Machdep.mach option ref

Machine model specified via CIL_MACHINE environment variable

val convertInts : int64 -> ikind -> int64 -> ikind -> int64 * int64 * ikind
  • deprecated

    . Convert two int64/kind pairs to a common int64/int64/kind triple.

val isInteger : exp -> int64 option
  • deprecated

    . Can't handle large 64-bit unsigned constants correctly - use getInteger instead. If the given expression is a (possibly cast'ed) character or an integer constant, return that integer. Otherwise, return None.

val truncateInteger64 : ikind -> int64 -> int64 * bool
  • deprecated

    . Use truncateCilint instead. Represents an integer as * for a given kind. Returns a flag saying whether the value was * changed during truncation (because it was too large to fit in k).

val gccBuiltins : (string, typ * typ list * bool) Hashtbl.t
val msvcBuiltins : (string, typ * typ list * bool) Hashtbl.t
val d_varinfo : unit -> varinfo -> Pretty.doc
include module type of struct include Pretty end

API

type doc = Pretty.doc

The type of unformated documents. Elements of this type can be * constructed in two ways. Either with a number of constructor shown below, * or using the Pretty.dprintf function with a printf-like interface. * The Pretty.dprintf method is slightly slower so we do not use it for * large jobs such as the output routines for a compiler. But we use it for * small jobs such as logging and error messages.

Constructors for the doc type.

val nil : doc

Constructs an empty document

val (++) : doc -> doc -> doc

Concatenates two documents. This is an infix operator that associates to the left.

val concat : doc -> doc -> doc
val text : string -> doc

A document that prints the given string

val num : int -> doc

A document that prints an integer in decimal form

val num64 : int64 -> doc

A document that prints a 64-bit int in decimal form

val real : float -> doc

A document that prints a real number

val chr : char -> doc

A document that prints a character. This is just like Pretty.text with a one-character string.

val line : doc

A document that consists of a mandatory newline. This is just like (text "\n"). The new line will be indented to the current indentation level, unless you use Pretty.leftflush right after this.

val leftflush : doc

Use after a Pretty.line to prevent the indentation. Whatever follows * next will be flushed left. Indentation resumes on the next line.

val break : doc

A document that consists of either a space or a line break. Also called an optional line break. Such a break will be taken only if necessary to fit the document in a given width. If the break is not taken a space is printed instead.

val align : doc

Mark the current column as the current indentation level. Does not print anything. All taken line breaks will align to this column. The previous alignment level is saved on a stack.

val unalign : doc

Reverts to the last saved indentation level.

val mark : doc

Mark the beginning of a markup section. The width of a markup section is * considered 0 for the purpose of computing identation

val unmark : doc

The end of a markup section

Syntactic sugar

val indent : int -> doc -> doc

Indents the document. Same as ((text " ") ++ align ++ doc ++ unalign), with the specified number of spaces.

val markup : doc -> doc

Prints a document as markup. The marked document cannot contain line * breaks or alignment constructs.

val seq : sep:doc -> doit:('a -> doc) -> elements:'a list -> doc

Formats a sequence. sep is a separator, doit is a function that * converts an element to a document.

val docList : ?sep:doc -> ('a -> doc) -> unit -> 'a list -> doc

An alternative function for printing a list. The unit argument is there * to make this function more easily usable with the Pretty.dprintf * interface. The first argument is a separator, by default a comma.

val d_list : string -> (unit -> 'a -> doc) -> unit -> 'a list -> doc

sm: Yet another list printer. This one accepts the same kind of * printing function that Pretty.dprintf does, and itself works * in the dprintf context. Also accepts * a string as the separator since that's by far the most common.

val docArray : ?sep:doc -> (int -> 'a -> doc) -> unit -> 'a array -> doc

Formats an array. A separator and a function that prints an array element. The default separator is a comma.

val docOpt : ('a -> doc) -> unit -> 'a option -> doc

Prints an 'a option with None or Some

val d_int32 : int32 -> doc

Print an int32

val f_int32 : unit -> int32 -> doc
val d_int64 : int64 -> doc
val f_int64 : unit -> int64 -> doc
module MakeMapPrinter = Pretty.MakeMapPrinter

Format maps.

module MakeSetPrinter = Pretty.MakeSetPrinter

Format sets.

val insert : unit -> doc -> doc

A function that is useful with the printf-like interface

val dprintf : ('a, unit, doc, doc) format4 -> 'a

This function provides an alternative method for constructing doc objects. The first argument for this function is a format string argument (of type ('a, unit, doc) format; if you insist on understanding what that means see the module Printf). The format string is like that for the printf function in C, except that it understands a few more formatting controls, all starting with the @ character.

See the gprintf function if you want to pipe the result of dprintf into some other functions.

The following special formatting characters are understood (these do not correspond to arguments of the function):

In addition to the usual printf % formatting characters the following two new characters are supported:

  • %t Corresponds to an argument of type unit -> doc. This argument is invoked to produce a document
  • %a Corresponds to two arguments. The first of type unit -> 'a -> doc and the second of type 'a. (The extra unit is do to the peculiarities of the built-in support for format strings in Ocaml. It turns out that it is not a major problem.) Here is an example of how you use this:
dprintf "Name=%s, SSN=%7d, Children=\@\[%a\@\]\n"
             pers.name pers.ssn (docList (chr ',' ++ break) text)
             pers.children

The result of dprintf is a Pretty.doc. You can format the document and emit it using the functions Pretty.fprint and Pretty.sprint.

val gprintf : (doc -> 'b) -> ('a, unit, doc, 'b) format4 -> 'a

Like Pretty.dprintf but more general. It also takes a function that is * invoked on the constructed document but before any formatting is done. The * type of the format argument means that 'a is the type of the parameters of * this function, unit is the type of the first argument to %a and %t * formats, doc is the type of the intermediate result, and 'b is the type of * the result of gprintf.

val fprint : out_channel -> width:int -> doc -> unit

Format the document to the given width and emit it to the given channel

val fprintf : out_channel -> ('a, unit, doc) format -> 'a

Like Pretty.dprintf followed by Pretty.fprint

val printf : ('a, unit, doc) format -> 'a

Like Pretty.fprintf applied to stdout

val eprintf : ('a, unit, doc) format -> 'a

Like Pretty.fprintf applied to stderr

val withPrintDepth : int -> (unit -> unit) -> unit

Invokes a thunk, with printDepth temporarily set to the specified value

The following variables can be used to control the operation of the printer

val printDepth : int ref

Specifies the nesting depth of the align/unalign pairs at which everything is replaced with ellipsis

val printIndent : bool ref

If false then does not indent

val fastMode : bool ref

If set to true then optional breaks are taken only when the document has exceeded the given width. This means that the printout will looked more ragged but it will be faster

val flushOften : bool ref

If true the it flushes after every print

val flattenBeforePrint : bool ref

Whether to rebalance doc before printing it to avoid stack-overflows

val countNewLines : int ref

Keep a running count of the taken newlines. You can read and write this * from the client code if you want

val auto_printer : string -> 'b

A function that when used at top-level in a module will direct * the pa_prtype module generate automatically the printing functions for a * type

val sprint : (unit -> 'a -> Pretty.doc) -> 'a -> string