Frama-C:
Plug-ins:
Libraries:

Frama-C API - Extlib

Useful operations. This module does not depend of any of frama-c module.

val adapt_filename : string -> string

Ensure that the given filename has the extension "cmo" in bytecode and "cmxs" in native

val max_cpt : int -> int -> int

max_cpt t1 t2 returns the maximum of t1 and t2 wrt the total ordering induced by tags creation. This ordering is defined as follows: forall tags t1 t2, t1 <= t2 iff t1 is before t2 in the finite sequence 0; 1; ..; max_int; min_int; min_int-1; -1

val number_to_color : int -> int

Function builders

exception Unregistered_function of string

Never catch it yourself: let the kernel do the job.

  • since Oxygen-20120901
val mk_labeled_fun : string -> 'a

To be used to initialized a reference over a labeled function.

  • since Oxygen-20120901
val mk_fun : string -> ('a -> 'b) Stdlib.ref

Build a reference to an uninitialized function

Tuples

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

Nest the first argument with the first element of the pair given as second argument.

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

Flatten the pairs into a triplet.

Strings

val make_unique_name : (string -> bool) -> ?sep:string -> ?start:int -> string -> int * string

make_unique_name mem s returns (0, s) when (mem s)=false otherwise returns (n,new_string) such that new_string is derived from (s,sep,start) and (mem new_string)=false and n<>0

  • since Oxygen-20120901
val format_string_of_stag : Stdlib.Format.stag -> string

format_string_of_stag stag returns the string corresponding to stag, or raises an exception if the tag extension is unsupported.

  • since 22.0-Titanium

Performance

val address_of_value : 'a -> int

System commands

val safe_at_exit : (unit -> unit) -> unit

Register function to call with Stdlib.at_exit, but only for non-child process (fork). The order of execution is preserved wrt ordinary calls to Stdlib.at_exit.

Comparison functions

val compare_basic : 'a -> 'a -> int

Use this function instead of Stdlib.compare, as this makes it easier to find incorrect uses of the latter