module Builtins_string:sig
..end
Value builtins related to functions in string.h.
The actual builtins are registered through Builtins.register_builtin
.
The functions below are also used for the evaluation of logical predicates
valid_string
and valid_read_string
.
module String_alarms:Datatype.S_with_collections
with type t = string * string
Alarms are pairs (assertion, warning_msg): ACSL "assertion", Informative message on why the evaluation raised an alarm
type
expterm =
| |
Exp of |
| |
Term of |
typestr_builtin_sig =
Cvalue.Model.t ->
(expterm * Cvalue.V.t) list ->
Value_types.call_result * String_alarms.Set.t
val frama_c_strlen_wrapper : str_builtin_sig
val frama_c_strnlen_wrapper : str_builtin_sig
val frama_c_rawmemchr_wrapper : str_builtin_sig
val frama_c_memchr_wrapper : str_builtin_sig
val frama_c_strchr_wrapper : str_builtin_sig
val frama_c_wcslen_wrapper : unit -> str_builtin_sig
val frama_c_wcschr_wrapper : unit -> str_builtin_sig
val frama_c_wmemchr_wrapper : unit -> str_builtin_sig