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
Tuples
Nest the first argument with the first element of the pair given as second argument.
Strings
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
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.
