Module Builtins_string

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 = 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 = 
| Exp of Cil_types.exp
| Term of Cil_types.term
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
val frama_c_wcslen_wrapper : unit -> str_builtin_sig