module Builtins_string: sig
.. end
Value builtins related to functions in string.h.
The actual builtins are registed 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 = Alarms.t * string * string
Alarms are triples (kind, text, warning_msg): Alarm kind, Message text (to be emitted via emit_alarm), Warning message (to be emitted via Value_util.alarm_report)
type
expterm =
type
str_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