package frama-c
Install
dune-project
Dependency
Authors
-
MMichele Alberti
-
TThibaud Antignac
-
GGergö Barany
-
PPatrick Baudin
-
TThibaut Benjamin
-
AAllan Blanchard
-
LLionel Blatter
-
FFrançois Bobot
-
RRichard Bonichon
-
QQuentin Bouillaguet
-
DDavid Bühler
-
ZZakaria Chihani
-
LLoïc Correnson
-
JJulien Crétin
-
PPascal Cuoq
-
ZZaynah Dargaye
-
BBasile Desloges
-
JJean-Christophe Filliâtre
-
PPhilippe Herrmann
-
MMaxime Jacquemin
-
FFlorent Kirchner
-
AAlexander Kogtenkov
-
TTristan Le Gall
-
JJean-Christophe Léchenet
-
MMatthieu Lemerre
-
DDara Ly
-
DDavid Maison
-
CClaude Marché
-
AAndré Maroneze
-
TThibault Martin
-
FFonenantsoa Maurica
-
MMelody Méaulle
-
BBenjamin Monate
-
YYannick Moy
-
PPierre Nigron
-
AAnne Pacalet
-
VValentin Perrelle
-
GGuillaume Petiot
-
DDario Pinto
-
VVirgile Prevosto
-
AArmand Puccetti
-
FFélix Ridoux
-
VVirgile Robles
-
JJan Rochel
-
MMuriel Roger
-
JJulien Signoles
-
NNicolas Stouls
-
KKostyantyn Vorobyov
-
BBoris Yakobowski
Maintainers
Sources
sha256=29612882330ecb6eddd0b4ca3afc0492b70d0feb3379a1b8e893194c6e173983
doc/frama-c.kernel/Frama_c_kernel/Extlib/index.html
Module Frama_c_kernel.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
val mk_fun : string -> ('a -> 'b) refBuild a reference to an uninitialized function
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.
Combines filter fold_left and map
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.
Options
merge f k a b returns
Noneif bothaandbareNoneSome a'(resp.b'ifb(respa) isNoneanda(resp.b) isSomef k a' b'if bothaandbareSome
It is mainly intended to be used with Map.merge
Strings
string_prefix ~strict p s returns true if and only if p is a prefix of the string s. If strict is true, the prefix must be strict (that is, s must moreover be strictly longer than p). strict is false by default.
string_del_prefix ~strict p s returns None if p is not a prefix of s and Some s1 iff s=p^s1.
string_suffix ~strict suf s returns true iff suf is a suffix of string s. strict, which defaults to false, indicates whether s should be strictly longer than p.
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
val format_string_of_stag : Format.stag -> stringformat_string_of_stag stag returns the string corresponding to stag, or raises an exception if the tag extension is unsupported.
Performance
System commands
val mkdir : ?parents:bool -> Filepath.Normalized.t -> Unix.file_perm -> boolmkdir ?parents name perm creates directory name with permission perm. If parents is true, recursively create parent directories if needed. parents defaults to false. Note that this function may create some of the parent directories and then fail to create the children, e.g. if perm does not allow user execution of the created directory. This will leave the filesystem in a modified state before raising an exception. Returns true if the directory was created, false otherwise.
but not a directory, otherwise do nothing if directory already exists). Changed type of name argument and return type.
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.
cleanup_at_exit file indicates that file must be removed when the program exits (except if exit is caused by a signal). If file does not exist, nothing happens.
Similar to Filename.temp_file except that the temporary file will be deleted at the end of the execution (see above), unless debug is set to true, in which case a message with the name of the kept file will be printed.
val temp_dir_cleanup_at_exit : ?debug:bool -> string -> Filepath.Normalized.tComparison functions
Use this function instead of Stdlib.compare, as this makes it easier to find incorrect uses of the latter