Frama-C API - Extlib
Useful operations. This module does not depend of any of frama-c module.
Ensure that the given filename has the extension "cmo" in bytecode and "cmxs" in native
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
Function builders
Function combinators
Tuples
Nest the first argument with the first element of the pair given as second argument.
Lists
replace cmp x l
replaces the first element y
of l
such that cmp x y
is true by x
. If no such element exists, x
is added at the tail of l
.
product f acc l1 l2
is similar to fold_left f acc l12
with l12 the list of all pairs of an elt of l1
and an elt of l2
product f l1 l2
applies f
to all the pairs of an elt of l1
and an element of l2
.
returns the index (starting at 0) of the first element verifying the condition
Generic list comparison function, where the elements are compared with the specified function
subsets k l
computes the combinations of k
elements from list l
. E.g. subsets 2 1;2;3;4
= [1;2];[1;3];[1;4];[2;3];[2;4];[3;4]
. This function preserves the order of the elements in l
when computing the sublists. l
should not contain duplicates.
list_first_n n l
returns the first n
elements of the list. Tail recursive. It returns an empty list if n
is nonpositive and the whole list if n
is greater than List.length l
. It is equivalent to list_slice ~last:n l
.
list_slice ?first ?last l
is equivalent to Python's slice operator (lfirst:last
): returns the range of the list between first
(inclusive) and last
(exclusive), starting from 0. If omitted, first
defaults to 0 and last
to List.length l
. Negative indices are allowed, and count from the end of the list. list_slice
never raises exceptions: out-of-bounds arguments are clipped, and inverted ranges result in empty lists.
Like map but each call can return a list. Try not to make a copy of the list
Options
merge f k a b
returns
None
if botha
andb
areNone
Some a'
(resp.b'
ifb
(respa
) isNone
anda
(resp.b
) isSome
f k a' b'
if botha
andb
areSome
It is mainly intended to be used with Map.merge
Strings
string_del_prefix ~strict p s
returns None
if p
is not a prefix of s
and Some s1
iff s=p^s1
.
string_del_suffix ~strict suf s
returns Some s1
when s = s1 ^ suf
and None of suf
is not a suffix of s
.
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
remove underscores at the beginning and end of a string. If a string is composed solely of underscores, return the empty string
format_string_of_stag stag
returns the string corresponding to stag
, or raises an exception if the tag extension is unsupported.
Performance
System commands
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
Use this function instead of Stdlib.compare
, as this makes it easier to find incorrect uses of the latter