From bf6266d6a1bffb7e7fe354394428a31cc06d16e7 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Tue, 9 Jun 2026 12:54:17 -0700 Subject: [PATCH 01/15] CHB: add support for gcc nonnull and format attributes --- .../bchlib/bCHAttributesFunctionSemantics.ml | 78 ++++++++++++++++++- .../bchlib/bCHFunctionSemanticsAttributes.ml | 9 +++ 2 files changed, 86 insertions(+), 1 deletion(-) diff --git a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml index 437509c6..0fbdccb4 100644 --- a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml +++ b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml @@ -25,6 +25,17 @@ SOFTWARE. ============================================================================= *) +(* Input path: attributes → function semantics (preconditions, side effects, + postconditions). + + Accepted attribute forms: + - GCC compatibility (read-only; never emitted on output): + access, nonnull, format + - Canonical CodeHawk forms (input and output): + chk_pre, chk_se, chk_post + + See bCHFunctionSemanticsAttributes.ml for the output path. *) + (* chutil *) open CHLogger open CHTraceResult @@ -215,6 +226,63 @@ let get_not_null_precondition attrparams_to_string "argparams" argparams] +let get_nonnull_preconditions + (fparams: fts_parameter_t list) + (attrparams: b_attrparam_t list): xxpredicate_t list = + match attrparams with + | [] -> + (* bare nonnull: all pointer parameters must be non-null *) + List.filter_map (fun par -> + if is_pointer par.apar_type then + Some (XXNotNull (ArgValue par)) + else + None) fparams + | _ -> + (* indexed nonnull: listed parameters must be non-null *) + List.filter_map (fun attrparam -> + match attrparam with + | AInt index -> + TR.tfold + ~ok:(fun par -> Some (XXNotNull (ArgValue par))) + ~error:(fun _ -> None) + (get_par fparams index) + | _ -> None) attrparams + + +let get_format_preconditions + (name: string) + (fparams: fts_parameter_t list) + (attrparams: b_attrparam_t list): xxpredicate_t list = + match attrparams with + | ACons (archetype, []) :: AInt string_index :: _ -> + let mk_pre constructor = + TR.tfold + ~ok:(fun par -> [constructor (ArgValue par)]) + ~error:(fun _ -> []) + (get_par fparams string_index) in + (match archetype with + | "printf" | "gnu_printf" -> mk_pre (fun t -> XXOutputFormatString t) + | "scanf" | "gnu_scanf" -> mk_pre (fun t -> XXInputFormatString t) + | _ -> + begin + log_diagnostics_result + ~tag:"get_format_preconditions:archetype not handled" + ~msg:name + __FILE__ __LINE__ + ["archetype: " ^ archetype]; + [] + end) + | _ -> + begin + log_diagnostics_result + ~tag:"get_format_preconditions:params not recognized" + ~msg:name + __FILE__ __LINE__ + [attrparams_to_string "attrparams" attrparams]; + [] + end + + let get_null_terminated_precondition (fparams: fts_parameter_t list) (tagparams: b_attrparam_t list) @@ -537,11 +605,19 @@ let convert_b_attributes_to_function_conditions List.fold_left (fun ((xpre, xside, xpost) as acc) attr -> match attr with - | Attr (("acccess" | "chk_access"), attrparams) -> + | Attr ("access", attrparams) -> let pre = get_access_preconditions name fparameters attrparams in let side = get_access_sideeffect name fparameters attrparams in (pre @ xpre, side @ xside, xpost) + | Attr ("nonnull", attrparams) -> + let pre = get_nonnull_preconditions fparameters attrparams in + (pre @ xpre, xside, xpost) + + | Attr ("format", attrparams) -> + let pre = get_format_preconditions name fparameters attrparams in + (pre @ xpre, xside, xpost) + | Attr ("chk_pre", attrparams) -> let pre = get_chk_pre_conditions name fparameters attrparams in (pre @ xpre, xside, xpost) diff --git a/CodeHawk/CHB/bchlib/bCHFunctionSemanticsAttributes.ml b/CodeHawk/CHB/bchlib/bCHFunctionSemanticsAttributes.ml index 1072a498..d284b449 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionSemanticsAttributes.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionSemanticsAttributes.ml @@ -25,6 +25,15 @@ SOFTWARE. ============================================================================= *) +(* Output path: function semantics → attributes (for delegated preconditions, + side effects, postconditions in generated header files). + + Only canonical CodeHawk forms (chk_pre, chk_se, chk_post) are emitted. + GCC compatibility forms (access, nonnull, format) are accepted on input + but never generated here. + + See bCHAttributesFunctionSemantics.ml for the input path. *) + (* chutil *) open CHLogger open CHTraceResult From 772dfb5b8a5275ac276085d2841cf1fdc5b658bc Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Tue, 9 Jun 2026 14:26:04 -0700 Subject: [PATCH 02/15] CHB: add codehawk-specific attributes for input of preconditions --- .../bchlib/bCHAttributesFunctionSemantics.ml | 246 ++++++++++++++++++ .../bchlib/bCHAttributesFunctionSemantics.mli | 204 ++++++++++++--- 2 files changed, 414 insertions(+), 36 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml index 0fbdccb4..06b15211 100644 --- a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml +++ b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml @@ -333,6 +333,140 @@ let get_trusted_os_cmd_fmt_string_precondition attrparams_to_string "argparams" argparams] +let string_to_relational_op (s: string): relational_op_t traceresult = + match s with + | "eq" -> Ok PEquals + | "lt" -> Ok PLessThan + | "leq" -> Ok PLessEqual + | "gt" -> Ok PGreaterThan + | "geq" -> Ok PGreaterEqual + | "neq" -> Ok PNotEqual + | _ -> Error [(elocm __LINE__) ^ "Unknown relational operator: " ^ s] + + +let get_input_format_string_precondition + (fparams: fts_parameter_t list) + (tagparams: b_attrparam_t list) + (argparams: b_attrparam_t list): xxpredicate_t traceresult = + match (tagparams, argparams) with + | ([], [AInt refindex]) -> + let* par = get_par fparams refindex in + Ok (XXInputFormatString (ArgValue par)) + | _ -> + Error [(elocm __LINE__) ^ "input_format_string params not recognized"; + fparams_to_string fparams; + attrparams_to_string "tagparams" tagparams; + attrparams_to_string "argparams" argparams] + + +let get_not_zero_precondition + (fparams: fts_parameter_t list) + (tagparams: b_attrparam_t list) + (argparams: b_attrparam_t list): xxpredicate_t traceresult = + match (tagparams, argparams) with + | ([], [AInt refindex]) -> + let* par = get_par fparams refindex in + Ok (XXNotZero (ArgValue par)) + | _ -> + Error [(elocm __LINE__) ^ "not_zero params not recognized"; + fparams_to_string fparams; + attrparams_to_string "tagparams" tagparams; + attrparams_to_string "argparams" argparams] + + +let get_non_negative_precondition + (fparams: fts_parameter_t list) + (tagparams: b_attrparam_t list) + (argparams: b_attrparam_t list): xxpredicate_t traceresult = + match (tagparams, argparams) with + | ([], [AInt refindex]) -> + let* par = get_par fparams refindex in + Ok (XXNonNegative (ArgValue par)) + | _ -> + Error [(elocm __LINE__) ^ "non_negative params not recognized"; + fparams_to_string fparams; + attrparams_to_string "tagparams" tagparams; + attrparams_to_string "argparams" argparams] + + +let get_relational_expr_precondition + (fparams: fts_parameter_t list) + (tagparams: b_attrparam_t list) + (argparams: b_attrparam_t list): xxpredicate_t traceresult = + match (tagparams, argparams) with + | ([ACons (opstr, [])], [AInt index1; AInt index2]) -> + let* op = string_to_relational_op opstr in + let* par1 = get_par fparams index1 in + let* par2 = get_par fparams index2 in + Ok (XXRelationalExpr (op, ArgValue par1, ArgValue par2)) + | _ -> + Error [(elocm __LINE__) ^ "relational_expr params not recognized"; + fparams_to_string fparams; + attrparams_to_string "tagparams" tagparams; + attrparams_to_string "argparams" argparams] + + +let get_no_overlap_precondition + (fparams: fts_parameter_t list) + (tagparams: b_attrparam_t list) + (argparams: b_attrparam_t list): xxpredicate_t traceresult = + match (tagparams, argparams) with + | ([], [AInt index1; AInt index2]) -> + let* par1 = get_par fparams index1 in + let* par2 = get_par fparams index2 in + Ok (XXNoOverlap (ArgValue par1, ArgValue par2)) + | _ -> + Error [(elocm __LINE__) ^ "no_overlap params not recognized"; + fparams_to_string fparams; + attrparams_to_string "tagparams" tagparams; + attrparams_to_string "argparams" argparams] + + +let get_allocation_base_precondition + (fparams: fts_parameter_t list) + (tagparams: b_attrparam_t list) + (argparams: b_attrparam_t list): xxpredicate_t traceresult = + match (tagparams, argparams) with + | ([], [AInt refindex]) -> + let* par = get_par fparams refindex in + Ok (XXAllocationBase (ArgValue par)) + | _ -> + Error [(elocm __LINE__) ^ "allocation_base params not recognized"; + fparams_to_string fparams; + attrparams_to_string "tagparams" tagparams; + attrparams_to_string "argparams" argparams] + + +let get_trusted_string_precondition + (fparams: fts_parameter_t list) + (tagparams: b_attrparam_t list) + (argparams: b_attrparam_t list): xxpredicate_t traceresult = + match (tagparams, argparams) with + | ([], [AInt refindex]) -> + let* par = get_par fparams refindex in + Ok (XXTrustedString (ArgValue par)) + | _ -> + Error [(elocm __LINE__) ^ "trusted_string params not recognized"; + fparams_to_string fparams; + attrparams_to_string "tagparams" tagparams; + attrparams_to_string "argparams" argparams] + + +let get_trusted_os_cmd_string_precondition + (fparams: fts_parameter_t list) + (tagparams: b_attrparam_t list) + (argparams: b_attrparam_t list): xxpredicate_t traceresult = + match (tagparams, argparams) with + | ([], [AInt refindex]) -> + let* par = get_par fparams refindex in + Ok (XXTrustedOsCmdString (ArgValue par)) + | _ -> + Error [(elocm __LINE__) ^ "trusted_os_cmd_string params not recognized"; + fparams_to_string fparams; + attrparams_to_string "tagparams" tagparams; + attrparams_to_string "argparams" argparams] + + let get_chk_pre_conditions (name: string) (fparams: fts_parameter_t list) @@ -436,6 +570,118 @@ let get_chk_pre_conditions end) (get_trusted_os_cmd_fmt_string_precondition fparams tagparams argparams) + | (ACons ("input_format_string", tagparams)) :: argparams -> + TR.tfold + ~ok:(fun xpre -> [xpre]) + ~error:(fun e -> + begin + log_error_result + ~tag:"get_chk_preconditions:input_format_string" + ~msg:name + __FILE__ __LINE__ + [String.concat ", " e]; + [] + end) + (get_input_format_string_precondition fparams tagparams argparams) + + | (ACons ("not_zero", tagparams)) :: argparams -> + TR.tfold + ~ok:(fun xpre -> [xpre]) + ~error:(fun e -> + begin + log_error_result + ~tag:"get_chk_preconditions:not_zero" + ~msg:name + __FILE__ __LINE__ + [String.concat ", " e]; + [] + end) + (get_not_zero_precondition fparams tagparams argparams) + + | (ACons ("non_negative", tagparams)) :: argparams -> + TR.tfold + ~ok:(fun xpre -> [xpre]) + ~error:(fun e -> + begin + log_error_result + ~tag:"get_chk_preconditions:non_negative" + ~msg:name + __FILE__ __LINE__ + [String.concat ", " e]; + [] + end) + (get_non_negative_precondition fparams tagparams argparams) + + | (ACons ("relational_expr", tagparams)) :: argparams -> + TR.tfold + ~ok:(fun xpre -> [xpre]) + ~error:(fun e -> + begin + log_error_result + ~tag:"get_chk_preconditions:relational_expr" + ~msg:name + __FILE__ __LINE__ + [String.concat ", " e]; + [] + end) + (get_relational_expr_precondition fparams tagparams argparams) + + | (ACons ("no_overlap", tagparams)) :: argparams -> + TR.tfold + ~ok:(fun xpre -> [xpre]) + ~error:(fun e -> + begin + log_error_result + ~tag:"get_chk_preconditions:no_overlap" + ~msg:name + __FILE__ __LINE__ + [String.concat ", " e]; + [] + end) + (get_no_overlap_precondition fparams tagparams argparams) + + | (ACons ("allocation_base", tagparams)) :: argparams -> + TR.tfold + ~ok:(fun xpre -> [xpre]) + ~error:(fun e -> + begin + log_error_result + ~tag:"get_chk_preconditions:allocation_base" + ~msg:name + __FILE__ __LINE__ + [String.concat ", " e]; + [] + end) + (get_allocation_base_precondition fparams tagparams argparams) + + | (ACons ("trusted_string", tagparams)) :: argparams -> + TR.tfold + ~ok:(fun xpre -> [xpre]) + ~error:(fun e -> + begin + log_error_result + ~tag:"get_chk_preconditions:trusted_string" + ~msg:name + __FILE__ __LINE__ + [String.concat ", " e]; + [] + end) + (get_trusted_string_precondition fparams tagparams argparams) + + | (ACons ("trusted_os_cmd_string", tagparams)) :: argparams -> + TR.tfold + ~ok:(fun xpre -> [xpre]) + ~error:(fun e -> + begin + log_error_result + ~tag:"get_chk_preconditions:trusted_os_cmd_string" + ~msg:name + __FILE__ __LINE__ + [String.concat ", " e]; + [] + end) + (get_trusted_os_cmd_string_precondition fparams tagparams argparams) + | (ACons (tag, _)) :: _ -> begin log_diagnostics_result diff --git a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.mli b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.mli index 624b45b0..4a7ac872 100644 --- a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.mli +++ b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.mli @@ -31,55 +31,187 @@ open BCHLibTypes (** {1 Function attributes} *) -(** Function declarations in C can be decorated with attributes. These attributes - are generally used to allow certain compiler optimizations - (https://gcc.gnu.org/onlinedocs/gcc/Common-Function-Attributes.html). Here - we use them to communicate preconditions about dynamically linked library - functions. +(** Function declarations in C can be decorated with attributes to communicate + preconditions, side effects, and postconditions about dynamically linked + library functions to the analyzer. - For many standard libc library functions the analyzer has comprehensive + For many standard libc library functions the analyzer has a comprehensive collection of (hand-made) function summaries that include pre- and - postconditions, side effects, etc, represented in xml. - However, binaries may of course be dynamically linked to a wide variety of - other libraries, for which it is not directly feasible to create these - summaries (e.g., because suitable binaries are not available for analysis). - One possibility is for the user to manually create the xml function summaries - for all functions of interest. A more user-friendly means of providing - similar information is through function prototypes decorated with suitable - attributes, as described here. + postconditions, side effects, etc., represented in XML. However, binaries + may be dynamically linked to a wide variety of other libraries for which + it is not feasible to create such summaries. A more user-friendly means of + providing this information is through function prototypes decorated with + suitable attributes, as described here. - We use the same syntax as presented in - (https://gcc.gnu.org/onlinedocs/gcc/Common-Function-Attributes.html). - Currently the following attributes are supported: + {2 Attribute policy} + Two categories of attributes are accepted on input. Only [chk_pre], + [chk_se], and [chk_post] are emitted in generated output headers; the + GCC compatibility attributes are read-only (see + bCHFunctionSemanticsAttributes.ml for the output path). + + {3 GCC compatibility attributes (read-only)} + + These attributes are accepted so that existing annotated system headers + (e.g., glibc) can be consumed without modification. + + {4 access} + + Syntax (GCC standard): {[ - (access (access-mode, ref-index)) - (access (access-mode, ref-index, size-index)) - (nonnull (ref-indices)) + __attribute__ ((access (access-mode, ref-index))) + __attribute__ ((access (access-mode, ref-index, size-index))) ]} - Access modes supported are [read_only], [read_write], and [write_only]; the - [ref-index] is an integer denoting the (1-based) index of the pointer - argument being accessed, and [size-index] is an integer denoting the - (1-based) index of an argument that provides a maximum size (in bytes) - for the memory region accessed. + Access modes: [read_only] -> {!XXBuffer}; [write_only] -> {!XXBlockWrite}; + [read_write] -> both. [ref-index] is the 1-based index of the pointer + argument; [size-index] is the 1-based index of the argument giving the + size in bytes. [write_only] and [read_write] also produce an + {!XXBlockWrite} side effect. - As an example, for [memcpy] this would be decorated as: + {4 nonnull} + Syntax: {[ - __attribute__ ((access (read_only, 2, 3)), - (access (write_only, 1, 3)), (nonnull (1, 2))) - void* memcpy (void *dst, const void *src, size_t len); + __attribute__ ((nonnull)) + __attribute__ ((nonnull (ref-index, ...))) + ]} + + Bare form: all pointer-typed parameters must be non-null -> {!XXNotNull} + for each. Indexed form: listed parameters must be non-null -> {!XXNotNull} + per index. + + {4 format} + + Syntax: + {[ + __attribute__ ((format (archetype, string-index, first-to-check))) + ]} + + [printf] and [gnu_printf] archetypes -> {!XXOutputFormatString} on the + format string parameter. [scanf] and [gnu_scanf] archetypes -> + {!XXInputFormatString} on the format string parameter. Other archetypes + are accepted but produce no precondition. + + {3 CodeHawk-specific attributes} + + These are the canonical forms used in hand-written CodeHawk header files + and in generated output headers. All use the [chk_pre] attribute name + with a sub-tag as the first parameter identifying the predicate kind. + + All argument indices are 1-based. Index 0 refers to the return value + (relevant for postconditions via [chk_post]). + + {4 Buffer and memory region predicates} + + {[ + __attribute__ ((chk_pre (deref_read, ref-index))) + __attribute__ ((chk_pre (deref_read, ref-index, size-index))) + __attribute__ ((chk_pre (deref_read (size), ref-index))) + __attribute__ ((chk_pre (deref_read (ntp), ref-index))) + ]} + -> {!XXBuffer}: pointer argument [ref-index] must be readable for at + least the given number of bytes ([size-index] argument, constant [size], + or up to the null terminator [ntp]). + + {[ + __attribute__ ((chk_pre (deref_write, ref-index))) + __attribute__ ((chk_pre (deref_write, ref-index, size-index))) + __attribute__ ((chk_pre (deref_write (size), ref-index))) + ]} + -> {!XXBlockWrite}: pointer argument [ref-index] must be writable for at + least the given number of bytes. + + {[ + __attribute__ ((chk_pre (initialized_range (ntp), ref-index))) + ]} + -> {!XXInitializedRange}: memory starting at [ref-index] is initialized + up to the null terminator. + + {[ + __attribute__ ((chk_pre (no_overlap, ref-index-1, ref-index-2))) + ]} + -> {!XXNoOverlap}: the memory regions pointed to by the two arguments + must not overlap. + + {4 Null and zero predicates} + + {[ + __attribute__ ((chk_pre (not_null, ref-index))) + ]} + -> {!XXNotNull}: argument must not be null. + + {[ + __attribute__ ((chk_pre (null_terminated, ref-index))) ]} + -> {!XXNullTerminated}: argument points to a null-terminated string. - (Note that the analyzer has a comprehensive function summary for memcpy, so - it is only shown here as an example, because of its familiar semantics.) + {[ + __attribute__ ((chk_pre (not_zero, ref-index))) + ]} + -> {!XXNotZero}: argument must not be zero. + + {[ + __attribute__ ((chk_pre (non_negative, ref-index))) + ]} + -> {!XXNonNegative}: argument must not be negative. + + {4 Relational predicates} + + {[ + __attribute__ ((chk_pre (relational_expr (op), ref-index-1, ref-index-2))) + ]} + -> {!XXRelationalExpr}: the two arguments satisfy the given relation. + Operators: [eq], [lt], [leq], [gt], [geq], [neq]. + + {4 Format string predicates} + + {[ + __attribute__ ((chk_pre (output_format_string, ref-index))) + ]} + -> {!XXOutputFormatString}: argument is a printf-style format string. + + {[ + __attribute__ ((chk_pre (input_format_string, ref-index))) + ]} + -> {!XXInputFormatString}: argument is a scanf-style format string. + + {4 Trusted string and allocation predicates} + + {[ + __attribute__ ((chk_pre (allocation_base, ref-index))) + ]} + -> {!XXAllocationBase}: argument is the base address of a dynamically + allocated region. + + {[ + __attribute__ ((chk_pre (trusted_string, ref-index))) + ]} + -> {!XXTrustedString}: argument is a trusted string value. + + {[ + __attribute__ ((chk_pre (trusted_os_cmd_string, ref-index))) + ]} + -> {!XXTrustedOsCmdString}: argument is safe to pass to [system(3)]. + + {[ + __attribute__ ((chk_pre (trusted_os_cmd_fmt_string (kind, size), ref-index))) + ]} + -> {!XXTrustedOsCmdFmtString}: the string constructed from this format + argument is safe to pass to [system(3)]. + + {2 Example} + + For [memcpy]: + {[ + __attribute__ ((access (read_only, 2, 3)), + (access (write_only, 1, 3)), + (nonnull (1, 2))) + void *memcpy (void *dst, const void *src, size_t len); + ]} - A prototype thus decorated will automatically generate a function interface - with the function semantics that include the corresponding preconditions - (and, in case of write_only, the corresponding side effect) for the given - library function, resulting in the appropriate proof obligations at their - call sites. + (The analyzer has a comprehensive built-in summary for [memcpy]; this + is shown only as an illustration of the attribute syntax.) *) val convert_b_attributes_to_function_conditions: From 698248fd1c1287f38a3e55821516e769bb90901c Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Tue, 9 Jun 2026 21:00:40 -0700 Subject: [PATCH 03/15] CHB: replace the XXFunctional predicate with a function qualifier --- .../bchlib/bCHAttributesFunctionSemantics.ml | 28 ++++++--- .../bchlib/bCHAttributesFunctionSemantics.mli | 5 +- CodeHawk/CHB/bchlib/bCHExternalPredicate.ml | 6 -- CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml | 57 +++++++++++++++++-- CodeHawk/CHB/bchlib/bCHFunctionSemantics.mli | 2 + CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml | 32 +++++++++-- CodeHawk/CHB/bchlib/bCHLibTypes.mli | 38 ++++++++++++- CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml | 6 +- CodeHawk/CHB/bchlib/bCHXPODictionary.ml | 1 - CodeHawk/CHB/bchlib/bCHXPOPredicate.ml | 2 - 10 files changed, 143 insertions(+), 34 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml index 06b15211..fe85afc2 100644 --- a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml +++ b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml @@ -845,28 +845,42 @@ let get_access_sideeffect let convert_b_attributes_to_function_conditions (fintf: function_interface_t) (attrs: b_attributes_t): - (xxpredicate_t list * xxpredicate_t list * xxpredicate_t list) = + (xxpredicate_t list + * xxpredicate_t list + * xxpredicate_t list + * function_qualifiers_t) = let fparameters = get_fts_parameters fintf in let name = fintf.fintf_name in + let empty_qualifiers = { + fq_noreturn = None; + fq_functional = None; + fq_sets_errno = None; + fq_must_use_return = None } in - List.fold_left (fun ((xpre, xside, xpost) as acc) attr -> + List.fold_left (fun ((xpre, xside, xpost, xqual) as acc) attr -> match attr with | Attr ("access", attrparams) -> let pre = get_access_preconditions name fparameters attrparams in let side = get_access_sideeffect name fparameters attrparams in - (pre @ xpre, side @ xside, xpost) + (pre @ xpre, side @ xside, xpost, xqual) | Attr ("nonnull", attrparams) -> let pre = get_nonnull_preconditions fparameters attrparams in - (pre @ xpre, xside, xpost) + (pre @ xpre, xside, xpost, xqual) | Attr ("format", attrparams) -> let pre = get_format_preconditions name fparameters attrparams in - (pre @ xpre, xside, xpost) + (pre @ xpre, xside, xpost, xqual) + + | Attr ("pure", []) -> + (xpre, xside, xpost, {xqual with fq_functional = Some FPure}) + + | Attr ("const", []) -> + (xpre, xside, xpost, {xqual with fq_functional = Some FConst}) | Attr ("chk_pre", attrparams) -> let pre = get_chk_pre_conditions name fparameters attrparams in - (pre @ xpre, xside, xpost) + (pre @ xpre, xside, xpost, xqual) | Attr (attrname, _) -> begin @@ -876,4 +890,4 @@ let convert_b_attributes_to_function_conditions __FILE__ __LINE__ ["attrname: " ^ attrname]; acc - end) ([], [], []) attrs + end) ([], [], [], empty_qualifiers) attrs diff --git a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.mli b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.mli index 4a7ac872..94ffc982 100644 --- a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.mli +++ b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.mli @@ -217,4 +217,7 @@ open BCHLibTypes val convert_b_attributes_to_function_conditions: function_interface_t -> b_attributes_t - -> (xxpredicate_t list * xxpredicate_t list * xxpredicate_t list) + -> (xxpredicate_t list + * xxpredicate_t list + * xxpredicate_t list + * function_qualifiers_t) diff --git a/CodeHawk/CHB/bchlib/bCHExternalPredicate.ml b/CodeHawk/CHB/bchlib/bCHExternalPredicate.ml index b89044b9..4bd65624 100644 --- a/CodeHawk/CHB/bchlib/bCHExternalPredicate.ml +++ b/CodeHawk/CHB/bchlib/bCHExternalPredicate.ml @@ -105,9 +105,6 @@ let rec xxpredicate_compare (p1: xxpredicate_t) (p2: xxpredicate_t): int = | (XXFreed t1, XXFreed t2) -> btc t1 t2 | (XXFreed _, _) -> -1 | (_, XXFreed _) -> 1 - | (XXFunctional, XXFunctional) -> 0 - | (XXFunctional, _) -> -1 - | (_, XXFunctional) -> 1 | (XXFunctionPointer (_, t1), XXFunctionPointer (_, t2)) -> btc t1 t2 | (XXFunctionPointer _, _) -> -1 | (_, XXFunctionPointer _) -> 1 @@ -234,7 +231,6 @@ let rec xxpredicate_terms (p: xxpredicate_t): bterm_t list = | XXEnum (t, _, _) -> [t] | XXFalse -> [] | XXFreed t -> [t] - | XXFunctional -> [] | XXFunctionPointer (_, t) -> [t] | XXIncludes (t, _) -> [t] | XXInitialized t -> [t] @@ -372,7 +368,6 @@ let rec xxpredicate_to_pretty (p: xxpredicate_t) = btp t; STR ": member of "; STR s; (if b then STR " (flags)" else STR "")] | XXFalse -> STR "false" | XXFreed t -> default "freed" [t] - | XXFunctional -> STR "functional" | XXFunctionPointer (ty, t) -> LBLOCK [ STR "function-pointer("; @@ -462,7 +457,6 @@ let rec modify_types_xxp | XXEnum (t, s, b) -> XXEnum (mbt t, s, b) | XXFalse -> XXFalse | XXFreed t -> XXFreed (mbt t) - | XXFunctional -> XXFunctional | XXFunctionPointer (ty, t) -> XXFunctionPointer (mt ty, mbt t) | XXIncludes (t, c) -> XXIncludes (mbt t, c) | XXInitialized t -> XXInitialized (mbt t) diff --git a/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml b/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml index a3ac8ddf..5252b362 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml @@ -195,7 +195,18 @@ let read_xml_function_semantics else []; fsem_desc = (if has "desc" then get "desc" else ""); - fsem_io_actions = io_actions + fsem_io_actions = io_actions; + fsem_qualifiers = + { fq_noreturn = + if has "noreturn" then Some true else None; + fq_functional = + if has "const" then Some FConst + else if has "pure" then Some FPure + else None; + fq_sets_errno = + if has "sets-errno" then Some true else None; + fq_must_use_return = + if has "must-use-return" then Some true else None } } @@ -240,7 +251,17 @@ let write_xml_function_semantics (if (List.length pre) > 0 then setlist "pre" pre); (if (List.length post) > 0 then setlist "post" post); (if (List.length epost) > 0 then setlist "epost" epost); - (if (List.length sidee) > 0 then setlist "sidee" sidee) + (if (List.length sidee) > 0 then setlist "sidee" sidee); + (match sem.fsem_qualifiers.fq_functional with + | Some FConst -> node#setAttribute "const" "yes" + | Some FPure -> node#setAttribute "pure" "yes" + | None -> ()); + (if sem.fsem_qualifiers.fq_noreturn = Some true then + node#setAttribute "noreturn" "yes"); + (if sem.fsem_qualifiers.fq_sets_errno = Some true then + node#setAttribute "sets-errno" "yes"); + (if sem.fsem_qualifiers.fq_must_use_return = Some true then + node#setAttribute "must-use-return" "yes") end @@ -300,11 +321,32 @@ let join_semantics fsem_postrequests = sem.fsem_postrequests @ s.fsem_postrequests; fsem_io_actions = sem.fsem_io_actions @ s.fsem_io_actions; fsem_throws = sem.fsem_throws @ s.fsem_throws; - fsem_desc = sem.fsem_desc ^ "; " ^ s.fsem_desc + fsem_desc = sem.fsem_desc ^ "; " ^ s.fsem_desc; + fsem_qualifiers = + let q1 = sem.fsem_qualifiers and q2 = s.fsem_qualifiers in + let join_bool a b = match (a, b) with + | (Some x, Some y) when x = y -> Some x + | _ -> None in + { fq_noreturn = join_bool q1.fq_noreturn q2.fq_noreturn; + fq_functional = + (match (q1.fq_functional, q2.fq_functional) with + | (Some FConst, Some FConst) -> Some FConst + | (Some _, Some _) -> Some FPure + | _ -> None); + fq_sets_errno = join_bool q1.fq_sets_errno q2.fq_sets_errno; + fq_must_use_return = join_bool q1.fq_must_use_return q2.fq_must_use_return } } | _ -> sem +let default_function_qualifiers = { + fq_noreturn = None; + fq_functional = None; + fq_sets_errno = None; + fq_must_use_return = None + } + + let default_function_semantics = { fsem_pre = []; fsem_post = []; @@ -313,14 +355,15 @@ let default_function_semantics = { fsem_postrequests = []; fsem_io_actions = []; fsem_throws = []; - fsem_desc = "" + fsem_desc = ""; + fsem_qualifiers = default_function_qualifiers } let bvarinfo_to_function_semantics (vinfo: bvarinfo_t) (fintf: function_interface_t): function_semantics_t = if (List.length vinfo.bvattr) > 0 then - let (preconditions, sideeffects, _) = + let (preconditions, sideeffects, _, qualifiers) = convert_b_attributes_to_function_conditions fintf vinfo.bvattr in let _ = log_diagnostics_result @@ -332,7 +375,9 @@ let bvarinfo_to_function_semantics "attrs: " ^ (attributes_to_string vinfo.bvattr)] in let fsem = {default_function_semantics with - fsem_pre = preconditions; fsem_sideeffects = sideeffects} in + fsem_pre = preconditions; + fsem_sideeffects = sideeffects; + fsem_qualifiers = qualifiers} in let _ = log_diagnostics_result ~tag:"bvarinfo_to_function_semantics" diff --git a/CodeHawk/CHB/bchlib/bCHFunctionSemantics.mli b/CodeHawk/CHB/bchlib/bCHFunctionSemantics.mli index e9c6ab73..94739022 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionSemantics.mli +++ b/CodeHawk/CHB/bchlib/bCHFunctionSemantics.mli @@ -40,6 +40,8 @@ open BCHLibTypes (** {1 Creation}*) +val default_function_qualifiers: function_qualifiers_t + val default_function_semantics: function_semantics_t val join_semantics: diff --git a/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml b/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml index 95b85b6d..d49700b0 100644 --- a/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml +++ b/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml @@ -88,6 +88,7 @@ object (self) val fts_parameter_value_table = mk_index_table "parameter-value-table" val function_signature_table = mk_index_table "function-signature-table" val function_interface_table = mk_index_table "function-interface-table" + val function_qualifiers_table = mk_index_table "function-qualifiers-table" val function_semantics_table = mk_index_table "function-semantics-table" val xxpredicate_table = mk_index_table "xxpredicate-table" val xxpredicate_list_table = mk_index_table "xxpredicate-list-table" @@ -117,6 +118,7 @@ object (self) fts_parameter_value_table; function_signature_table; function_interface_table; + function_qualifiers_table; function_semantics_table; xxpredicate_table; xxpredicate_list_table; @@ -459,6 +461,28 @@ object (self) fintf_bctype = if (a 6) = (-1) then None else Some (bcd#get_typ (a 6)) } + method index_function_qualifiers (fq: function_qualifiers_t) = + let ibo = function Some true -> 1 | Some false -> 0 | None -> -1 in + let ifunc = function Some FConst -> 1 | Some FPure -> 0 | None -> -1 in + let args = [ + ibo fq.fq_noreturn; + ifunc fq.fq_functional; + ibo fq.fq_sets_errno; + ibo fq.fq_must_use_return + ] in + function_qualifiers_table#add ([], args) + + method get_function_qualifiers (index: int): function_qualifiers_t = + let name = "function-qualifiers" in + let (_, args) = function_qualifiers_table#retrieve index in + let a = a name args in + let gbo = function 1 -> Some true | 0 -> Some false | _ -> None in + let gfunc = function 1 -> Some FConst | 0 -> Some FPure | _ -> None in + { fq_noreturn = gbo (a 0); + fq_functional = gfunc (a 1); + fq_sets_errno = gbo (a 2); + fq_must_use_return = gbo (a 3) } + method index_function_semantics (fsem: function_semantics_t) = let tags = [] in let args = [ @@ -466,7 +490,8 @@ object (self) self#index_xxpredicate_list fsem.fsem_post; self#index_xxpredicate_list fsem.fsem_errorpost; self#index_xxpredicate_list fsem.fsem_sideeffects; - self#index_xxpredicate_list fsem.fsem_postrequests + self#index_xxpredicate_list fsem.fsem_postrequests; + self#index_function_qualifiers fsem.fsem_qualifiers ] in function_semantics_table#add (tags, args) @@ -481,7 +506,8 @@ object (self) fsem_postrequests = self#get_xxpredicate_list (a 4); fsem_io_actions = []; fsem_desc = "id"; - fsem_throws = [] + fsem_throws = []; + fsem_qualifiers = self#get_function_qualifiers (a 5) } method index_xxpredicate (p: xxpredicate_t) = @@ -498,7 +524,6 @@ object (self) | XXEnum (t, s, b) -> (tags, [it t; bd#index_string s; ib b]) | XXFalse -> (tags, []) | XXFreed t -> (tags, [it t]) - | XXFunctional -> (tags, []) | XXFunctionPointer (ty, t) -> (tags, [ity ty; it t]) | XXIncludes (t, c) -> (tags, [it t; self#index_c_struct_constant c]) | XXInitialized t -> (tags, [it t]) @@ -562,7 +587,6 @@ object (self) | "e" -> XXEnum (gt (a 0), bd#get_string (a 1), (a 2) = 1) | "f" -> XXFalse | "fr" -> XXFreed (gt (a 0)) - | "fn" -> XXFunctional | "fp" -> XXFunctionPointer (gty (a 0), gt (a 1)) | "inc" -> XXIncludes (gt (a 0), self#get_c_struct_constant (a 1)) | "i" -> XXInitialized (gt (a 0)) diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli index 5ad87998..f4f78434 100644 --- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli +++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli @@ -2386,7 +2386,6 @@ type xxpredicate_t = | XXFalse (** always false, used as a post condition to indicate non-returning*) | XXFreed of bterm_t (** term pointed to is freed *) - | XXFunctional (** function has no observable side effects *) | XXFunctionPointer of btype_t * bterm_t (** term is pointer to a function *) | XXIncludes of bterm_t * c_struct_constant_t | XXInitialized of bterm_t (** lval denoted is initialized *) @@ -2461,6 +2460,34 @@ type io_action_t = { (** {2 Function semantics} *) +(** Purity level of a function: [FPure] means no observable side effects but + may read global or pointed-to memory (GCC [pure]); [FConst] means no side + effects and reads only direct arguments (GCC [const], strictly stronger). *) +type function_purity_t = FPure | FConst + + +(** Non-predicate qualifiers of a function: boolean or simple-enum properties + that describe function-level behavior and calling protocol, but are not + predicates over argument or return values. + + All fields use [bool option] or an enum option to allow a three-valued + interpretation: [Some v] means the property is positively documented, + [None] means unknown. + + - [fq_noreturn]: function never returns (GCC [noreturn], C23 [_Noreturn]). + - [fq_functional]: purity level — [FPure] or [FConst] (GCC [pure]/[const]). + - [fq_sets_errno]: documented to set [errno] on the error path. + - [fq_must_use_return]: caller must inspect the return value before + continuing (implied by any error postcondition; corresponds to GCC + [warn_unused_result] when consumed from third-party headers). *) +type function_qualifiers_t = { + fq_noreturn: bool option; + fq_functional: function_purity_t option; + fq_sets_errno: bool option; + fq_must_use_return: bool option +} + + (** Function semantics, combining pre- and postconditions and side effects.*) type function_semantics_t = { fsem_pre: xxpredicate_t list; @@ -2470,7 +2497,8 @@ type function_semantics_t = { fsem_sideeffects: xxpredicate_t list; fsem_io_actions: io_action_t list; fsem_desc: string; - fsem_throws: string list + fsem_throws: string list; + fsem_qualifiers: function_qualifiers_t } @@ -2607,7 +2635,6 @@ type xpo_predicate_t = | XPOEnum of xpr_t * string * bool | XPOFalse | XPOFreed of xpr_t - | XPOFunctional | XPOFunctionPointer of btype_t * xpr_t | XPOIncludes of xpr_t * c_struct_constant_t | XPOInitialized of xpr_t @@ -2867,6 +2894,11 @@ class type interface_dictionary_int = method read_xml_function_interface: ?tag:string -> xml_element_int -> function_interface_t + (** {1 Function qualifiers}*) + + method index_function_qualifiers: function_qualifiers_t -> int + method get_function_qualifiers: int -> function_qualifiers_t + (** {1 Function semantics}*) method index_function_semantics: function_semantics_t -> int diff --git a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml index 0a89b0d8..f025720f 100644 --- a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml +++ b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml @@ -432,7 +432,6 @@ object | XXEnum _ -> "e" | XXFalse -> "f" | XXFreed _ -> "fr" - | XXFunctional -> "fn" | XXFunctionPointer _ -> "fp" | XXIncludes _ -> "inc" | XXInitialized _ -> "i" @@ -466,7 +465,7 @@ object | XXConditional _ -> "con" method !tags = [ - "ab"; "b"; "bw"; "con"; "dis"; "e"; "f"; "fn"; "fp"; "fr"; "ga"; + "ab"; "b"; "bw"; "con"; "dis"; "e"; "f"; "fp"; "fr"; "ga"; "ha"; "i"; "ifs"; "inc"; "inv"; "ir"; "m"; "nm"; "nn"; "nng"; "no"; "nt"; "nu"; "nz"; "ofs"; "pos"; "sa"; "st"; "t"; "tc"; "tfa"; "tfs"; "ts"; "v"; "wfs"; "x" @@ -490,7 +489,6 @@ object | XPOEnum _ -> "e" | XPOFalse -> "f" | XPOFreed _ -> "fr" - | XPOFunctional -> "fn" | XPOFunctionPointer _ -> "fp" | XPOIncludes _ -> "inc" | XPOInitialized _ -> "i" @@ -524,7 +522,7 @@ object | XPOConditional _ -> "con" method !tags = [ - "ab"; "b"; "bw"; "con"; "dis"; "e"; "f"; "fn"; "fp"; "fr"; "ga"; + "ab"; "b"; "bw"; "con"; "dis"; "e"; "f"; "fp"; "fr"; "ga"; "ha"; "i"; "ifs"; "inc"; "inv"; "ir"; "m"; "nm"; "nn"; "nng"; "no"; "nt"; "nu"; "nz"; "ofs"; "pos"; "sa"; "st"; "t"; "tc"; "tfa"; "tfs"; "ts"; "v"; "wfs"; "x" diff --git a/CodeHawk/CHB/bchlib/bCHXPODictionary.ml b/CodeHawk/CHB/bchlib/bCHXPODictionary.ml index 478bf494..64775519 100644 --- a/CodeHawk/CHB/bchlib/bCHXPODictionary.ml +++ b/CodeHawk/CHB/bchlib/bCHXPODictionary.ml @@ -102,7 +102,6 @@ object (self) | XPOEnum (x, s, b) -> (tags, [ix x; bd#index_string s; ib b]) | XPOFalse -> (tags, []) | XPOFreed x -> (tags, [ix x]) - | XPOFunctional -> (tags, []) | XPOFunctionPointer (ty, x) -> (tags, [it ty; ix x]) | XPOIncludes (x, c) -> (tags, [ix x; id#index_c_struct_constant c]) | XPOInitialized x -> (tags, [ix x]) diff --git a/CodeHawk/CHB/bchlib/bCHXPOPredicate.ml b/CodeHawk/CHB/bchlib/bCHXPOPredicate.ml index e102add3..134ec520 100644 --- a/CodeHawk/CHB/bchlib/bCHXPOPredicate.ml +++ b/CodeHawk/CHB/bchlib/bCHXPOPredicate.ml @@ -71,7 +71,6 @@ let rec xxp_to_xpo_predicate | XXEnum (t, s, b) -> XPOEnum (btx t, s, b) | XXFalse -> XPOFalse | XXFreed t -> XPOFreed (btx t) - | XXFunctional -> XPOFunctional | XXFunctionPointer (ty, t) -> XPOFunctionPointer (ty, btx t) | XXIncludes (t, c) -> XPOIncludes (btx t, c) | XXInitialized t -> XPOInitialized (btx t) @@ -140,7 +139,6 @@ let rec xpo_predicate_to_pretty (p: xpo_predicate_t) = x2p t; STR ": member of "; STR s; (if b then STR " (flags)" else STR "")] | XPOFalse -> STR "false" | XPOFreed t -> default "freed" [t] - | XPOFunctional -> STR "functional" | XPOFunctionPointer (ty, t) -> LBLOCK [ STR "function-pointer("; From ff206f9b9fd75195950e5a0f59b31f9db076f9a3 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Tue, 9 Jun 2026 21:30:28 -0700 Subject: [PATCH 04/15] CHB: replace XXFalse predicate with noreturn qualifier --- .../bchlib/bCHAttributesFunctionSemantics.ml | 3 ++ .../bchlib/bCHAttributesFunctionSemantics.mli | 32 +++++++++++++++++++ CodeHawk/CHB/bchlib/bCHCallTargetInfo.ml | 3 +- CodeHawk/CHB/bchlib/bCHExternalPredicate.ml | 6 ---- CodeHawk/CHB/bchlib/bCHFloc.ml | 26 ++++++++------- CodeHawk/CHB/bchlib/bCHFunctionSummary.ml | 4 +-- CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml | 2 -- CodeHawk/CHB/bchlib/bCHLibTypes.mli | 3 -- CodeHawk/CHB/bchlib/bCHPostcondition.ml | 6 +--- CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml | 6 ++-- CodeHawk/CHB/bchlib/bCHXPODictionary.ml | 1 - CodeHawk/CHB/bchlib/bCHXPOPredicate.ml | 2 -- CodeHawk/CHB/bchsummaries/jni/jni_18.xml | 6 ++-- .../bchsummaries/kernel32_dll/DebugBreak.xml | 6 ++-- .../bchsummaries/kernel32_dll/ExitProcess.xml | 10 ++---- .../bchsummaries/kernel32_dll/ExitThread.xml | 10 ++---- .../kernel32_dll/FatalAppExit.xml | 6 ++-- .../kernel32_dll/FreeLibraryAndExitThread.xml | 6 ++-- .../kernel32_dll/RaiseException.xml | 10 ++---- .../msvcrt_dll/_CxxThrowException.xml | 6 ++-- .../bchsummaries/msvcrt_dll/_amsg_exit.xml | 10 ++---- .../CHB/bchsummaries/msvcrt_dll/_assert.xml | 6 ++-- .../CHB/bchsummaries/msvcrt_dll/_exit.xml | 10 ++---- .../CHB/bchsummaries/msvcrt_dll/abort.xml | 10 ++---- CodeHawk/CHB/bchsummaries/msvcrt_dll/exit.xml | 10 ++---- .../so_functions/__uClibc_main.xml | 10 ++---- .../CHB/bchsummaries/so_functions/_exit.xml | 10 ++---- .../CHB/bchsummaries/so_functions/abort.xml | 10 ++---- .../CHB/bchsummaries/so_functions/execl.xml | 6 ++-- .../CHB/bchsummaries/so_functions/exit.xml | 10 ++---- .../so_functions/pthread_exit.xml | 10 ++---- 31 files changed, 92 insertions(+), 164 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml index fe85afc2..7911b341 100644 --- a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml +++ b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml @@ -872,6 +872,9 @@ let convert_b_attributes_to_function_conditions let pre = get_format_preconditions name fparameters attrparams in (pre @ xpre, xside, xpost, xqual) + | Attr ("noreturn", []) -> + (xpre, xside, xpost, {xqual with fq_noreturn = Some true}) + | Attr ("pure", []) -> (xpre, xside, xpost, {xqual with fq_functional = Some FPure}) diff --git a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.mli b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.mli index 94ffc982..e72d6645 100644 --- a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.mli +++ b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.mli @@ -93,6 +93,38 @@ open BCHLibTypes {!XXInputFormatString} on the format string parameter. Other archetypes are accepted but produce no precondition. + {4 noreturn} + + Syntax: + {[ + __attribute__ ((noreturn)) + ]} + + Sets [fq_noreturn = Some true] in {!function_qualifiers_t}. Indicates + that the function does not return to the caller. + + {4 pure} + + Syntax: + {[ + __attribute__ ((pure)) + ]} + + Sets [fq_functional = Some FPure] in {!function_qualifiers_t}. The + function has no side effects but its return value may depend on global + state or memory passed via pointers (e.g., [strlen]). + + {4 const} + + Syntax: + {[ + __attribute__ ((const)) + ]} + + Sets [fq_functional = Some FConst] in {!function_qualifiers_t}. The + function reads only its direct arguments and has no side effects + (e.g., [abs], [sqrt]). Strictly stronger than [pure]. + {3 CodeHawk-specific attributes} These are the canonical forms used in hand-written CodeHawk header files diff --git a/CodeHawk/CHB/bchlib/bCHCallTargetInfo.ml b/CodeHawk/CHB/bchlib/bCHCallTargetInfo.ml index fda8f232..efd4a2f1 100644 --- a/CodeHawk/CHB/bchlib/bCHCallTargetInfo.ml +++ b/CodeHawk/CHB/bchlib/bCHCallTargetInfo.ml @@ -192,8 +192,7 @@ object (self) | _ -> None) None self#get_preconditions method is_nonreturning = - List.exists - (fun p -> match p with XXFalse -> true | _ -> false) sem.fsem_post + sem.fsem_qualifiers.fq_noreturn = Some true method has_sideeffects = match self#get_sideeffects with diff --git a/CodeHawk/CHB/bchlib/bCHExternalPredicate.ml b/CodeHawk/CHB/bchlib/bCHExternalPredicate.ml index 4bd65624..f857e706 100644 --- a/CodeHawk/CHB/bchlib/bCHExternalPredicate.ml +++ b/CodeHawk/CHB/bchlib/bCHExternalPredicate.ml @@ -99,9 +99,6 @@ let rec xxpredicate_compare (p1: xxpredicate_t) (p2: xxpredicate_t): int = let l0 = btc t1 t2 in if l0 = 0 then Stdlib.compare s1 s2 else l0 | (XXEnum _, _) -> -1 | (_, XXEnum _) -> 1 - | (XXFalse, XXFalse) -> 0 - | (XXFalse, _) -> -1 - | (_, XXFalse) -> 1 | (XXFreed t1, XXFreed t2) -> btc t1 t2 | (XXFreed _, _) -> -1 | (_, XXFreed _) -> 1 @@ -229,7 +226,6 @@ let rec xxpredicate_terms (p: xxpredicate_t): bterm_t list = | XXBlockWrite (_, t1, t2) -> [t1; t2] | XXBuffer (_, t1, t2) -> [t1; t2] | XXEnum (t, _, _) -> [t] - | XXFalse -> [] | XXFreed t -> [t] | XXFunctionPointer (_, t) -> [t] | XXIncludes (t, _) -> [t] @@ -366,7 +362,6 @@ let rec xxpredicate_to_pretty (p: xxpredicate_t) = | XXEnum (t, s, b) -> LBLOCK [ btp t; STR ": member of "; STR s; (if b then STR " (flags)" else STR "")] - | XXFalse -> STR "false" | XXFreed t -> default "freed" [t] | XXFunctionPointer (ty, t) -> LBLOCK [ @@ -455,7 +450,6 @@ let rec modify_types_xxp | XXBlockWrite (ty, t1, t2) -> XXBlockWrite (mt ty, mbt t1, mbt t2) | XXBuffer (ty, t1, t2) -> XXBuffer (mt ty, mbt t1, mbt t2) | XXEnum (t, s, b) -> XXEnum (mbt t, s, b) - | XXFalse -> XXFalse | XXFreed t -> XXFreed (mbt t) | XXFunctionPointer (ty, t) -> XXFunctionPointer (mt ty, mbt t) | XXIncludes (t, c) -> XXIncludes (mbt t, c) diff --git a/CodeHawk/CHB/bchlib/bCHFloc.ml b/CodeHawk/CHB/bchlib/bCHFloc.ml index 72b9eb4f..c51944dc 100644 --- a/CodeHawk/CHB/bchlib/bCHFloc.ml +++ b/CodeHawk/CHB/bchlib/bCHFloc.ml @@ -3723,18 +3723,6 @@ object (self) | XXNull term -> get_null_commands term | XXNotNull term -> get_not_null_commands term | XXRelationalExpr (op, t1, t2) -> get_post_expr_commands op t1 t2 - | XXFalse -> - let ctinfo = self#get_call_target in - if ctinfo#is_nonreturning then - [] (* was known during translation, or has been established earlier *) - else - begin - (* ctinfo#set_nonreturning; *) - chlog#add - "function retracing" - (LBLOCK [self#l#toPretty; STR ": "; STR name]); - raise Request_function_retracing - end | _ -> let msg = xxpredicate_to_pretty post in begin @@ -3747,6 +3735,20 @@ object (self) (returnvar:variable_t) (string_retriever:doubleword_int -> string option) = let name = summary#get_name in + if summary#is_nonreturning then + begin + let ctinfo = self#get_call_target in + if ctinfo#is_nonreturning then + [] (* was known during translation, or has been established earlier *) + else + begin + chlog#add + "function retracing" + (LBLOCK [self#l#toPretty; STR ": "; STR name]); + raise Request_function_retracing + end + end + else let postCommands = List.concat (List.map (fun post -> self#assert_post name post returnvar string_retriever) diff --git a/CodeHawk/CHB/bchlib/bCHFunctionSummary.ml b/CodeHawk/CHB/bchlib/bCHFunctionSummary.ml index c732b9d0..d59770fe 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionSummary.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionSummary.ml @@ -273,9 +273,7 @@ object (self:'a) sem.fsem_sideeffects method is_nonreturning = - List.exists - (fun p -> match p with XXFalse -> true | _ -> false) - sem.fsem_post + sem.fsem_qualifiers.fq_noreturn = Some true method is_jni_function = match finterface.fintf_jni_index with Some _ -> true | _ -> false diff --git a/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml b/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml index d49700b0..21cd9382 100644 --- a/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml +++ b/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml @@ -522,7 +522,6 @@ object (self) | XXBlockWrite (ty, t1, t2) -> (tags, [ity ty; it t1; it t2]) | XXBuffer (ty, t1, t2) -> (tags, [ity ty; it t1; it t2]) | XXEnum (t, s, b) -> (tags, [it t; bd#index_string s; ib b]) - | XXFalse -> (tags, []) | XXFreed t -> (tags, [it t]) | XXFunctionPointer (ty, t) -> (tags, [ity ty; it t]) | XXIncludes (t, c) -> (tags, [it t; self#index_c_struct_constant c]) @@ -585,7 +584,6 @@ object (self) | "bw" -> XXBlockWrite (gty (a 0), gt (a 1), gt (a 2)) | "b" -> XXBuffer (gty (a 0), gt (a 1), gt (a 2)) | "e" -> XXEnum (gt (a 0), bd#get_string (a 1), (a 2) = 1) - | "f" -> XXFalse | "fr" -> XXFreed (gt (a 0)) | "fp" -> XXFunctionPointer (gty (a 0), gt (a 1)) | "inc" -> XXIncludes (gt (a 0), self#get_c_struct_constant (a 1)) diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli index f4f78434..16de206d 100644 --- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli +++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli @@ -2383,8 +2383,6 @@ type xxpredicate_t = | XXEnum of bterm_t * string * bool (** term t is one of the values included in the named enumeration, if [flags] is true, the constant is a set of flags *) - | XXFalse - (** always false, used as a post condition to indicate non-returning*) | XXFreed of bterm_t (** term pointed to is freed *) | XXFunctionPointer of btype_t * bterm_t (** term is pointer to a function *) | XXIncludes of bterm_t * c_struct_constant_t @@ -2633,7 +2631,6 @@ type xpo_predicate_t = | XPOBlockWrite of btype_t * xpr_t * xpr_t | XPOBuffer of btype_t * xpr_t * xpr_t | XPOEnum of xpr_t * string * bool - | XPOFalse | XPOFreed of xpr_t | XPOFunctionPointer of btype_t * xpr_t | XPOIncludes of xpr_t * c_struct_constant_t diff --git a/CodeHawk/CHB/bchlib/bCHPostcondition.ml b/CodeHawk/CHB/bchlib/bCHPostcondition.ml index 09f45f9c..d24eaaca 100644 --- a/CodeHawk/CHB/bchlib/bCHPostcondition.ml +++ b/CodeHawk/CHB/bchlib/bCHPostcondition.ml @@ -88,7 +88,6 @@ let read_xml_postcondition | "not-null" -> XXNotNull (get_term (arg 0)) | "null-terminated" -> XXNullTerminated (get_term (arg 0)) | "enum" -> XXEnum (get_term (arg 0), pNode#getAttribute "name", false) - | "non-returning" -> XXFalse | "or" -> XXDisjunction (List.map aux pNode#getChildren) | "implies" -> let condition = @@ -106,9 +105,7 @@ let read_xml_postcondition STR "Postcondition predicate "; STR s; STR " not recognized"]) in - match (node#getTaggedChild "math")#getChild#getTag with - | "non-returning" -> XXFalse - | _ -> aux ((node#getTaggedChild "math")#getTaggedChild "apply") + aux ((node#getTaggedChild "math")#getTaggedChild "apply") let read_xml_postconditions @@ -137,7 +134,6 @@ let read_xml_shortcut_postconditions match n#getTag with | "post" | "error-post" -> (p, ep) | "enum" -> ((XXEnum (rv, n#getAttribute "name", false)):: p, ep) - | "non-returning" -> (XXFalse :: p, ep) | "null-terminated" -> ((XXNullTerminated rv) :: p, ep) | "notzero-zero" | "nonzero-zero" -> ((XXRelationalExpr (PNotEqual, rv, zero)) :: p, diff --git a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml index f025720f..ab1c725e 100644 --- a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml +++ b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml @@ -430,7 +430,6 @@ object | XXBlockWrite _ -> "bw" | XXBuffer _ -> "b" | XXEnum _ -> "e" - | XXFalse -> "f" | XXFreed _ -> "fr" | XXFunctionPointer _ -> "fp" | XXIncludes _ -> "inc" @@ -465,7 +464,7 @@ object | XXConditional _ -> "con" method !tags = [ - "ab"; "b"; "bw"; "con"; "dis"; "e"; "f"; "fp"; "fr"; "ga"; + "ab"; "b"; "bw"; "con"; "dis"; "e"; "fp"; "fr"; "ga"; "ha"; "i"; "ifs"; "inc"; "inv"; "ir"; "m"; "nm"; "nn"; "nng"; "no"; "nt"; "nu"; "nz"; "ofs"; "pos"; "sa"; "st"; "t"; "tc"; "tfa"; "tfs"; "ts"; "v"; "wfs"; "x" @@ -487,7 +486,6 @@ object | XPOBlockWrite _ -> "bw" | XPOBuffer _ -> "b" | XPOEnum _ -> "e" - | XPOFalse -> "f" | XPOFreed _ -> "fr" | XPOFunctionPointer _ -> "fp" | XPOIncludes _ -> "inc" @@ -522,7 +520,7 @@ object | XPOConditional _ -> "con" method !tags = [ - "ab"; "b"; "bw"; "con"; "dis"; "e"; "f"; "fp"; "fr"; "ga"; + "ab"; "b"; "bw"; "con"; "dis"; "e"; "fp"; "fr"; "ga"; "ha"; "i"; "ifs"; "inc"; "inv"; "ir"; "m"; "nm"; "nn"; "nng"; "no"; "nt"; "nu"; "nz"; "ofs"; "pos"; "sa"; "st"; "t"; "tc"; "tfa"; "tfs"; "ts"; "v"; "wfs"; "x" diff --git a/CodeHawk/CHB/bchlib/bCHXPODictionary.ml b/CodeHawk/CHB/bchlib/bCHXPODictionary.ml index 64775519..d7ff7135 100644 --- a/CodeHawk/CHB/bchlib/bCHXPODictionary.ml +++ b/CodeHawk/CHB/bchlib/bCHXPODictionary.ml @@ -100,7 +100,6 @@ object (self) | XPOBlockWrite (ty, x1, x2) -> (tags, [it ty; ix x1; ix x2]) | XPOBuffer (ty, x1, x2) -> (tags, [it ty; ix x1; ix x2]) | XPOEnum (x, s, b) -> (tags, [ix x; bd#index_string s; ib b]) - | XPOFalse -> (tags, []) | XPOFreed x -> (tags, [ix x]) | XPOFunctionPointer (ty, x) -> (tags, [it ty; ix x]) | XPOIncludes (x, c) -> (tags, [ix x; id#index_c_struct_constant c]) diff --git a/CodeHawk/CHB/bchlib/bCHXPOPredicate.ml b/CodeHawk/CHB/bchlib/bCHXPOPredicate.ml index 134ec520..cf6e0fec 100644 --- a/CodeHawk/CHB/bchlib/bCHXPOPredicate.ml +++ b/CodeHawk/CHB/bchlib/bCHXPOPredicate.ml @@ -69,7 +69,6 @@ let rec xxp_to_xpo_predicate | XXBlockWrite (ty, t1, t2) -> XPOBlockWrite (ty, btx t1, btx t2) | XXBuffer (ty, t1, t2) -> XPOBuffer (ty, btx t1, btx t2) | XXEnum (t, s, b) -> XPOEnum (btx t, s, b) - | XXFalse -> XPOFalse | XXFreed t -> XPOFreed (btx t) | XXFunctionPointer (ty, t) -> XPOFunctionPointer (ty, btx t) | XXIncludes (t, c) -> XPOIncludes (btx t, c) @@ -137,7 +136,6 @@ let rec xpo_predicate_to_pretty (p: xpo_predicate_t) = | XPOEnum (t, s, b) -> LBLOCK [ x2p t; STR ": member of "; STR s; (if b then STR " (flags)" else STR "")] - | XPOFalse -> STR "false" | XPOFreed t -> default "freed" [t] | XPOFunctionPointer (ty, t) -> LBLOCK [ diff --git a/CodeHawk/CHB/bchsummaries/jni/jni_18.xml b/CodeHawk/CHB/bchsummaries/jni/jni_18.xml index ebde2fe9..6b24e258 100644 --- a/CodeHawk/CHB/bchsummaries/jni/jni_18.xml +++ b/CodeHawk/CHB/bchsummaries/jni/jni_18.xml @@ -42,14 +42,12 @@ void - + - - - + diff --git a/CodeHawk/CHB/bchsummaries/kernel32_dll/DebugBreak.xml b/CodeHawk/CHB/bchsummaries/kernel32_dll/DebugBreak.xml index 55ffccac..5fa7eb08 100644 --- a/CodeHawk/CHB/bchsummaries/kernel32_dll/DebugBreak.xml +++ b/CodeHawk/CHB/bchsummaries/kernel32_dll/DebugBreak.xml @@ -21,14 +21,12 @@ - + - - - + diff --git a/CodeHawk/CHB/bchsummaries/kernel32_dll/ExitProcess.xml b/CodeHawk/CHB/bchsummaries/kernel32_dll/ExitProcess.xml index 5e3718a8..f30355b2 100644 --- a/CodeHawk/CHB/bchsummaries/kernel32_dll/ExitProcess.xml +++ b/CodeHawk/CHB/bchsummaries/kernel32_dll/ExitProcess.xml @@ -19,18 +19,12 @@ - + - - - - - - - + diff --git a/CodeHawk/CHB/bchsummaries/kernel32_dll/ExitThread.xml b/CodeHawk/CHB/bchsummaries/kernel32_dll/ExitThread.xml index 2d65be79..49d7336f 100644 --- a/CodeHawk/CHB/bchsummaries/kernel32_dll/ExitThread.xml +++ b/CodeHawk/CHB/bchsummaries/kernel32_dll/ExitThread.xml @@ -19,18 +19,12 @@ - + - - - - - - - + diff --git a/CodeHawk/CHB/bchsummaries/kernel32_dll/FatalAppExit.xml b/CodeHawk/CHB/bchsummaries/kernel32_dll/FatalAppExit.xml index 03dd70c8..2300a2a7 100644 --- a/CodeHawk/CHB/bchsummaries/kernel32_dll/FatalAppExit.xml +++ b/CodeHawk/CHB/bchsummaries/kernel32_dll/FatalAppExit.xml @@ -33,15 +33,13 @@ - + - - - + diff --git a/CodeHawk/CHB/bchsummaries/kernel32_dll/FreeLibraryAndExitThread.xml b/CodeHawk/CHB/bchsummaries/kernel32_dll/FreeLibraryAndExitThread.xml index 87fd62ae..16145e5f 100644 --- a/CodeHawk/CHB/bchsummaries/kernel32_dll/FreeLibraryAndExitThread.xml +++ b/CodeHawk/CHB/bchsummaries/kernel32_dll/FreeLibraryAndExitThread.xml @@ -42,15 +42,13 @@ VOID - + - - - + diff --git a/CodeHawk/CHB/bchsummaries/kernel32_dll/RaiseException.xml b/CodeHawk/CHB/bchsummaries/kernel32_dll/RaiseException.xml index cabb401a..e221fc93 100644 --- a/CodeHawk/CHB/bchsummaries/kernel32_dll/RaiseException.xml +++ b/CodeHawk/CHB/bchsummaries/kernel32_dll/RaiseException.xml @@ -47,7 +47,7 @@ - + @@ -63,13 +63,7 @@ - - - - - - - + diff --git a/CodeHawk/CHB/bchsummaries/msvcrt_dll/_CxxThrowException.xml b/CodeHawk/CHB/bchsummaries/msvcrt_dll/_CxxThrowException.xml index ae6c34a6..3e86a328 100644 --- a/CodeHawk/CHB/bchsummaries/msvcrt_dll/_CxxThrowException.xml +++ b/CodeHawk/CHB/bchsummaries/msvcrt_dll/_CxxThrowException.xml @@ -34,14 +34,12 @@ void - + - - - + diff --git a/CodeHawk/CHB/bchsummaries/msvcrt_dll/_amsg_exit.xml b/CodeHawk/CHB/bchsummaries/msvcrt_dll/_amsg_exit.xml index 9fb1ded9..3dfef7cd 100644 --- a/CodeHawk/CHB/bchsummaries/msvcrt_dll/_amsg_exit.xml +++ b/CodeHawk/CHB/bchsummaries/msvcrt_dll/_amsg_exit.xml @@ -22,15 +22,9 @@ int - + - - - - - - - + diff --git a/CodeHawk/CHB/bchsummaries/msvcrt_dll/_assert.xml b/CodeHawk/CHB/bchsummaries/msvcrt_dll/_assert.xml index a3a0240c..0e06f051 100644 --- a/CodeHawk/CHB/bchsummaries/msvcrt_dll/_assert.xml +++ b/CodeHawk/CHB/bchsummaries/msvcrt_dll/_assert.xml @@ -39,14 +39,12 @@ void - + - - - + diff --git a/CodeHawk/CHB/bchsummaries/msvcrt_dll/_exit.xml b/CodeHawk/CHB/bchsummaries/msvcrt_dll/_exit.xml index b087a519..65493217 100644 --- a/CodeHawk/CHB/bchsummaries/msvcrt_dll/_exit.xml +++ b/CodeHawk/CHB/bchsummaries/msvcrt_dll/_exit.xml @@ -19,19 +19,13 @@ - + - - - - - - - + diff --git a/CodeHawk/CHB/bchsummaries/msvcrt_dll/abort.xml b/CodeHawk/CHB/bchsummaries/msvcrt_dll/abort.xml index b48ca69d..26582b2f 100644 --- a/CodeHawk/CHB/bchsummaries/msvcrt_dll/abort.xml +++ b/CodeHawk/CHB/bchsummaries/msvcrt_dll/abort.xml @@ -15,18 +15,12 @@ void - + - - - - - - - + diff --git a/CodeHawk/CHB/bchsummaries/msvcrt_dll/exit.xml b/CodeHawk/CHB/bchsummaries/msvcrt_dll/exit.xml index c0f4adad..42f28be9 100644 --- a/CodeHawk/CHB/bchsummaries/msvcrt_dll/exit.xml +++ b/CodeHawk/CHB/bchsummaries/msvcrt_dll/exit.xml @@ -19,20 +19,14 @@ - + - - - - - - - + diff --git a/CodeHawk/CHB/bchsummaries/so_functions/__uClibc_main.xml b/CodeHawk/CHB/bchsummaries/so_functions/__uClibc_main.xml index 35882f38..6a53ea70 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/__uClibc_main.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/__uClibc_main.xml @@ -51,16 +51,10 @@ void - + - - - - - - - + diff --git a/CodeHawk/CHB/bchsummaries/so_functions/_exit.xml b/CodeHawk/CHB/bchsummaries/so_functions/_exit.xml index 2eb16807..ec9ecde7 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/_exit.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/_exit.xml @@ -19,19 +19,13 @@ - + - - - - - - - + diff --git a/CodeHawk/CHB/bchsummaries/so_functions/abort.xml b/CodeHawk/CHB/bchsummaries/so_functions/abort.xml index a15618e2..ec07bb62 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/abort.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/abort.xml @@ -13,20 +13,14 @@ void - + - - - - - - - + diff --git a/CodeHawk/CHB/bchsummaries/so_functions/execl.xml b/CodeHawk/CHB/bchsummaries/so_functions/execl.xml index 88fc5471..1e0c0014 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/execl.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/execl.xml @@ -34,12 +34,10 @@ int - + - - - + diff --git a/CodeHawk/CHB/bchsummaries/so_functions/exit.xml b/CodeHawk/CHB/bchsummaries/so_functions/exit.xml index 922592e1..d5b68a5a 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/exit.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/exit.xml @@ -19,20 +19,14 @@ - + - - - - - - - + diff --git a/CodeHawk/CHB/bchsummaries/so_functions/pthread_exit.xml b/CodeHawk/CHB/bchsummaries/so_functions/pthread_exit.xml index 7e4e99d1..f2867b27 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/pthread_exit.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/pthread_exit.xml @@ -20,20 +20,14 @@ void - + - - - - - - - + From 008dafa99d981a5400b9f0e18223920f14092e9f Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Tue, 9 Jun 2026 21:47:27 -0700 Subject: [PATCH 05/15] CHB: add support for input of function qualifiers via attributes --- .../bchlib/bCHAttributesFunctionSemantics.ml | 38 +++++++++++++++++++ .../bchlib/bCHAttributesFunctionSemantics.mli | 34 +++++++++++++++++ 2 files changed, 72 insertions(+) diff --git a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml index 7911b341..504fcedd 100644 --- a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml +++ b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml @@ -842,6 +842,38 @@ let get_access_sideeffect end +let get_chk_qual_conditions + (name: string) + (attrparams: b_attrparam_t list) + (xqual: function_qualifiers_t): function_qualifiers_t = + match attrparams with + | [ACons ("sets_errno", [])] -> + {xqual with fq_sets_errno = Some true} + + | [ACons ("must_use_return", [])] -> + {xqual with fq_must_use_return = Some true} + + | (ACons (tag, _)) :: _ -> + begin + log_diagnostics_result + ~tag:"get_chk_qual_conditions:tag not recognized" + ~msg:name + __FILE__ __LINE__ + ["tag: " ^ tag]; + xqual + end + + | _ -> + begin + log_diagnostics_result + ~tag:"get_chk_qual_conditions:not recognized" + ~msg:name + __FILE__ __LINE__ + [attrparams_to_string "attrparams" attrparams]; + xqual + end + + let convert_b_attributes_to_function_conditions (fintf: function_interface_t) (attrs: b_attributes_t): @@ -881,10 +913,16 @@ let convert_b_attributes_to_function_conditions | Attr ("const", []) -> (xpre, xside, xpost, {xqual with fq_functional = Some FConst}) + | Attr ("warn_unused_result", []) -> + (xpre, xside, xpost, {xqual with fq_must_use_return = Some true}) + | Attr ("chk_pre", attrparams) -> let pre = get_chk_pre_conditions name fparameters attrparams in (pre @ xpre, xside, xpost, xqual) + | Attr ("chk_qual", attrparams) -> + (xpre, xside, xpost, get_chk_qual_conditions name attrparams xqual) + | Attr (attrname, _) -> begin log_diagnostics_result diff --git a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.mli b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.mli index e72d6645..6da23c81 100644 --- a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.mli +++ b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.mli @@ -125,6 +125,17 @@ open BCHLibTypes function reads only its direct arguments and has no side effects (e.g., [abs], [sqrt]). Strictly stronger than [pure]. + {4 warn_unused_result} + + Syntax: + {[ + __attribute__ ((warn_unused_result)) + ]} + + Sets [fq_must_use_return = Some true] in {!function_qualifiers_t}. The + caller is obligated to inspect the return value. Equivalent to + [chk_qual(must_use_return)] for headers that use the GCC standard form. + {3 CodeHawk-specific attributes} These are the canonical forms used in hand-written CodeHawk header files @@ -232,6 +243,29 @@ open BCHLibTypes -> {!XXTrustedOsCmdFmtString}: the string constructed from this format argument is safe to pass to [system(3)]. + {3 chk_qual: CodeHawk function qualifiers} + + These are the canonical forms for non-predicate function properties that + have no GCC-standard attribute equivalent. Unlike [chk_pre] (preconditions) + and [chk_se] (side effects), [chk_qual] qualifiers carry no argument + indices — they are properties of the function itself. + + {[ + __attribute__ ((chk_qual (sets_errno))) + ]} + Sets [fq_sets_errno = Some true] in {!function_qualifiers_t}. The function + sets [errno] to indicate the specific error when it fails. This is a + property documented in the C standard and POSIX, distinct from any + observable memory side effect. + + {[ + __attribute__ ((chk_qual (must_use_return))) + ]} + Sets [fq_must_use_return = Some true] in {!function_qualifiers_t}. The + caller is obligated to inspect the return value (e.g., to check for an + error code). Implied by the presence of an error-postcondition in a + function summary; provided here for use in hand-written CodeHawk headers. + {2 Example} For [memcpy]: From c4e13b06042508c8fb1403868151b76384867e9e Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Tue, 9 Jun 2026 22:17:56 -0700 Subject: [PATCH 06/15] CHB: replace the XXSetsErrno predicate with a function qualifier --- CodeHawk/CHB/bchcmdline/bCHXMakeLibSummary.ml | 14 ++------------ CodeHawk/CHB/bchlib/bCHExternalPredicate.ml | 6 ------ CodeHawk/CHB/bchlib/bCHFunctionSummary.ml | 3 +-- CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml | 2 -- CodeHawk/CHB/bchlib/bCHLibTypes.mli | 2 -- CodeHawk/CHB/bchlib/bCHSideeffect.ml | 6 +----- CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml | 2 -- CodeHawk/CHB/bchlib/bCHXPODictionary.ml | 1 - CodeHawk/CHB/bchlib/bCHXPOPredicate.ml | 2 -- CodeHawk/CHB/bchsummaries/msvcrt_dll/_fileno.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/msvcrt_dll/_setmode.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/msvcrt_dll/fgets.xml | 7 +------ CodeHawk/CHB/bchsummaries/msvcrt_dll/fputc.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/msvcrt_dll/fread.xml | 7 +------ CodeHawk/CHB/bchsummaries/msvcrt_dll/ftell.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/msvcrt_dll/gmtime.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/msvcrt_dll/localtime.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/msvcrt_dll/signal.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/msvcrt_dll/strtol.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/msvcrt_dll/strtoul.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/msvcrt_dll/strxfrm.xml | 7 +------ CodeHawk/CHB/bchsummaries/msvcrt_dll/vfprintf.xml | 10 ++-------- .../bchsummaries/so_functions/__fgetc_unlocked.xml | 10 ++-------- .../bchsummaries/so_functions/__fputc_unlocked.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/accept.xml | 7 +------ CodeHawk/CHB/bchsummaries/so_functions/access.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/bind.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/chmod.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/chown.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/chroot.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/close.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/closedir.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/connect.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/fdopen.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/fgetc.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/fgets.xml | 7 +------ CodeHawk/CHB/bchsummaries/so_functions/fileno.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/flock.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/fopen.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/fopen64.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/fputc.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/fputs.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/fread.xml | 7 +------ .../CHB/bchsummaries/so_functions/freeaddrinfo.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/fseek.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/fstat.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/fstat64.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/ftell.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/ftruncate.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/ftruncate64.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/fwrite.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/getaddrinfo.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/getcwd.xml | 7 +------ .../CHB/bchsummaries/so_functions/getgrgid.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/getgrnam.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/getgroups.xml | 7 +------ .../bchsummaries/so_functions/gethostbyname.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/getline.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/getpeername.xml | 7 +------ .../CHB/bchsummaries/so_functions/getpriority.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/getpwnam.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/getrlimit.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/getrlimit64.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/getrusage.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/getsockname.xml | 7 +------ .../CHB/bchsummaries/so_functions/getsockopt.xml | 7 +------ .../CHB/bchsummaries/so_functions/getspnam.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/gmtime.xml | 10 ++-------- .../bchsummaries/so_functions/if_indextoname.xml | 7 +------ .../CHB/bchsummaries/so_functions/inet_ntop.xml | 7 +------ .../CHB/bchsummaries/so_functions/inet_pton.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/ioctl.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/kill.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/killpg.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/listen.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/localtime.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/lockf.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/lockf64.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/lseek.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/lseek64.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/malloc.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/mkdir.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/mkstemp.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/mkstemp64.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/mktime.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/mmap.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/mmap64.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/msgrcv.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/munmap.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/nanosleep.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/open.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/open64.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/opendir.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/pclose.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/pipe.xml | 7 +------ CodeHawk/CHB/bchsummaries/so_functions/poll.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/popen.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/putenv.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/puts.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/read.xml | 7 +------ CodeHawk/CHB/bchsummaries/so_functions/readdir.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/readdir64.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/readlink.xml | 7 +------ .../CHB/bchsummaries/so_functions/realpath.xml | 7 +------ CodeHawk/CHB/bchsummaries/so_functions/recv.xml | 7 +------ .../CHB/bchsummaries/so_functions/recvfrom.xml | 7 +------ CodeHawk/CHB/bchsummaries/so_functions/recvmsg.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/remove.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/rename.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/rewind.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/rmdir.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/select.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/sem_init.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/sem_post.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/sem_wait.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/send.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/sendmsg.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/sendto.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/setegid.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/setenv.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/seteuid.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/setgid.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/sethostname.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/setpgid.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/setpriority.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/setrlimit.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/setrlimit64.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/setsid.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/setsockopt.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/settimeofday.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/setuid.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/shutdown.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/sigaction.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/sigaddset.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/sigemptyset.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/sigprocmask.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/socket.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/socketpair.xml | 7 +------ CodeHawk/CHB/bchsummaries/so_functions/sscanf.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/stat.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/stat64.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/statfs.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/statfs64.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/strdup.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/strtoll.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/strtoul.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/strtoull.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/sysinfo.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/system.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/tcflush.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/tcgetattr.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/tcsetattr.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/tempnam.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/time.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/times.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/unlink.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/usleep.xml | 10 ++-------- .../CHB/bchsummaries/so_functions/vfprintf.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/wait.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/wait4.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/waitpid.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/write.xml | 10 ++-------- CodeHawk/CHB/bchsummaries/so_functions/writev.xml | 10 ++-------- .../CHB/bchsummaries/ws2_32_dll/gethostname.xml | 3 +-- 164 files changed, 293 insertions(+), 1228 deletions(-) diff --git a/CodeHawk/CHB/bchcmdline/bCHXMakeLibSummary.ml b/CodeHawk/CHB/bchcmdline/bCHXMakeLibSummary.ml index 746394a3..89d8bbec 100644 --- a/CodeHawk/CHB/bchcmdline/bCHXMakeLibSummary.ml +++ b/CodeHawk/CHB/bchcmdline/bCHXMakeLibSummary.ml @@ -173,18 +173,7 @@ let write_xml_postconditions (node:xml_element_int) = begin pNode#setAttribute "name" p; pNode :: acc end) pNodes !enumpost in append pNodes -let write_xml_sideeffects (node:xml_element_int) = - if !sets_errno then - let sNode = xmlElement "sideeffect" in - let mNode = xmlElement "math" in - let eNode = xmlElement "sets-errno" in - begin - sNode#appendChildren [mNode]; - mNode#appendChildren [eNode]; - node#appendChildren [sNode] - end - else - () +let write_xml_sideeffects (_node:xml_element_int) = () let write_xml_io_actions (node:xml_element_int) _parameters = if !iox_cat = "" then () else @@ -216,6 +205,7 @@ let write_xml_summary (node:xml_element_int) parameters = begin write_xml_doc docNode parameters; write_xml_api apiNode parameters; + (if !sets_errno then semNode#setAttribute "sets-errno" "yes"); write_xml_sem semNode parameters; append [docNode; apiNode; semNode] end diff --git a/CodeHawk/CHB/bchlib/bCHExternalPredicate.ml b/CodeHawk/CHB/bchlib/bCHExternalPredicate.ml index f857e706..1f4820d8 100644 --- a/CodeHawk/CHB/bchlib/bCHExternalPredicate.ml +++ b/CodeHawk/CHB/bchlib/bCHExternalPredicate.ml @@ -172,9 +172,6 @@ let rec xxpredicate_compare (p1: xxpredicate_t) (p2: xxpredicate_t): int = l0 | (XXRelationalExpr _, _) -> -1 | (_, XXRelationalExpr _) -> 1 - | (XXSetsErrno, XXSetsErrno) -> 0 - | (XXSetsErrno, _) -> -1 - | (_, XXSetsErrno) -> 1 | (XXStartsThread (t1, tl1), XXStartsThread (t2, tl2)) -> let l0 = btc t1 t2 in if l0 = 0 then list_compare tl1 tl2 btc else l0 | (XXStartsThread _, _) -> -1 @@ -247,7 +244,6 @@ let rec xxpredicate_terms (p: xxpredicate_t): bterm_t list = | XXOutputFormatString t -> [t] | XXPositive t -> [t] | XXRelationalExpr (_, t1, t2) -> [t1; t2] - | XXSetsErrno -> [] | XXStartsThread (t, tt) -> t :: tt | XXTainted t -> [t] | XXTrustedString t -> [t] @@ -399,7 +395,6 @@ let rec xxpredicate_to_pretty (p: xxpredicate_t) = | XXPositive t -> default "positive" [t] | XXRelationalExpr (op, t1, t2) -> LBLOCK [btp t1; STR (relational_op_to_string op); btp t2] - | XXSetsErrno -> STR "sets errno" | XXStartsThread (t, tt) -> default "starts-thread" (t :: tt) | XXTainted t -> default "tainted" [t] | XXTrustedString t -> default "trusted-string" [t] @@ -471,7 +466,6 @@ let rec modify_types_xxp | XXNullTerminated t -> XXNullTerminated (mbt t) | XXOutputFormatString t -> XXOutputFormatString (mbt t) | XXRelationalExpr (op, t1, t2) -> XXRelationalExpr (op, mbt t1, mbt t2) - | XXSetsErrno -> XXSetsErrno | XXStartsThread (t, tt) -> XXStartsThread (mbt t, List.map mbt tt) | XXTainted t -> XXTainted (mbt t) | XXTrustedString t -> XXTrustedString (mbt t) diff --git a/CodeHawk/CHB/bchlib/bCHFunctionSummary.ml b/CodeHawk/CHB/bchlib/bCHFunctionSummary.ml index d59770fe..5692bb51 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionSummary.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionSummary.ml @@ -269,8 +269,7 @@ object (self:'a) sem.fsem_sideeffects method sets_errno = - List.exists (fun p -> match p with XXSetsErrno -> true | _ -> false) - sem.fsem_sideeffects + sem.fsem_qualifiers.fq_sets_errno = Some true method is_nonreturning = sem.fsem_qualifiers.fq_noreturn = Some true diff --git a/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml b/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml index 21cd9382..e6f07e79 100644 --- a/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml +++ b/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml @@ -544,7 +544,6 @@ object (self) | XXPositive t -> (tags, [it t]) | XXRelationalExpr (op, t1, t2) -> (tags @ [relational_op_mfts#ts op], [it t1; it t2]) - | XXSetsErrno -> (tags, []) | XXStartsThread (t, tl) -> (tags, List.map it (t::tl)) | XXTainted t -> (tags, [it t]) | XXTrustedString t -> (tags, [it t]) @@ -605,7 +604,6 @@ object (self) | "ofs" -> XXOutputFormatString (gt (a 0)) | "pos" -> XXPositive (gt (a 0)) | "x" -> XXRelationalExpr (relational_op_mfts#fs (t 1), gt (a 0), gt (a 1)) - | "errno" -> XXSetsErrno | "st" -> XXStartsThread (gt (a 0), List.map gt (List.tl args)) | "t" -> XXTainted (gt (a 0)) | "tc" -> XXTrustedOsCmdString (gt (a 0)) diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli index 16de206d..799f4801 100644 --- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli +++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli @@ -2414,7 +2414,6 @@ type xxpredicate_t = | XXRelationalExpr of relational_op_t * bterm_t * bterm_t (** relational expression *) - | XXSetsErrno | XXStartsThread of bterm_t * bterm_t list (** starts a thread with [t1] as start address and the remaining terms as parameters *) @@ -2652,7 +2651,6 @@ type xpo_predicate_t = | XPONullTerminated of xpr_t | XPOOutputFormatString of xpr_t | XPORelationalExpr of relational_op_t * xpr_t * xpr_t - | XPOSetsErrno | XPOStartsThread of xpr_t * xpr_t list | XPOTainted of xpr_t | XPOTrustedString of xpr_t diff --git a/CodeHawk/CHB/bchlib/bCHSideeffect.ml b/CodeHawk/CHB/bchlib/bCHSideeffect.ml index 20b3a7f2..f8815540 100644 --- a/CodeHawk/CHB/bchlib/bCHSideeffect.ml +++ b/CodeHawk/CHB/bchlib/bCHSideeffect.ml @@ -151,7 +151,6 @@ let read_xml_sideeffect | "starts-thread" -> XXStartsThread (get_term (arg 0), List.map get_term (List.tl argNodes)) | "invalidates" -> XXInvalidated (get_term (arg 0)) - | "sets-errno" -> XXSetsErrno | "implies" -> let condition = List.hd @@ -185,10 +184,7 @@ let read_xml_sideeffect STR "Sideeffect predicate "; STR s; STR " not recognized"]) in - match (node#getTaggedChild "math")#getChild#getTag with - | "sets-errno" -> XXSetsErrno - (* | "unknown-sideeffect" -> UnknownSideeffect *) - | _ -> aux ((node#getTaggedChild "math")#getTaggedChild "apply") + aux ((node#getTaggedChild "math")#getTaggedChild "apply") let read_xml_sideeffects diff --git a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml index ab1c725e..7ea171b4 100644 --- a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml +++ b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml @@ -451,7 +451,6 @@ object | XXNullTerminated _ -> "nt" | XXOutputFormatString _ -> "ofs" | XXRelationalExpr _ -> "x" - | XXSetsErrno -> "errno" | XXStartsThread _ -> "st" | XXTainted _ -> "t" | XXTrustedString _ -> "ts" @@ -507,7 +506,6 @@ object | XPONullTerminated _ -> "nt" | XPOOutputFormatString _ -> "ofs" | XPORelationalExpr _ -> "x" - | XPOSetsErrno -> "errno" | XPOStartsThread _ -> "st" | XPOTainted _ -> "t" | XPOTrustedString _ -> "ts" diff --git a/CodeHawk/CHB/bchlib/bCHXPODictionary.ml b/CodeHawk/CHB/bchlib/bCHXPODictionary.ml index d7ff7135..94149ec7 100644 --- a/CodeHawk/CHB/bchlib/bCHXPODictionary.ml +++ b/CodeHawk/CHB/bchlib/bCHXPODictionary.ml @@ -122,7 +122,6 @@ object (self) | XPOOutputFormatString x -> (tags, [ix x]) | XPORelationalExpr (op, x1, x2) -> (tags @ [relational_op_mfts#ts op], [ix x1; ix x2]) - | XPOSetsErrno -> (tags, []) | XPOStartsThread (x, xl) -> (tags, (ix x) :: (List.map ix xl)) | XPOTainted x -> (tags, [ix x]) | XPOTrustedString x -> (tags, [ix x]) diff --git a/CodeHawk/CHB/bchlib/bCHXPOPredicate.ml b/CodeHawk/CHB/bchlib/bCHXPOPredicate.ml index cf6e0fec..23df214f 100644 --- a/CodeHawk/CHB/bchlib/bCHXPOPredicate.ml +++ b/CodeHawk/CHB/bchlib/bCHXPOPredicate.ml @@ -90,7 +90,6 @@ let rec xxp_to_xpo_predicate | XXNullTerminated t -> XPONullTerminated (btx t) | XXOutputFormatString t -> XPOOutputFormatString (btx t) | XXRelationalExpr (op, t1, t2) -> XPORelationalExpr (op, btx t1, btx t2) - | XXSetsErrno -> XPOSetsErrno | XXStartsThread (t1, t2) -> XPOStartsThread (btx t1, List.map btx t2) | XXTainted t -> XPOTainted (btx t) | XXTrustedString t -> XPOTrustedString (btx t) @@ -173,7 +172,6 @@ let rec xpo_predicate_to_pretty (p: xpo_predicate_t) = | XPOPositive t -> default "positive" [t] | XPORelationalExpr (op, t1, t2) -> LBLOCK [x2p t1; STR (relational_op_to_string op); x2p t2] - | XPOSetsErrno -> STR "sets errno" | XPOStartsThread (t, tt) -> default "starts-thread" (t :: tt) | XPOTainted t -> default "tainted" [t] | XPOTrustedString t -> default "trusted-string" [t] diff --git a/CodeHawk/CHB/bchsummaries/msvcrt_dll/_fileno.xml b/CodeHawk/CHB/bchsummaries/msvcrt_dll/_fileno.xml index c5339cfe..4aefa6f5 100644 --- a/CodeHawk/CHB/bchsummaries/msvcrt_dll/_fileno.xml +++ b/CodeHawk/CHB/bchsummaries/msvcrt_dll/_fileno.xml @@ -24,7 +24,7 @@ - + @@ -32,13 +32,7 @@ - - - - - - - + Copyright 2012-2015, Kestrel Technology LLC, Palo Alto, CA 94304 diff --git a/CodeHawk/CHB/bchsummaries/msvcrt_dll/_setmode.xml b/CodeHawk/CHB/bchsummaries/msvcrt_dll/_setmode.xml index 30955106..1b628e0c 100644 --- a/CodeHawk/CHB/bchsummaries/msvcrt_dll/_setmode.xml +++ b/CodeHawk/CHB/bchsummaries/msvcrt_dll/_setmode.xml @@ -27,19 +27,13 @@ int - + - - - - - - - + Copyright 2012-2016, Kestrel Technology LLC, Palo Alto, CA 94304 diff --git a/CodeHawk/CHB/bchsummaries/msvcrt_dll/fgets.xml b/CodeHawk/CHB/bchsummaries/msvcrt_dll/fgets.xml index 1c86922b..c73d2929 100644 --- a/CodeHawk/CHB/bchsummaries/msvcrt_dll/fgets.xml +++ b/CodeHawk/CHB/bchsummaries/msvcrt_dll/fgets.xml @@ -56,7 +56,7 @@
- + @@ -110,11 +110,6 @@ - - - - - diff --git a/CodeHawk/CHB/bchsummaries/msvcrt_dll/fputc.xml b/CodeHawk/CHB/bchsummaries/msvcrt_dll/fputc.xml index 149c5f95..f3a41928 100644 --- a/CodeHawk/CHB/bchsummaries/msvcrt_dll/fputc.xml +++ b/CodeHawk/CHB/bchsummaries/msvcrt_dll/fputc.xml @@ -31,7 +31,7 @@
- + @@ -39,13 +39,7 @@ - - - - - - - + Copyright 2012-2016, Kestrel Technology LLC, Palo Alto, CA 94304 diff --git a/CodeHawk/CHB/bchsummaries/msvcrt_dll/fread.xml b/CodeHawk/CHB/bchsummaries/msvcrt_dll/fread.xml index 9ee93ae3..602518bf 100644 --- a/CodeHawk/CHB/bchsummaries/msvcrt_dll/fread.xml +++ b/CodeHawk/CHB/bchsummaries/msvcrt_dll/fread.xml @@ -48,7 +48,7 @@
- + @@ -99,11 +99,6 @@ - - - - - diff --git a/CodeHawk/CHB/bchsummaries/msvcrt_dll/ftell.xml b/CodeHawk/CHB/bchsummaries/msvcrt_dll/ftell.xml index ac644668..7d31037c 100644 --- a/CodeHawk/CHB/bchsummaries/msvcrt_dll/ftell.xml +++ b/CodeHawk/CHB/bchsummaries/msvcrt_dll/ftell.xml @@ -24,7 +24,7 @@ - + @@ -33,13 +33,7 @@ - - - - - - - + Copyright 2012-2015, Kestrel Technology LLC, Palo Alto, CA 94304 diff --git a/CodeHawk/CHB/bchsummaries/msvcrt_dll/gmtime.xml b/CodeHawk/CHB/bchsummaries/msvcrt_dll/gmtime.xml index 93697674..6a02bb6f 100644 --- a/CodeHawk/CHB/bchsummaries/msvcrt_dll/gmtime.xml +++ b/CodeHawk/CHB/bchsummaries/msvcrt_dll/gmtime.xml @@ -33,7 +33,7 @@
- + @@ -41,13 +41,7 @@ - - - - - - - + Copyright 2012-2016, Kestrel Technology LLC, Palo Alto, CA 94304 diff --git a/CodeHawk/CHB/bchsummaries/msvcrt_dll/localtime.xml b/CodeHawk/CHB/bchsummaries/msvcrt_dll/localtime.xml index 88078c88..28d23f77 100644 --- a/CodeHawk/CHB/bchsummaries/msvcrt_dll/localtime.xml +++ b/CodeHawk/CHB/bchsummaries/msvcrt_dll/localtime.xml @@ -24,7 +24,7 @@ - + @@ -32,13 +32,7 @@ - - - - - - - + Copyright 2012-2016, Kestrel Technology LLC, Palo Alto, CA 94304 diff --git a/CodeHawk/CHB/bchsummaries/msvcrt_dll/signal.xml b/CodeHawk/CHB/bchsummaries/msvcrt_dll/signal.xml index f59ff3af..afcc12df 100644 --- a/CodeHawk/CHB/bchsummaries/msvcrt_dll/signal.xml +++ b/CodeHawk/CHB/bchsummaries/msvcrt_dll/signal.xml @@ -32,19 +32,13 @@
- + - - - - - - - + Copyright 2012-2016, Kestrel Technology LLC, Palo Alto, CA 94304 diff --git a/CodeHawk/CHB/bchsummaries/msvcrt_dll/strtol.xml b/CodeHawk/CHB/bchsummaries/msvcrt_dll/strtol.xml index 52ac4a19..8925b231 100644 --- a/CodeHawk/CHB/bchsummaries/msvcrt_dll/strtol.xml +++ b/CodeHawk/CHB/bchsummaries/msvcrt_dll/strtol.xml @@ -34,19 +34,13 @@ int - + - - - - - - - + Copyright 2012-2016, Kestrel Technology LLC, Palo Alto, CA 94304 diff --git a/CodeHawk/CHB/bchsummaries/msvcrt_dll/strtoul.xml b/CodeHawk/CHB/bchsummaries/msvcrt_dll/strtoul.xml index 56e50859..19b8bdfd 100644 --- a/CodeHawk/CHB/bchsummaries/msvcrt_dll/strtoul.xml +++ b/CodeHawk/CHB/bchsummaries/msvcrt_dll/strtoul.xml @@ -34,19 +34,13 @@ int - + - - - - - - - + Copyright 2012-2016, Kestrel Technology LLC, Palo Alto, CA 94304 diff --git a/CodeHawk/CHB/bchsummaries/msvcrt_dll/strxfrm.xml b/CodeHawk/CHB/bchsummaries/msvcrt_dll/strxfrm.xml index 1d702509..04a072ce 100644 --- a/CodeHawk/CHB/bchsummaries/msvcrt_dll/strxfrm.xml +++ b/CodeHawk/CHB/bchsummaries/msvcrt_dll/strxfrm.xml @@ -42,7 +42,7 @@ size_t - + @@ -80,11 +80,6 @@ - - - - - diff --git a/CodeHawk/CHB/bchsummaries/msvcrt_dll/vfprintf.xml b/CodeHawk/CHB/bchsummaries/msvcrt_dll/vfprintf.xml index 05e622b6..71447c52 100644 --- a/CodeHawk/CHB/bchsummaries/msvcrt_dll/vfprintf.xml +++ b/CodeHawk/CHB/bchsummaries/msvcrt_dll/vfprintf.xml @@ -42,7 +42,7 @@ VOID - + @@ -51,13 +51,7 @@ 0 0 - - - - - - - + Copyright 2012-2016, Kestrel Technology LLC, Palo Alto, CA 94304 diff --git a/CodeHawk/CHB/bchsummaries/so_functions/__fgetc_unlocked.xml b/CodeHawk/CHB/bchsummaries/so_functions/__fgetc_unlocked.xml index 37108783..8248fa83 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/__fgetc_unlocked.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/__fgetc_unlocked.xml @@ -24,20 +24,14 @@ int - + - - - - - - - + Copyright 2012-2015, Kestrel Technology LLC, Palo Alto, CA 94304 diff --git a/CodeHawk/CHB/bchsummaries/so_functions/__fputc_unlocked.xml b/CodeHawk/CHB/bchsummaries/so_functions/__fputc_unlocked.xml index 102fda47..3df3b5a0 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/__fputc_unlocked.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/__fputc_unlocked.xml @@ -31,7 +31,7 @@
- + @@ -39,13 +39,7 @@ - - - - - - - + Copyright 2012-2016, Kestrel Technology LLC, Palo Alto, CA 94304 diff --git a/CodeHawk/CHB/bchsummaries/so_functions/accept.xml b/CodeHawk/CHB/bchsummaries/so_functions/accept.xml index b7dcd082..8e918df9 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/accept.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/accept.xml @@ -49,7 +49,7 @@ int - + 
@@ -77,11 +77,6 @@
 	    
 	  
 	
-        
-          
-            
-          
-        
       
     
   
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/access.xml b/CodeHawk/CHB/bchsummaries/so_functions/access.xml
index c0a1dd7c..ad240412 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/access.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/access.xml
@@ -33,7 +33,7 @@
     
     int
    
-   
+   
     
        
     
@@ -41,13 +41,7 @@
     
       
     
-    
-      
-        
-          
-        
-      
-    
+    
    
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/bind.xml b/CodeHawk/CHB/bchsummaries/so_functions/bind.xml
index 17884200..27d36684 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/bind.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/bind.xml
@@ -41,7 +41,7 @@
       
       int
     
-    
+    
       
       
 	
@@ -58,13 +58,7 @@
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/chmod.xml b/CodeHawk/CHB/bchsummaries/so_functions/chmod.xml
index a35fc971..4b1914fc 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/chmod.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/chmod.xml
@@ -30,19 +30,13 @@
       
       int
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/chown.xml b/CodeHawk/CHB/bchsummaries/so_functions/chown.xml
index 0a59b761..148b9637 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/chown.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/chown.xml
@@ -35,19 +35,13 @@
       
       int
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/chroot.xml b/CodeHawk/CHB/bchsummaries/so_functions/chroot.xml
index 5c1bed6f..fe782f69 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/chroot.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/chroot.xml
@@ -21,19 +21,13 @@
       
       int
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/close.xml b/CodeHawk/CHB/bchsummaries/so_functions/close.xml
index a691685b..8320cfde 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/close.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/close.xml
@@ -20,19 +20,13 @@
       
       int
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2019, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/closedir.xml b/CodeHawk/CHB/bchsummaries/so_functions/closedir.xml
index a9fbce1e..72359a0d 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/closedir.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/closedir.xml
@@ -21,19 +21,13 @@
       
       int
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/connect.xml b/CodeHawk/CHB/bchsummaries/so_functions/connect.xml
index dd5b5afc..9fe097a7 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/connect.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/connect.xml
@@ -43,7 +43,7 @@
       
       int
     
-    
+    
       
       
 	
@@ -60,13 +60,7 @@
       
         
       
-      
-	
-	  
-            
-	  
-	
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fdopen.xml b/CodeHawk/CHB/bchsummaries/so_functions/fdopen.xml
index e03ba7b0..a25f3190 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/fdopen.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/fdopen.xml
@@ -35,7 +35,7 @@
     
     ch__FILE
    
-   
+   
     
        
     
@@ -43,13 +43,7 @@
     
       
     
-    
-      
-        
-          
-        
-      
-    
+    
    
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fgetc.xml b/CodeHawk/CHB/bchsummaries/so_functions/fgetc.xml
index 486d1280..2b81c849 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/fgetc.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/fgetc.xml
@@ -24,7 +24,7 @@
     
     int
    
-   
+   
     
      
@@ -33,13 +33,7 @@
     
       
     
-    
-      
-        
-          
-        
-      
-    
+    
    
   
   Copyright 2012-2015, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fgets.xml b/CodeHawk/CHB/bchsummaries/so_functions/fgets.xml
index f6b2282a..4608805e 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/fgets.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/fgets.xml
@@ -56,7 +56,7 @@
      

     
    
-   
+   
     
        
     
@@ -110,11 +110,6 @@
        
       
      
-     
-      
-       
-      
-     
     
    
   
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fileno.xml b/CodeHawk/CHB/bchsummaries/so_functions/fileno.xml
index 398a0563..7b920432 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/fileno.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/fileno.xml
@@ -24,7 +24,7 @@
       
     
    
-   
+   
      
        
      
@@ -32,13 +32,7 @@
     
       
     
-    
-     
-      
-       
-      
-     
-    
+    
    
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/flock.xml b/CodeHawk/CHB/bchsummaries/so_functions/flock.xml
index e9820e5f..f9bbe5b8 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/flock.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/flock.xml
@@ -31,19 +31,13 @@
       
       int
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fopen.xml b/CodeHawk/CHB/bchsummaries/so_functions/fopen.xml
index 3eb0d729..99bfb21d 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/fopen.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/fopen.xml
@@ -29,7 +29,7 @@
       

     
    
-   
+   
      
        
      
@@ -37,13 +37,7 @@
     
      
     
-    
-      
-        
-          
-        
-      
-    
+    
    
   
   Copyright 2012-2016, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fopen64.xml b/CodeHawk/CHB/bchsummaries/so_functions/fopen64.xml
index c171b9bf..52624c3e 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/fopen64.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/fopen64.xml
@@ -29,7 +29,7 @@
      

     
    
-   
+   
      
        
      
@@ -37,13 +37,7 @@
     
      
     
-    
-      
-        
-          
-        
-      
-    
+    
    
   
   Copyright 2012-2016, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fputc.xml b/CodeHawk/CHB/bchsummaries/so_functions/fputc.xml
index ba6d072a..a7de5598 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/fputc.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/fputc.xml
@@ -31,7 +31,7 @@
      

     
    
-   
+   
     
        
     
@@ -39,13 +39,7 @@
     
       
     
-    
-     
-      
-       
-      
-     
-    
+    
    
   
   Copyright 2012-2016, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fputs.xml b/CodeHawk/CHB/bchsummaries/so_functions/fputs.xml
index cdcc051a..c2deb320 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/fputs.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/fputs.xml
@@ -37,7 +37,7 @@
      

     
    
-   
+   
     
       
     
@@ -45,13 +45,7 @@
     
       
     
-    
-      
-        
-          
-        
-      
-    
+    
    
   
   Copyright 2012-2016, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fread.xml b/CodeHawk/CHB/bchsummaries/so_functions/fread.xml
index a58134d9..7f266545 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/fread.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/fread.xml
@@ -48,7 +48,7 @@
      

     
    
-   
+   
      
        
      
@@ -99,11 +99,6 @@
        
       
      
-     
-      
-       
-      
-     
     
    
   
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/freeaddrinfo.xml b/CodeHawk/CHB/bchsummaries/so_functions/freeaddrinfo.xml
index 766f0fb7..c311b011 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/freeaddrinfo.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/freeaddrinfo.xml
@@ -20,19 +20,13 @@
       
       void
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fseek.xml b/CodeHawk/CHB/bchsummaries/so_functions/fseek.xml
index 62e0c1f7..9ef7be9e 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/fseek.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/fseek.xml
@@ -38,7 +38,7 @@
       int
     
    
-   
+   
      
        
      
@@ -46,13 +46,7 @@
     
       
     
-    
-      
-        
-          
-        
-      
-    
+    
    
   
   Copyright 2012-2016, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fstat.xml b/CodeHawk/CHB/bchsummaries/so_functions/fstat.xml
index 4be3e1d9..d46bc178 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/fstat.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/fstat.xml
@@ -33,19 +33,13 @@
       
       int
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fstat64.xml b/CodeHawk/CHB/bchsummaries/so_functions/fstat64.xml
index eaac3cda..fa672596 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/fstat64.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/fstat64.xml
@@ -33,19 +33,13 @@
       
       int
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/ftell.xml b/CodeHawk/CHB/bchsummaries/so_functions/ftell.xml
index dfedd356..f75e8a17 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/ftell.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/ftell.xml
@@ -24,7 +24,7 @@
       
     
    
-   
+   
      
        
@@ -33,13 +33,7 @@
     
       
     
-    
-     
-      
-       
-      
-     
-    
+    
    
   
   Copyright 2012-2015, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/ftruncate.xml b/CodeHawk/CHB/bchsummaries/so_functions/ftruncate.xml
index 4e6bb34e..accc9bc5 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/ftruncate.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/ftruncate.xml
@@ -29,19 +29,13 @@
       
       int
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/ftruncate64.xml b/CodeHawk/CHB/bchsummaries/so_functions/ftruncate64.xml
index 0e2aa5bf..68e35fe9 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/ftruncate64.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/ftruncate64.xml
@@ -29,19 +29,13 @@
       
       int
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fwrite.xml b/CodeHawk/CHB/bchsummaries/so_functions/fwrite.xml
index df8252b5..7fd28f66 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/fwrite.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/fwrite.xml
@@ -43,7 +43,7 @@
       
     
    
-   
+   
      
        
      
@@ -79,13 +79,7 @@
       
      
     
-    
-      
-        
-          
-        
-      
-    
+    
    
   
   Copyright 2012-2016, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/getaddrinfo.xml b/CodeHawk/CHB/bchsummaries/so_functions/getaddrinfo.xml
index 84586daf..7c460cb3 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/getaddrinfo.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/getaddrinfo.xml
@@ -58,19 +58,13 @@
       
       int
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/getcwd.xml b/CodeHawk/CHB/bchsummaries/so_functions/getcwd.xml
index 8272b0d8..b8fa3620 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/getcwd.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/getcwd.xml
@@ -33,7 +33,7 @@
       
       char
     
-    
+    
       
       
 	
@@ -77,11 +77,6 @@
             
           
         
-        
-          
-            
-          
-        
       
     
   
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/getgrgid.xml b/CodeHawk/CHB/bchsummaries/so_functions/getgrgid.xml
index aa3084b0..3995de38 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/getgrgid.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/getgrgid.xml
@@ -20,19 +20,13 @@
       
       ch__group
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
 
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/getgrnam.xml b/CodeHawk/CHB/bchsummaries/so_functions/getgrnam.xml
index d00509f9..0cbe0034 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/getgrnam.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/getgrnam.xml
@@ -23,19 +23,13 @@
       
       ch__group
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
 
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/getgroups.xml b/CodeHawk/CHB/bchsummaries/so_functions/getgroups.xml
index 182739d2..e11eea0b 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/getgroups.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/getgroups.xml
@@ -35,7 +35,7 @@
       
       int
     
-    
+    
       
       
 	
@@ -67,11 +67,6 @@
 	    
 	  
 	
-        
-          
-            
-          
-        
       
     
   
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/gethostbyname.xml b/CodeHawk/CHB/bchsummaries/so_functions/gethostbyname.xml
index bde8f2e6..373e3aca 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/gethostbyname.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/gethostbyname.xml
@@ -20,19 +20,13 @@
       
       ch__hostent
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
 
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/getline.xml b/CodeHawk/CHB/bchsummaries/so_functions/getline.xml
index a1f61dd0..46e4656e 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/getline.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/getline.xml
@@ -36,19 +36,13 @@
       
       int
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/getpeername.xml b/CodeHawk/CHB/bchsummaries/so_functions/getpeername.xml
index 4f75107e..8e893ead 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/getpeername.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/getpeername.xml
@@ -40,7 +40,7 @@
       
       int
     
-    
+    
       
       
 	
@@ -68,11 +68,6 @@
 	    
 	  
 	
-        
-          
-            
-          
-        
       
     
   
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/getpriority.xml b/CodeHawk/CHB/bchsummaries/so_functions/getpriority.xml
index f629ed7d..d7911305 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/getpriority.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/getpriority.xml
@@ -35,19 +35,13 @@
       
       int
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
 
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/getpwnam.xml b/CodeHawk/CHB/bchsummaries/so_functions/getpwnam.xml
index 2305daff..04b93351 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/getpwnam.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/getpwnam.xml
@@ -21,19 +21,13 @@
       
       ch__passwd
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/getrlimit.xml b/CodeHawk/CHB/bchsummaries/so_functions/getrlimit.xml
index 22408951..2c730b19 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/getrlimit.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/getrlimit.xml
@@ -30,19 +30,13 @@
       
       int
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/getrlimit64.xml b/CodeHawk/CHB/bchsummaries/so_functions/getrlimit64.xml
index 0f1d40f1..27f96a34 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/getrlimit64.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/getrlimit64.xml
@@ -31,19 +31,13 @@
       
       int
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/getrusage.xml b/CodeHawk/CHB/bchsummaries/so_functions/getrusage.xml
index 8139374b..962f302d 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/getrusage.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/getrusage.xml
@@ -34,19 +34,13 @@
       
       int
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/getsockname.xml b/CodeHawk/CHB/bchsummaries/so_functions/getsockname.xml
index 4b50ce7d..c0fba875 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/getsockname.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/getsockname.xml
@@ -36,7 +36,7 @@
       
       int
     
-    
+    
       
       
 	
@@ -72,11 +72,6 @@
 	    
 	  
 	
-        
-          
-            
-          
-        
       
     
   
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/getsockopt.xml b/CodeHawk/CHB/bchsummaries/so_functions/getsockopt.xml
index e5085065..1c37a2c6 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/getsockopt.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/getsockopt.xml
@@ -46,7 +46,7 @@
       
       int
     
-    
+    
       
       
 	
@@ -82,11 +82,6 @@
 	    
 	  
 	
-        
-          
-            
-          
-        
       
     
   
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/getspnam.xml b/CodeHawk/CHB/bchsummaries/so_functions/getspnam.xml
index b5268376..772ef320 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/getspnam.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/getspnam.xml
@@ -25,19 +25,13 @@
       
       ch__spwd
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Henny Sipma, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/gmtime.xml b/CodeHawk/CHB/bchsummaries/so_functions/gmtime.xml
index 5a0722f4..1eb1e499 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/gmtime.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/gmtime.xml
@@ -33,7 +33,7 @@
      

     
    
-   
+   
      
        
      
@@ -41,13 +41,7 @@
     
      
     
-    
-     
-      
-       
-      
-     
-    
+    
    
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/if_indextoname.xml b/CodeHawk/CHB/bchsummaries/so_functions/if_indextoname.xml
index 75be8aaa..b5a7de23 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/if_indextoname.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/if_indextoname.xml
@@ -29,7 +29,7 @@
       
       char
     
-    
+    
       
       
 	
@@ -57,11 +57,6 @@
             
           
         
-        
-          
-            
-          
-        
       
     
   
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/inet_ntop.xml b/CodeHawk/CHB/bchsummaries/so_functions/inet_ntop.xml
index 464e135d..d1b918f4 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/inet_ntop.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/inet_ntop.xml
@@ -51,7 +51,7 @@
       
       char
     
-    
+    
       
       
 	
@@ -88,11 +88,6 @@
 	    
 	  
 	
-        
-          
-            
-          
-        
       
     
   
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/inet_pton.xml b/CodeHawk/CHB/bchsummaries/so_functions/inet_pton.xml
index 36c6eff0..989db78b 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/inet_pton.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/inet_pton.xml
@@ -43,19 +43,13 @@
       
       int
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/ioctl.xml b/CodeHawk/CHB/bchsummaries/so_functions/ioctl.xml
index b8f11775..225d6fc5 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/ioctl.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/ioctl.xml
@@ -37,19 +37,13 @@
       
       int
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/kill.xml b/CodeHawk/CHB/bchsummaries/so_functions/kill.xml
index d836d5f5..c4690a30 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/kill.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/kill.xml
@@ -31,19 +31,13 @@
       
       int
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
 
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/killpg.xml b/CodeHawk/CHB/bchsummaries/so_functions/killpg.xml
index 963319cb..5007139c 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/killpg.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/killpg.xml
@@ -29,7 +29,7 @@
       
       int
     
-    
+    
       
       
 	
@@ -45,13 +45,7 @@
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
 
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/listen.xml b/CodeHawk/CHB/bchsummaries/so_functions/listen.xml
index f57cfd15..39e5b861 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/listen.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/listen.xml
@@ -35,19 +35,13 @@
       
       int
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/localtime.xml b/CodeHawk/CHB/bchsummaries/so_functions/localtime.xml
index f98ebe39..5b2dd54b 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/localtime.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/localtime.xml
@@ -24,7 +24,7 @@
       
     
    
-   
+   
      
        
      
@@ -32,13 +32,7 @@
     
      
     
-    
-     
-      
-       
-      
-     
-    
+    
    
   
   Copyright 2012-2016, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/lockf.xml b/CodeHawk/CHB/bchsummaries/so_functions/lockf.xml
index f92e38d5..f7c6fbd0 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/lockf.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/lockf.xml
@@ -38,19 +38,13 @@
       
       int
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/lockf64.xml b/CodeHawk/CHB/bchsummaries/so_functions/lockf64.xml
index 6068c0b1..3603772e 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/lockf64.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/lockf64.xml
@@ -38,19 +38,13 @@
       
       int
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/lseek.xml b/CodeHawk/CHB/bchsummaries/so_functions/lseek.xml
index e81bf2a3..d333f9bc 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/lseek.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/lseek.xml
@@ -36,19 +36,13 @@
       
       off_t
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/lseek64.xml b/CodeHawk/CHB/bchsummaries/so_functions/lseek64.xml
index ed746d70..c6022d4c 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/lseek64.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/lseek64.xml
@@ -36,19 +36,13 @@
       
       off_t
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/malloc.xml b/CodeHawk/CHB/bchsummaries/so_functions/malloc.xml
index 728e9cf8..2b90b004 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/malloc.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/malloc.xml
@@ -24,7 +24,7 @@
      
     
    
-   
+   
      
        
      
@@ -48,13 +48,7 @@
       
      
     
-    
-      
-        
-          
-        
-      
-    
+    
    
   
   Copyright 2012-2016, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/mkdir.xml b/CodeHawk/CHB/bchsummaries/so_functions/mkdir.xml
index facbd57d..dc6b7570 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/mkdir.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/mkdir.xml
@@ -33,7 +33,7 @@
       
       int
     
-    
+    
       
 	
       
@@ -41,13 +41,7 @@
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2024, Henny Sipma, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/mkstemp.xml b/CodeHawk/CHB/bchsummaries/so_functions/mkstemp.xml
index e68c063d..422cfc5f 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/mkstemp.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/mkstemp.xml
@@ -23,19 +23,13 @@
       
       int
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/mkstemp64.xml b/CodeHawk/CHB/bchsummaries/so_functions/mkstemp64.xml
index f549a6d5..18e0e2bb 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/mkstemp64.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/mkstemp64.xml
@@ -23,19 +23,13 @@
       
       int
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/mktime.xml b/CodeHawk/CHB/bchsummaries/so_functions/mktime.xml
index fa2d7970..812b4fb8 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/mktime.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/mktime.xml
@@ -20,7 +20,7 @@
     
     time_t
    
-   
+   
     
       
     
@@ -28,13 +28,7 @@
     
       
     
-    
-      
-        
-          
-        
-      
-    
+    
    
   
  
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/mmap.xml b/CodeHawk/CHB/bchsummaries/so_functions/mmap.xml
index 9b97f00d..90a85b6d 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/mmap.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/mmap.xml
@@ -52,17 +52,11 @@
       
       void
     
-    
+    
       
       
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/mmap64.xml b/CodeHawk/CHB/bchsummaries/so_functions/mmap64.xml
index 0b4ec743..a102968f 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/mmap64.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/mmap64.xml
@@ -52,17 +52,11 @@
       
       void
     
-    
+    
       
       
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/msgrcv.xml b/CodeHawk/CHB/bchsummaries/so_functions/msgrcv.xml
index 92e448a8..b3065c10 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/msgrcv.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/msgrcv.xml
@@ -46,7 +46,7 @@
       
       ssize_t
     
-    
+    
       
       
         
@@ -63,13 +63,7 @@
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2024, Henny Sipma, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/munmap.xml b/CodeHawk/CHB/bchsummaries/so_functions/munmap.xml
index b2bee55f..e15bb911 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/munmap.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/munmap.xml
@@ -33,19 +33,13 @@
       
       int
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/nanosleep.xml b/CodeHawk/CHB/bchsummaries/so_functions/nanosleep.xml
index 41142aa5..c07028d8 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/nanosleep.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/nanosleep.xml
@@ -31,19 +31,13 @@
       
       int
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
 
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/open.xml b/CodeHawk/CHB/bchsummaries/so_functions/open.xml
index 523d1fce..fba56007 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/open.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/open.xml
@@ -33,7 +33,7 @@
     
     int
    
-   
+   
      
        
      
@@ -41,13 +41,7 @@
     
       
     
-    
-      
-        
-          
-        
-      
-    
+    
    
   
   Copyright 2012-2016, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/open64.xml b/CodeHawk/CHB/bchsummaries/so_functions/open64.xml
index b90cfbf5..79d65203 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/open64.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/open64.xml
@@ -38,7 +38,7 @@
     
     int
    
-   
+   
      
        
      
@@ -46,13 +46,7 @@
     
       
     
-    
-      
-        
-          
-        
-      
-    
+    
    
   
   Copyright 2012-2016, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/opendir.xml b/CodeHawk/CHB/bchsummaries/so_functions/opendir.xml
index 2d42f486..07f1083c 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/opendir.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/opendir.xml
@@ -21,19 +21,13 @@
       
       ch__DIR
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
 
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/pclose.xml b/CodeHawk/CHB/bchsummaries/so_functions/pclose.xml
index 92e9c3c7..e7872c22 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/pclose.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/pclose.xml
@@ -21,19 +21,13 @@
       
       int
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/pipe.xml b/CodeHawk/CHB/bchsummaries/so_functions/pipe.xml
index ed49041b..8ceadf7b 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/pipe.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/pipe.xml
@@ -20,7 +20,7 @@
       
       int
     
-    
+    
       
       
 	
@@ -51,11 +51,6 @@
 	    
 	  
 	
-        
-          
-            
-          
-        
       
     
   
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/poll.xml b/CodeHawk/CHB/bchsummaries/so_functions/poll.xml
index 3ec0e56a..1a7a318e 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/poll.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/poll.xml
@@ -40,19 +40,13 @@
       
       int
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/popen.xml b/CodeHawk/CHB/bchsummaries/so_functions/popen.xml
index 2ed17abb..25b173ec 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/popen.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/popen.xml
@@ -31,7 +31,7 @@
       
       ch__FILE
     
-    
+    
       
       
         
@@ -46,13 +46,7 @@
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/putenv.xml b/CodeHawk/CHB/bchsummaries/so_functions/putenv.xml
index 79e49e9a..a89b1325 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/putenv.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/putenv.xml
@@ -30,19 +30,13 @@
       
       int
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
 
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/puts.xml b/CodeHawk/CHB/bchsummaries/so_functions/puts.xml
index 75a1b6d5..7fcd8cad 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/puts.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/puts.xml
@@ -27,7 +27,7 @@
     
     int
    
-   
+   
     
      
     
@@ -35,13 +35,7 @@
     
       
     
-    
-      
-        
-          
-        
-      
-    
+    
    
   
   Copyright 2012-2016, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/read.xml b/CodeHawk/CHB/bchsummaries/so_functions/read.xml
index c73dfe7c..228fd774 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/read.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/read.xml
@@ -34,7 +34,7 @@
       
       ssize_t
     
-    
+    
       
       
 	
@@ -88,11 +88,6 @@
 	    
 	  
 	
-        
-          
-            
-          
-        
       
     
   
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/readdir.xml b/CodeHawk/CHB/bchsummaries/so_functions/readdir.xml
index dd95a671..a47000cc 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/readdir.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/readdir.xml
@@ -21,19 +21,13 @@
       
       ch__dirent
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
 
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/readdir64.xml b/CodeHawk/CHB/bchsummaries/so_functions/readdir64.xml
index f794b394..8ecbaf4c 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/readdir64.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/readdir64.xml
@@ -21,19 +21,13 @@
       
       ch__dirent
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
 
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/readlink.xml b/CodeHawk/CHB/bchsummaries/so_functions/readlink.xml
index f3152e0e..a7889300 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/readlink.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/readlink.xml
@@ -36,7 +36,7 @@
       
       ssize_t
     
-    
+    
       
 	
       
@@ -75,11 +75,6 @@
 	    
 	  
 	
-        
-          
-            
-          
-        
       
     
   
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/realpath.xml b/CodeHawk/CHB/bchsummaries/so_functions/realpath.xml
index 440b182f..0c348adc 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/realpath.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/realpath.xml
@@ -41,7 +41,7 @@
       
       char
     
-    
+    
       
       
 	
@@ -67,11 +67,6 @@
 	    
 	  
 	
-        
-          
-            
-          
-        
       
     
   
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/recv.xml b/CodeHawk/CHB/bchsummaries/so_functions/recv.xml
index 734acc07..c41abc5c 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/recv.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/recv.xml
@@ -44,7 +44,7 @@
       
       ssize_t
     
-    
+    
       
       
 	
@@ -89,11 +89,6 @@
 	    
 	  
 	
-        
-          
-            
-          
-        
       
     
   
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/recvfrom.xml b/CodeHawk/CHB/bchsummaries/so_functions/recvfrom.xml
index fdc413d6..927e0c8d 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/recvfrom.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/recvfrom.xml
@@ -62,7 +62,7 @@
       
       ssize_t
     
-    
+    
       
       
 	
@@ -127,11 +127,6 @@
 	    
 	  
 	
-        
-          
-            
-          
-        
       
     
   
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/recvmsg.xml b/CodeHawk/CHB/bchsummaries/so_functions/recvmsg.xml
index 727ce38a..10055036 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/recvmsg.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/recvmsg.xml
@@ -41,19 +41,13 @@
       
       ssize_t
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
 
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/remove.xml b/CodeHawk/CHB/bchsummaries/so_functions/remove.xml
index bc107c3b..b22b2395 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/remove.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/remove.xml
@@ -24,7 +24,7 @@
      

     
    
-   
+   
     
        
     
@@ -32,13 +32,7 @@
     
       
     
-    
-      
-        
-          
-        
-      
-    
+    
    
   
   Copyright 2012-2016, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/rename.xml b/CodeHawk/CHB/bchsummaries/so_functions/rename.xml
index 765e5de9..f75b22d4 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/rename.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/rename.xml
@@ -31,19 +31,13 @@
       
       int
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/rewind.xml b/CodeHawk/CHB/bchsummaries/so_functions/rewind.xml
index 404ada4b..b9477f41 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/rewind.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/rewind.xml
@@ -21,19 +21,13 @@
     
     void
    
-   
+   
     
       
     
     
     
-    
-      
-        
-          
-        
-      
-    
+    
    
   
   Copyright 2012-2015, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/rmdir.xml b/CodeHawk/CHB/bchsummaries/so_functions/rmdir.xml
index 20a25559..90a486c8 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/rmdir.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/rmdir.xml
@@ -24,7 +24,7 @@
       
       int
     
-    
+    
       
 	
       
@@ -32,13 +32,7 @@
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2024, Henny Sipma, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/select.xml b/CodeHawk/CHB/bchsummaries/so_functions/select.xml
index 69a3c932..3ca8a9f9 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/select.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/select.xml
@@ -61,19 +61,13 @@
       
       int
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/sem_init.xml b/CodeHawk/CHB/bchsummaries/so_functions/sem_init.xml
index c74974d4..4a813734 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/sem_init.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/sem_init.xml
@@ -38,7 +38,7 @@
       
       int
     
-    
+    
       
 	
       
@@ -46,13 +46,7 @@
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2024, Henny Sipma, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/sem_post.xml b/CodeHawk/CHB/bchsummaries/so_functions/sem_post.xml
index abf19f27..f3c35d1d 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/sem_post.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/sem_post.xml
@@ -24,7 +24,7 @@
       
       int
     
-    
+    
       
 	
       
@@ -32,13 +32,7 @@
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2024, Henny Sipma, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/sem_wait.xml b/CodeHawk/CHB/bchsummaries/so_functions/sem_wait.xml
index 97d38a23..e8366684 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/sem_wait.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/sem_wait.xml
@@ -24,7 +24,7 @@
       
       int
     
-    
+    
       
 	
       
@@ -32,13 +32,7 @@
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2024, Henny Sipma, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/send.xml b/CodeHawk/CHB/bchsummaries/so_functions/send.xml
index c0e91bf4..a5404c97 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/send.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/send.xml
@@ -39,7 +39,7 @@
       
       ssize_t
     
-    
+    
       
       
         
@@ -56,13 +56,7 @@
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/sendmsg.xml b/CodeHawk/CHB/bchsummaries/so_functions/sendmsg.xml
index d1e67c4a..37ba8dae 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/sendmsg.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/sendmsg.xml
@@ -41,19 +41,13 @@
       
       ssize_t
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
 
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/sendto.xml b/CodeHawk/CHB/bchsummaries/so_functions/sendto.xml
index 6e03d3fd..78d94c73 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/sendto.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/sendto.xml
@@ -60,7 +60,7 @@
       
       ssize_t
     
-    
+    
       
       
 	
@@ -104,13 +104,7 @@
 	  
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/setegid.xml b/CodeHawk/CHB/bchsummaries/so_functions/setegid.xml
index 45d45c34..c23d18e3 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/setegid.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/setegid.xml
@@ -20,19 +20,13 @@
       
       int
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2024, Henny Sipma, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/setenv.xml b/CodeHawk/CHB/bchsummaries/so_functions/setenv.xml
index a6172625..afa266d9 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/setenv.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/setenv.xml
@@ -45,19 +45,13 @@
       
       int
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
 
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/seteuid.xml b/CodeHawk/CHB/bchsummaries/so_functions/seteuid.xml
index d15a858d..3383de2e 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/seteuid.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/seteuid.xml
@@ -20,19 +20,13 @@
       
       int
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2024, Henny Sipma, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/setgid.xml b/CodeHawk/CHB/bchsummaries/so_functions/setgid.xml
index 254896c2..85ad9548 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/setgid.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/setgid.xml
@@ -23,19 +23,13 @@
       
       int
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
 
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/sethostname.xml b/CodeHawk/CHB/bchsummaries/so_functions/sethostname.xml
index 1792b6b1..154b23e0 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/sethostname.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/sethostname.xml
@@ -29,7 +29,7 @@
       
       int
     
-    
+    
       
       
         
@@ -46,13 +46,7 @@
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2024, Henny Sipma, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/setpgid.xml b/CodeHawk/CHB/bchsummaries/so_functions/setpgid.xml
index 8e4765fa..b79537e6 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/setpgid.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/setpgid.xml
@@ -29,19 +29,13 @@
       
       int
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/setpriority.xml b/CodeHawk/CHB/bchsummaries/so_functions/setpriority.xml
index 633f3565..8e624633 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/setpriority.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/setpriority.xml
@@ -40,19 +40,13 @@
       
       int
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
 
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/setrlimit.xml b/CodeHawk/CHB/bchsummaries/so_functions/setrlimit.xml
index 7809e081..b945b6a4 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/setrlimit.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/setrlimit.xml
@@ -32,19 +32,13 @@
       
       int
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/setrlimit64.xml b/CodeHawk/CHB/bchsummaries/so_functions/setrlimit64.xml
index e30653c1..ee1d6906 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/setrlimit64.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/setrlimit64.xml
@@ -32,19 +32,13 @@
       
       int
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/setsid.xml b/CodeHawk/CHB/bchsummaries/so_functions/setsid.xml
index e88df7c2..ef355f0b 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/setsid.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/setsid.xml
@@ -18,19 +18,13 @@
     
       pid_t
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/setsockopt.xml b/CodeHawk/CHB/bchsummaries/so_functions/setsockopt.xml
index 53694522..14829085 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/setsockopt.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/setsockopt.xml
@@ -46,7 +46,7 @@
       
       int
     
-    
+    
       
       
 	
@@ -63,13 +63,7 @@
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2019, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/settimeofday.xml b/CodeHawk/CHB/bchsummaries/so_functions/settimeofday.xml
index 6df23c7c..9ca629d8 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/settimeofday.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/settimeofday.xml
@@ -31,19 +31,13 @@
       
       int
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2026, Henny Sipma, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/setuid.xml b/CodeHawk/CHB/bchsummaries/so_functions/setuid.xml
index 5821de90..da76910b 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/setuid.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/setuid.xml
@@ -23,19 +23,13 @@
       
       int
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
 
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/shutdown.xml b/CodeHawk/CHB/bchsummaries/so_functions/shutdown.xml
index 02300326..e59b278f 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/shutdown.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/shutdown.xml
@@ -29,19 +29,13 @@
       
       int
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
 
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/sigaction.xml b/CodeHawk/CHB/bchsummaries/so_functions/sigaction.xml
index 18b45c04..ef92014e 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/sigaction.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/sigaction.xml
@@ -43,19 +43,13 @@
       
       int
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/sigaddset.xml b/CodeHawk/CHB/bchsummaries/so_functions/sigaddset.xml
index 7945ccb4..213bba29 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/sigaddset.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/sigaddset.xml
@@ -30,19 +30,13 @@
       
       int
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
 
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/sigemptyset.xml b/CodeHawk/CHB/bchsummaries/so_functions/sigemptyset.xml
index 56b0d884..1146810f 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/sigemptyset.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/sigemptyset.xml
@@ -22,19 +22,13 @@
       
       int
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/sigprocmask.xml b/CodeHawk/CHB/bchsummaries/so_functions/sigprocmask.xml
index 10cfc21d..f5c4ee52 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/sigprocmask.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/sigprocmask.xml
@@ -43,19 +43,13 @@
       
       int
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Henny Sipma, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/socket.xml b/CodeHawk/CHB/bchsummaries/so_functions/socket.xml
index 9a631853..dfdc595b 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/socket.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/socket.xml
@@ -43,19 +43,13 @@
       
       int
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2019, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/socketpair.xml b/CodeHawk/CHB/bchsummaries/so_functions/socketpair.xml
index 0e01a2e2..9ba6ef1d 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/socketpair.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/socketpair.xml
@@ -51,7 +51,7 @@
       
       int
     
-    
+    
       
       
 	
@@ -79,11 +79,6 @@
 	    
 	  
 	
-        
-          
-            
-          
-        
       
     
   
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/sscanf.xml b/CodeHawk/CHB/bchsummaries/so_functions/sscanf.xml
index 660e3fab..7150caa7 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/sscanf.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/sscanf.xml
@@ -34,7 +34,7 @@
       
       int
     
-    
+    
       
       
       
@@ -57,13 +57,7 @@
 	  
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
 
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/stat.xml b/CodeHawk/CHB/bchsummaries/so_functions/stat.xml
index c2319cde..80b29fb1 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/stat.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/stat.xml
@@ -41,7 +41,7 @@
      
     
    
-   
+   
     
        
     
@@ -49,13 +49,7 @@
     
       
     
-    
-      
-        
-          
-        
-      
-    
+    
    
   
   Copyright 2012-2016, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/stat64.xml b/CodeHawk/CHB/bchsummaries/so_functions/stat64.xml
index cc90f736..c6bbf2f0 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/stat64.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/stat64.xml
@@ -41,7 +41,7 @@
      
     
    
-   
+   
     
        
     
@@ -49,13 +49,7 @@
     
       
     
-    
-      
-        
-          
-        
-      
-    
+    
    
   
  
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/statfs.xml b/CodeHawk/CHB/bchsummaries/so_functions/statfs.xml
index 4bd37add..927e658d 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/statfs.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/statfs.xml
@@ -32,19 +32,13 @@
       
       int
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2026, Henny Sipma, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/statfs64.xml b/CodeHawk/CHB/bchsummaries/so_functions/statfs64.xml
index 6eee5e48..8048d7c0 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/statfs64.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/statfs64.xml
@@ -32,19 +32,13 @@
       
       int
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2026, Henny Sipma, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/strdup.xml b/CodeHawk/CHB/bchsummaries/so_functions/strdup.xml
index cc8d83f9..55749fc2 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/strdup.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/strdup.xml
@@ -26,7 +26,7 @@
      

     
    
-   
+   
     
        
     
@@ -58,13 +58,7 @@
       
      
     
-    
-      
-        
-          
-        
-      
-    
+    
    
   
   Copyright 2012-2016, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/strtoll.xml b/CodeHawk/CHB/bchsummaries/so_functions/strtoll.xml
index 02af9f2c..91c3296c 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/strtoll.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/strtoll.xml
@@ -34,19 +34,13 @@
       int
     
    
-   
+   
      
        
      
     
     
-    
-     
-      
-       
-      
-     
-    
+    
    
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/strtoul.xml b/CodeHawk/CHB/bchsummaries/so_functions/strtoul.xml
index 7a536af3..29745b88 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/strtoul.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/strtoul.xml
@@ -34,19 +34,13 @@
       int
     
    
-   
+   
      
        
      
     
     
-    
-     
-      
-       
-      
-     
-    
+    
    
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/strtoull.xml b/CodeHawk/CHB/bchsummaries/so_functions/strtoull.xml
index f594f1e0..5772ae2f 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/strtoull.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/strtoull.xml
@@ -34,19 +34,13 @@
       int
     
    
-   
+   
      
        
      
     
     
-    
-     
-      
-       
-      
-     
-    
+    
    
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/sysinfo.xml b/CodeHawk/CHB/bchsummaries/so_functions/sysinfo.xml
index 65ca66b9..e05d274d 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/sysinfo.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/sysinfo.xml
@@ -21,17 +21,11 @@
       
       int
     
-    
+    
       
       
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/system.xml b/CodeHawk/CHB/bchsummaries/so_functions/system.xml
index 912fd803..4b4de97e 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/system.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/system.xml
@@ -28,7 +28,7 @@
     
     int
    
-   
+   
     
      
     
@@ -45,13 +45,7 @@
     
       
     
-    
-      
-        
-          
-        
-      
-    
+    
    
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/tcflush.xml b/CodeHawk/CHB/bchsummaries/so_functions/tcflush.xml
index 0363416d..64cd8348 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/tcflush.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/tcflush.xml
@@ -29,19 +29,13 @@
       
       int
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2024, Henny Sipma, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/tcgetattr.xml b/CodeHawk/CHB/bchsummaries/so_functions/tcgetattr.xml
index 389979f1..be97fdf4 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/tcgetattr.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/tcgetattr.xml
@@ -31,17 +31,11 @@
       
       int
     
-    
+    
       
       
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2024, Henny Sipma, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/tcsetattr.xml b/CodeHawk/CHB/bchsummaries/so_functions/tcsetattr.xml
index b7b9d456..f93fd292 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/tcsetattr.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/tcsetattr.xml
@@ -35,19 +35,13 @@
       
       int
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2024, Henny Sipma, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/tempnam.xml b/CodeHawk/CHB/bchsummaries/so_functions/tempnam.xml
index 0e0814d1..aff0cd45 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/tempnam.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/tempnam.xml
@@ -31,19 +31,13 @@
       
       char
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2024, Henny Sipma, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/time.xml b/CodeHawk/CHB/bchsummaries/so_functions/time.xml
index 66d4baf7..56a0b027 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/time.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/time.xml
@@ -25,7 +25,7 @@
       
     
    
-   
+   
      
        
      
@@ -33,13 +33,7 @@
     
       
     
-    
-      
-        
-          
-        
-      
-    
+    
    
   
   Copyright 2012-2017, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/times.xml b/CodeHawk/CHB/bchsummaries/so_functions/times.xml
index f624c556..1c2e4011 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/times.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/times.xml
@@ -22,19 +22,13 @@
       
       clock_t
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2026, Henny Sipma, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/unlink.xml b/CodeHawk/CHB/bchsummaries/so_functions/unlink.xml
index 1cecaca1..9f143571 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/unlink.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/unlink.xml
@@ -21,19 +21,13 @@
       
       int
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/usleep.xml b/CodeHawk/CHB/bchsummaries/so_functions/usleep.xml
index 8c67e204..a315195b 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/usleep.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/usleep.xml
@@ -21,19 +21,13 @@
       
       UINT
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
 
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/vfprintf.xml b/CodeHawk/CHB/bchsummaries/so_functions/vfprintf.xml
index 4f7d2576..58b6b795 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/vfprintf.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/vfprintf.xml
@@ -42,7 +42,7 @@
      VOID
     
    
-   
+   
     
        
     
@@ -51,13 +51,7 @@
       0
       0
     
-    
-     
-      
-       
-      
-     
-    
+    
    
   
   Copyright 2012-2016, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/wait.xml b/CodeHawk/CHB/bchsummaries/so_functions/wait.xml
index 4ca3f7e1..17de0a0b 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/wait.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/wait.xml
@@ -21,19 +21,13 @@
       
       pid_t
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2026, Henny Sipma, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/wait4.xml b/CodeHawk/CHB/bchsummaries/so_functions/wait4.xml
index af6693f7..d35acf2d 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/wait4.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/wait4.xml
@@ -43,19 +43,13 @@
       
       pid_t
     
-    
+    
       
       
       
         
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2026, Henny Sipma, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/waitpid.xml b/CodeHawk/CHB/bchsummaries/so_functions/waitpid.xml
index 4c54e311..5b96acfe 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/waitpid.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/waitpid.xml
@@ -41,19 +41,13 @@
       
       pid_t
     
-    
+    
       
       
       
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2020, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/write.xml b/CodeHawk/CHB/bchsummaries/so_functions/write.xml
index 195c1531..af8541d6 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/write.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/write.xml
@@ -34,7 +34,7 @@
       
       size_t
     
-    
+    
       
       
 	
@@ -77,13 +77,7 @@
 	  
 	
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
   Copyright 2012-2019, Kestrel Technology LLC, Palo Alto, CA 94304
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/writev.xml b/CodeHawk/CHB/bchsummaries/so_functions/writev.xml
index 876645ad..506f2552 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/writev.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/writev.xml
@@ -37,7 +37,7 @@
       
       ssize_t
     
-    
+    
       
       
 	
@@ -55,13 +55,7 @@
 	

       
       
-      
-        
-          
-            
-          
-        
-      
+      
     
   
 
diff --git a/CodeHawk/CHB/bchsummaries/ws2_32_dll/gethostname.xml b/CodeHawk/CHB/bchsummaries/ws2_32_dll/gethostname.xml
index faf6c182..2f923eff 100644
--- a/CodeHawk/CHB/bchsummaries/ws2_32_dll/gethostname.xml
+++ b/CodeHawk/CHB/bchsummaries/ws2_32_dll/gethostname.xml
@@ -38,7 +38,7 @@
     
     

    
-   
+   
      
        
@@ -59,7 +59,6 @@
       
     
     
-     
      
       
        

From 2a6c81ec4a3de5b22d2b1ef4e78cc0273ac92083 Mon Sep 17 00:00:00 2001
From: Henny Sipma 
Date: Tue, 9 Jun 2026 22:36:08 -0700
Subject: [PATCH 07/15] CHB: add support for importing postconditions via
 attributes

---
 .../bchlib/bCHAttributesFunctionSemantics.ml  | 75 ++++++++++++++---
 .../bchlib/bCHAttributesFunctionSemantics.mli | 82 ++++++++++++++++++-
 CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml   |  6 +-
 3 files changed, 148 insertions(+), 15 deletions(-)

diff --git a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml
index 504fcedd..ca36457c 100644
--- a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml
+++ b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml
@@ -842,6 +842,50 @@ let get_access_sideeffect
      end
 
 
+let get_chk_post_one
+      (name: string)
+      (attrparams: b_attrparam_t list): xxpredicate_t list =
+  let thisf = NamedConstant name in
+  let rv = ReturnValue thisf in
+  let zero = NumConstant CHNumerical.numerical_zero in
+  match attrparams with
+  | [ACons ("not_null", [])] -> [XXNotNull rv]
+  | [ACons ("null", [])] -> [XXNull rv]
+  | [ACons ("non_negative", [])] -> [XXNonNegative rv]
+  | [ACons ("not_zero", [])] -> [XXNotZero rv]
+  | [ACons ("positive", [])] -> [XXPositive rv]
+  | [ACons ("null_terminated", [])] -> [XXNullTerminated rv]
+  | [ACons ("new_memory", [])] -> [XXNewMemory (rv, RunTimeValue)]
+  | [ACons ("allocation_base", [])] -> [XXAllocationBase rv]
+  | [ACons ("negone", [])] ->
+     let negone = NumConstant (CHNumerical.mkNumerical (-1)) in
+     [XXRelationalExpr (PEquals, rv, negone)]
+  | [ACons ("zero", [])] ->
+     [XXRelationalExpr (PEquals, rv, zero)]
+  | [ACons ("negative", [])] ->
+     [XXRelationalExpr (PLessThan, rv, zero)]
+  | [ACons ("nonpositive", [])] ->
+     [XXRelationalExpr (PLessEqual, rv, zero)]
+  | (ACons (tag, _)) :: _ ->
+     begin
+       log_diagnostics_result
+         ~tag:"get_chk_post_one:tag not recognized"
+         ~msg:name
+         __FILE__ __LINE__
+         ["tag: " ^ tag];
+       []
+     end
+  | _ ->
+     begin
+       log_diagnostics_result
+         ~tag:"get_chk_post_one:not recognized"
+         ~msg:name
+         __FILE__ __LINE__
+         [attrparams_to_string "attrparams" attrparams];
+       []
+     end
+
+
 let get_chk_qual_conditions
       (name: string)
       (attrparams: b_attrparam_t list)
@@ -878,6 +922,7 @@ let convert_b_attributes_to_function_conditions
       (fintf: function_interface_t)
       (attrs: b_attributes_t):
       (xxpredicate_t list
+       * xxpredicate_t list
        * xxpredicate_t list
        * xxpredicate_t list
        * function_qualifiers_t) =
@@ -889,39 +934,47 @@ let convert_b_attributes_to_function_conditions
       fq_sets_errno = None;
       fq_must_use_return = None } in
 
-  List.fold_left (fun ((xpre, xside, xpost, xqual) as acc) attr ->
+  List.fold_left (fun ((xpre, xside, xpost, xepost, xqual) as acc) attr ->
       match attr with
       | Attr ("access", attrparams) ->
          let pre = get_access_preconditions name fparameters attrparams in
          let side = get_access_sideeffect name fparameters attrparams in
-         (pre @ xpre, side @ xside, xpost, xqual)
+         (pre @ xpre, side @ xside, xpost, xepost, xqual)
 
       | Attr ("nonnull", attrparams) ->
          let pre = get_nonnull_preconditions fparameters attrparams in
-         (pre @ xpre, xside, xpost, xqual)
+         (pre @ xpre, xside, xpost, xepost, xqual)
 
       | Attr ("format", attrparams) ->
          let pre = get_format_preconditions name fparameters attrparams in
-         (pre @ xpre, xside, xpost, xqual)
+         (pre @ xpre, xside, xpost, xepost, xqual)
 
       | Attr ("noreturn", []) ->
-         (xpre, xside, xpost, {xqual with fq_noreturn = Some true})
+         (xpre, xside, xpost, xepost, {xqual with fq_noreturn = Some true})
 
       | Attr ("pure", []) ->
-         (xpre, xside, xpost, {xqual with fq_functional = Some FPure})
+         (xpre, xside, xpost, xepost, {xqual with fq_functional = Some FPure})
 
       | Attr ("const", []) ->
-         (xpre, xside, xpost, {xqual with fq_functional = Some FConst})
+         (xpre, xside, xpost, xepost, {xqual with fq_functional = Some FConst})
 
       | Attr ("warn_unused_result", []) ->
-         (xpre, xside, xpost, {xqual with fq_must_use_return = Some true})
+         (xpre, xside, xpost, xepost, {xqual with fq_must_use_return = Some true})
 
       | Attr ("chk_pre", attrparams) ->
          let pre = get_chk_pre_conditions name fparameters attrparams in
-         (pre @ xpre, xside, xpost, xqual)
+         (pre @ xpre, xside, xpost, xepost, xqual)
+
+      | Attr ("chk_post", attrparams) ->
+         let post = get_chk_post_one name attrparams in
+         (xpre, xside, post @ xpost, xepost, xqual)
+
+      | Attr ("chk_epost", attrparams) ->
+         let epost = get_chk_post_one name attrparams in
+         (xpre, xside, xpost, epost @ xepost, xqual)
 
       | Attr ("chk_qual", attrparams) ->
-         (xpre, xside, xpost, get_chk_qual_conditions name attrparams xqual)
+         (xpre, xside, xpost, xepost, get_chk_qual_conditions name attrparams xqual)
 
       | Attr (attrname, _) ->
          begin
@@ -931,4 +984,4 @@ let convert_b_attributes_to_function_conditions
              __FILE__ __LINE__
              ["attrname: " ^ attrname];
            acc
-         end) ([], [], [], empty_qualifiers) attrs
+         end) ([], [], [], [], empty_qualifiers) attrs
diff --git a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.mli b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.mli
index 6da23c81..77b7068e 100644
--- a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.mli
+++ b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.mli
@@ -46,9 +46,9 @@ open BCHLibTypes
     {2 Attribute policy}
 
     Two categories of attributes are accepted on input. Only [chk_pre],
-    [chk_se], and [chk_post] are emitted in generated output headers; the
-    GCC compatibility attributes are read-only (see
-    bCHFunctionSemanticsAttributes.ml for the output path).
+    [chk_se], [chk_post], [chk_epost], and [chk_qual] are emitted in
+    generated output headers; the GCC compatibility attributes are read-only
+    (see bCHFunctionSemanticsAttributes.ml for the output path).
 
     {3 GCC compatibility attributes (read-only)}
 
@@ -243,6 +243,81 @@ open BCHLibTypes
     -> {!XXTrustedOsCmdFmtString}: the string constructed from this format
     argument is safe to pass to [system(3)].
 
+    {3 chk_post / chk_epost: CodeHawk postconditions}
+
+    These are the canonical forms for postconditions on the return value
+    ([chk_post] for the success case, [chk_epost] for the error case). Index 0
+    always refers to the return value; no argument index is specified.
+
+    {[
+    __attribute__ ((chk_post (not_null)))
+    ]}
+    -> {!XXNotNull} on the return value (return is not null on success).
+
+    {[
+    __attribute__ ((chk_post (null)))
+    ]}
+    -> {!XXNull} on the return value (return is null on success).
+
+    {[
+    __attribute__ ((chk_post (non_negative)))
+    ]}
+    -> {!XXNonNegative} on the return value (return >= 0 on success).
+
+    {[
+    __attribute__ ((chk_post (not_zero)))
+    ]}
+    -> {!XXNotZero} on the return value (return != 0 on success).
+
+    {[
+    __attribute__ ((chk_post (positive)))
+    ]}
+    -> {!XXPositive} on the return value (return > 0 on success).
+
+    {[
+    __attribute__ ((chk_post (null_terminated)))
+    ]}
+    -> {!XXNullTerminated} on the return value (return points to a
+    null-terminated string on success).
+
+    {[
+    __attribute__ ((chk_post (new_memory)))
+    ]}
+    -> {!XXNewMemory} on the return value (return is freshly allocated
+    memory on success).
+
+    {[
+    __attribute__ ((chk_post (allocation_base)))
+    ]}
+    -> {!XXAllocationBase} on the return value (return is the base of an
+    allocation on success).
+
+    The following forms are primarily useful as error postconditions with
+    [chk_epost], but are accepted by both:
+
+    {[
+    __attribute__ ((chk_epost (null)))       (* return is NULL on error *)
+    __attribute__ ((chk_epost (negone)))      (* return is -1 on error  *)
+    __attribute__ ((chk_epost (zero)))        (* return is 0 on error   *)
+    __attribute__ ((chk_epost (negative)))    (* return < 0 on error    *)
+    __attribute__ ((chk_epost (nonpositive))) (* return <= 0 on error   *)
+    ]}
+
+    Common paired patterns (each requires two attributes):
+    {[
+    /* notnull-null: success=not null, error=null */
+    __attribute__ ((chk_post (not_null), chk_epost (null)))
+
+    /* zero-negone: success=0, error=-1 */
+    __attribute__ ((chk_post (zero), chk_epost (negone)))
+
+    /* nonnegative-negative: success>=0, error<0 */
+    __attribute__ ((chk_post (non_negative), chk_epost (negative)))
+
+    /* positive-zero: success>0, error=0 */
+    __attribute__ ((chk_post (positive), chk_epost (zero)))
+    ]}
+
     {3 chk_qual: CodeHawk function qualifiers}
 
     These are the canonical forms for non-predicate function properties that
@@ -284,6 +359,7 @@ val convert_b_attributes_to_function_conditions:
   function_interface_t
   -> b_attributes_t
   -> (xxpredicate_t list
+      * xxpredicate_t list
       * xxpredicate_t list
       * xxpredicate_t list
       * function_qualifiers_t)
diff --git a/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml b/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml
index 5252b362..8e12895c 100644
--- a/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml
+++ b/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml
@@ -363,7 +363,7 @@ let default_function_semantics = {
 let bvarinfo_to_function_semantics
            (vinfo: bvarinfo_t) (fintf: function_interface_t): function_semantics_t =
   if (List.length vinfo.bvattr) > 0 then
-    let (preconditions, sideeffects, _, qualifiers) =
+    let (preconditions, sideeffects, postconditions, errorpostconditions, qualifiers) =
       convert_b_attributes_to_function_conditions fintf vinfo.bvattr in
     let _ =
       log_diagnostics_result
@@ -372,11 +372,15 @@ let bvarinfo_to_function_semantics
         __FILE__ __LINE__
         ["pre: " ^ (string_of_int (List.length preconditions));
          "side: " ^ (string_of_int (List.length sideeffects));
+         "post: " ^ (string_of_int (List.length postconditions));
+         "epost: " ^ (string_of_int (List.length errorpostconditions));
          "attrs: " ^ (attributes_to_string vinfo.bvattr)] in
     let fsem =
       {default_function_semantics with
         fsem_pre = preconditions;
         fsem_sideeffects = sideeffects;
+        fsem_post = postconditions;
+        fsem_errorpost = errorpostconditions;
         fsem_qualifiers = qualifiers} in
     let _ =
       log_diagnostics_result

From b58943e97c87b44af941f92bb782ab7e2ccf6ff6 Mon Sep 17 00:00:00 2001
From: Henny Sipma 
Date: Tue, 9 Jun 2026 22:58:41 -0700
Subject: [PATCH 08/15] CHB: add support for importing side effects via
 attributes

---
 .../bchlib/bCHAttributesFunctionSemantics.ml  | 170 ++++++++++++++++++
 .../bchlib/bCHAttributesFunctionSemantics.mli |  39 ++++
 2 files changed, 209 insertions(+)

diff --git a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml
index ca36457c..a7be144e 100644
--- a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml
+++ b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml
@@ -800,6 +800,172 @@ let get_deref_write_sideeffect
             attrparams_to_string "argparams" argparams]
 
 
+let get_freed_sideeffect
+      (fparams: fts_parameter_t list)
+      (tagparams: b_attrparam_t list)
+      (argparams: b_attrparam_t list): xxpredicate_t traceresult =
+  match (tagparams, argparams) with
+  | ([], [AInt refindex]) ->
+     let* par = get_par fparams refindex in
+     Ok (XXFreed (ArgValue par))
+  | _ ->
+     Error [(elocm __LINE__) ^ "freed params not recognized";
+            fparams_to_string fparams;
+            attrparams_to_string "tagparams" tagparams;
+            attrparams_to_string "argparams" argparams]
+
+
+let get_modifies_sideeffect
+      (fparams: fts_parameter_t list)
+      (tagparams: b_attrparam_t list)
+      (argparams: b_attrparam_t list): xxpredicate_t traceresult =
+  match (tagparams, argparams) with
+  | ([], [AInt refindex]) ->
+     let* par = get_par fparams refindex in
+     Ok (XXModified (ArgValue par))
+  | _ ->
+     Error [(elocm __LINE__) ^ "modifies params not recognized";
+            fparams_to_string fparams;
+            attrparams_to_string "tagparams" tagparams;
+            attrparams_to_string "argparams" argparams]
+
+
+let get_invalidates_sideeffect
+      (fparams: fts_parameter_t list)
+      (tagparams: b_attrparam_t list)
+      (argparams: b_attrparam_t list): xxpredicate_t traceresult =
+  match (tagparams, argparams) with
+  | ([], [AInt refindex]) ->
+     let* par = get_par fparams refindex in
+     Ok (XXInvalidated (ArgValue par))
+  | _ ->
+     Error [(elocm __LINE__) ^ "invalidates params not recognized";
+            fparams_to_string fparams;
+            attrparams_to_string "tagparams" tagparams;
+            attrparams_to_string "argparams" argparams]
+
+
+let get_deref_write_null_sideeffect
+      (fparams: fts_parameter_t list)
+      (tagparams: b_attrparam_t list)
+      (argparams: b_attrparam_t list): xxpredicate_t traceresult =
+  match (tagparams, argparams) with
+  | ([], [AInt refindex]) ->
+     let* par = get_par fparams refindex in
+     let* ty = get_derefty par in
+     let pval = ArgValue par in
+     Ok (XXConditional (XXNotNull pval, XXBlockWrite (ty, pval, RunTimeValue)))
+
+  | ([], [AInt refindex; AInt sizeindex]) ->
+     let* bufferparam = get_par fparams refindex in
+     let* sizeparam = get_par fparams sizeindex in
+     let* ty = get_derefty bufferparam in
+     let pval = ArgValue bufferparam in
+     Ok (XXConditional (XXNotNull pval, XXBlockWrite (ty, pval, ArgValue sizeparam)))
+
+  | _ ->
+     Error [(elocm __LINE__) ^ "deref_write_null params not recognized";
+            fparams_to_string fparams;
+            attrparams_to_string "tagparams" tagparams;
+            attrparams_to_string "argparams" argparams]
+
+
+let get_chk_se_conditions
+      (name: string)
+      (fparams: fts_parameter_t list)
+      (attrparams: b_attrparam_t list): xxpredicate_t list =
+  match attrparams with
+  | (ACons ("deref_write", tagparams)) :: argparams ->
+     TR.tfold
+       ~ok:(fun xse -> [xse])
+       ~error:(fun e ->
+         begin
+           log_error_result
+             ~tag:"get_chk_se_conditions:deref_write"
+             ~msg:name
+             __FILE__ __LINE__
+             [String.concat ", " e];
+           []
+         end)
+       (get_deref_write_sideeffect fparams tagparams argparams)
+
+  | (ACons ("deref_write_null", tagparams)) :: argparams ->
+     TR.tfold
+       ~ok:(fun xse -> [xse])
+       ~error:(fun e ->
+         begin
+           log_error_result
+             ~tag:"get_chk_se_conditions:deref_write_null"
+             ~msg:name
+             __FILE__ __LINE__
+             [String.concat ", " e];
+           []
+         end)
+       (get_deref_write_null_sideeffect fparams tagparams argparams)
+
+  | (ACons ("freed", tagparams)) :: argparams ->
+     TR.tfold
+       ~ok:(fun xse -> [xse])
+       ~error:(fun e ->
+         begin
+           log_error_result
+             ~tag:"get_chk_se_conditions:freed"
+             ~msg:name
+             __FILE__ __LINE__
+             [String.concat ", " e];
+           []
+         end)
+       (get_freed_sideeffect fparams tagparams argparams)
+
+  | (ACons ("modifies", tagparams)) :: argparams ->
+     TR.tfold
+       ~ok:(fun xse -> [xse])
+       ~error:(fun e ->
+         begin
+           log_error_result
+             ~tag:"get_chk_se_conditions:modifies"
+             ~msg:name
+             __FILE__ __LINE__
+             [String.concat ", " e];
+           []
+         end)
+       (get_modifies_sideeffect fparams tagparams argparams)
+
+  | (ACons ("invalidates", tagparams)) :: argparams ->
+     TR.tfold
+       ~ok:(fun xse -> [xse])
+       ~error:(fun e ->
+         begin
+           log_error_result
+             ~tag:"get_chk_se_conditions:invalidates"
+             ~msg:name
+             __FILE__ __LINE__
+             [String.concat ", " e];
+           []
+         end)
+       (get_invalidates_sideeffect fparams tagparams argparams)
+
+  | (ACons (tag, _)) :: _ ->
+     begin
+       log_diagnostics_result
+         ~tag:"get_chk_se_conditions:tag not recognized"
+         ~msg:name
+         __FILE__ __LINE__
+         ["tag: " ^ tag];
+       []
+     end
+
+  | _ ->
+     begin
+       log_diagnostics_result
+         ~tag:"get_chk_se_conditions:not recognized"
+         ~msg:name
+         __FILE__ __LINE__
+         [fparams_to_string fparams; attrparams_to_string "attrparams" attrparams];
+       []
+     end
+
+
 let get_access_sideeffect
       (name: string)
       (fparams: fts_parameter_t list)
@@ -965,6 +1131,10 @@ let convert_b_attributes_to_function_conditions
          let pre = get_chk_pre_conditions name fparameters attrparams in
          (pre @ xpre, xside, xpost, xepost, xqual)
 
+      | Attr ("chk_se", attrparams) ->
+         let side = get_chk_se_conditions name fparameters attrparams in
+         (xpre, side @ xside, xpost, xepost, xqual)
+
       | Attr ("chk_post", attrparams) ->
          let post = get_chk_post_one name attrparams in
          (xpre, xside, post @ xpost, xepost, xqual)
diff --git a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.mli b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.mli
index 77b7068e..53b4277c 100644
--- a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.mli
+++ b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.mli
@@ -243,6 +243,45 @@ open BCHLibTypes
     -> {!XXTrustedOsCmdFmtString}: the string constructed from this format
     argument is safe to pass to [system(3)].
 
+    {3 chk_se: CodeHawk side effects}
+
+    The canonical form for side effects on pointer arguments. The sub-tag
+    identifies the kind; [ref-index] is the 1-based index of the pointer
+    parameter.
+
+    {[
+    __attribute__ ((chk_se (deref_write, ref-index)))
+    __attribute__ ((chk_se (deref_write, ref-index, size-index)))
+    __attribute__ ((chk_se (deref_write (size), ref-index)))
+    ]}
+    -> {!XXBlockWrite}: the function writes into the buffer at [ref-index].
+    Size is given by [size-index] argument, a constant, or is unknown
+    ([RunTimeValue]).
+
+    {[
+    __attribute__ ((chk_se (deref_write_null, ref-index)))
+    __attribute__ ((chk_se (deref_write_null, ref-index, size-index)))
+    ]}
+    -> {!XXConditional} ({!XXNotNull}, {!XXBlockWrite}): the function writes
+    into [ref-index] only when it is not null.
+
+    {[
+    __attribute__ ((chk_se (freed, ref-index)))
+    ]}
+    -> {!XXFreed}: the function frees the pointer at [ref-index].
+
+    {[
+    __attribute__ ((chk_se (modifies, ref-index)))
+    ]}
+    -> {!XXModified}: the function modifies the memory at [ref-index] in an
+    unspecified way.
+
+    {[
+    __attribute__ ((chk_se (invalidates, ref-index)))
+    ]}
+    -> {!XXInvalidated}: the pointer at [ref-index] becomes invalid after the
+    call (e.g., after [realloc] the old pointer must not be used).
+
     {3 chk_post / chk_epost: CodeHawk postconditions}
 
     These are the canonical forms for postconditions on the return value

From 07964361c75158430f8fe315adb50f6706f26cbf Mon Sep 17 00:00:00 2001
From: Henny Sipma 
Date: Tue, 9 Jun 2026 23:34:29 -0700
Subject: [PATCH 09/15] CHB: allow for postcondition attributes on parameters

---
 .../bchlib/bCHAttributesFunctionSemantics.ml  | 91 +++++++++++--------
 .../bchlib/bCHAttributesFunctionSemantics.mli | 44 ++++++++-
 2 files changed, 94 insertions(+), 41 deletions(-)

diff --git a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml
index a7be144e..1663e3b3 100644
--- a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml
+++ b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml
@@ -1010,46 +1010,61 @@ let get_access_sideeffect
 
 let get_chk_post_one
       (name: string)
+      (fparams: fts_parameter_t list)
       (attrparams: b_attrparam_t list): xxpredicate_t list =
   let thisf = NamedConstant name in
   let rv = ReturnValue thisf in
   let zero = NumConstant CHNumerical.numerical_zero in
-  match attrparams with
-  | [ACons ("not_null", [])] -> [XXNotNull rv]
-  | [ACons ("null", [])] -> [XXNull rv]
-  | [ACons ("non_negative", [])] -> [XXNonNegative rv]
-  | [ACons ("not_zero", [])] -> [XXNotZero rv]
-  | [ACons ("positive", [])] -> [XXPositive rv]
-  | [ACons ("null_terminated", [])] -> [XXNullTerminated rv]
-  | [ACons ("new_memory", [])] -> [XXNewMemory (rv, RunTimeValue)]
-  | [ACons ("allocation_base", [])] -> [XXAllocationBase rv]
-  | [ACons ("negone", [])] ->
-     let negone = NumConstant (CHNumerical.mkNumerical (-1)) in
-     [XXRelationalExpr (PEquals, rv, negone)]
-  | [ACons ("zero", [])] ->
-     [XXRelationalExpr (PEquals, rv, zero)]
-  | [ACons ("negative", [])] ->
-     [XXRelationalExpr (PLessThan, rv, zero)]
-  | [ACons ("nonpositive", [])] ->
-     [XXRelationalExpr (PLessEqual, rv, zero)]
-  | (ACons (tag, _)) :: _ ->
-     begin
-       log_diagnostics_result
-         ~tag:"get_chk_post_one:tag not recognized"
-         ~msg:name
-         __FILE__ __LINE__
-         ["tag: " ^ tag];
-       []
-     end
-  | _ ->
-     begin
-       log_diagnostics_result
-         ~tag:"get_chk_post_one:not recognized"
-         ~msg:name
-         __FILE__ __LINE__
-         [attrparams_to_string "attrparams" attrparams];
-       []
-     end
+  (* Resolve target term: bare predicate → return value; predicate + AInt → parameter *)
+  let target_result =
+    match attrparams with
+    | [ACons (pred, [])] -> Ok (pred, rv)
+    | [ACons (pred, []); AInt refindex] ->
+       let* par = get_par fparams refindex in
+       Ok (pred, ArgValue par)
+    | (ACons (tag, _)) :: _ ->
+       Error [(elocm __LINE__) ^ "chk_post tag not recognized: " ^ tag]
+    | _ ->
+       Error [(elocm __LINE__) ^ "chk_post params not recognized";
+              attrparams_to_string "attrparams" attrparams] in
+  TR.tfold
+    ~error:(fun e ->
+      begin
+        log_diagnostics_result
+          ~tag:"get_chk_post_one:not recognized"
+          ~msg:name
+          __FILE__ __LINE__
+          e;
+        []
+      end)
+    ~ok:(fun (pred, target) ->
+      let negone = NumConstant (CHNumerical.mkNumerical (-1)) in
+      match pred with
+      | "not_null"            -> [XXNotNull target]
+      | "null"                -> [XXNull target]
+      | "non_negative"        -> [XXNonNegative target]
+      | "not_zero"            -> [XXNotZero target]
+      | "positive"            -> [XXPositive target]
+      | "null_terminated"     -> [XXNullTerminated target]
+      | "new_memory"          -> [XXNewMemory (target, RunTimeValue)]
+      | "allocation_base"     -> [XXAllocationBase target]
+      | "trusted_string"      -> [XXTrustedString target]
+      | "trusted_os_cmd_string" -> [XXTrustedOsCmdString target]
+      | "tainted"             -> [XXTainted target]
+      | "negone"              -> [XXRelationalExpr (PEquals, target, negone)]
+      | "zero"                -> [XXRelationalExpr (PEquals, target, zero)]
+      | "negative"            -> [XXRelationalExpr (PLessThan, target, zero)]
+      | "nonpositive"         -> [XXRelationalExpr (PLessEqual, target, zero)]
+      | tag ->
+         begin
+           log_diagnostics_result
+             ~tag:"get_chk_post_one:tag not recognized"
+             ~msg:name
+             __FILE__ __LINE__
+             ["tag: " ^ tag];
+           []
+         end)
+    target_result
 
 
 let get_chk_qual_conditions
@@ -1136,11 +1151,11 @@ let convert_b_attributes_to_function_conditions
          (xpre, side @ xside, xpost, xepost, xqual)
 
       | Attr ("chk_post", attrparams) ->
-         let post = get_chk_post_one name attrparams in
+         let post = get_chk_post_one name fparameters attrparams in
          (xpre, xside, post @ xpost, xepost, xqual)
 
       | Attr ("chk_epost", attrparams) ->
-         let epost = get_chk_post_one name attrparams in
+         let epost = get_chk_post_one name fparameters attrparams in
          (xpre, xside, xpost, epost @ xepost, xqual)
 
       | Attr ("chk_qual", attrparams) ->
diff --git a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.mli b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.mli
index 53b4277c..496b411a 100644
--- a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.mli
+++ b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.mli
@@ -284,9 +284,18 @@ open BCHLibTypes
 
     {3 chk_post / chk_epost: CodeHawk postconditions}
 
-    These are the canonical forms for postconditions on the return value
-    ([chk_post] for the success case, [chk_epost] for the error case). Index 0
-    always refers to the return value; no argument index is specified.
+    These are the canonical forms for postconditions ([chk_post] for the
+    success case, [chk_epost] for the error case).
+
+    Each attribute takes a predicate name and an optional 1-based argument
+    index. When no index is given the predicate applies to the return value;
+    when an index is given the predicate applies to the post-call state of
+    that parameter.
+
+    {[
+    __attribute__ ((chk_post (pred)))           (* applies to return value *)
+    __attribute__ ((chk_post (pred, ref-index))) (* applies to parameter   *)
+    ]}
 
     {[
     __attribute__ ((chk_post (not_null)))
@@ -331,6 +340,28 @@ open BCHLibTypes
     -> {!XXAllocationBase} on the return value (return is the base of an
     allocation on success).
 
+    {[
+    __attribute__ ((chk_post (trusted_string)))
+    ]}
+    -> {!XXTrustedString} on the return value (return is a trusted string
+    value). Used in patching: a sanitizing replacement function can declare
+    its output trusted so that downstream proof obligations on the string
+    value are discharged.
+
+    {[
+    __attribute__ ((chk_post (trusted_os_cmd_string)))
+    ]}
+    -> {!XXTrustedOsCmdString} on the return value (return is safe to pass
+    to [system(3)]). Used in patching: a command-injection sanitizer declares
+    its output safe, discharging the [XPOTrustedOsCmdString] proof obligation
+    at the [system] call site.
+
+    {[
+    __attribute__ ((chk_post (tainted)))
+    ]}
+    -> {!XXTainted} on the return value (return value is externally controlled
+    and must not be used without validation).
+
     The following forms are primarily useful as error postconditions with
     [chk_epost], but are accepted by both:
 
@@ -357,6 +388,13 @@ open BCHLibTypes
     __attribute__ ((chk_post (positive), chk_epost (zero)))
     ]}
 
+    Parameter postcondition example ([strcpy]-style: destination is
+    null-terminated after the call):
+    {[
+    __attribute__ ((chk_post (null_terminated, 1)))
+    char *strcpy (char *dst, const char *src);
+    ]}
+
     {3 chk_qual: CodeHawk function qualifiers}
 
     These are the canonical forms for non-predicate function properties that

From c094ba50c2245e88fa6617a05424c4b18619d5cb Mon Sep 17 00:00:00 2001
From: Henny Sipma 
Date: Wed, 10 Jun 2026 16:16:30 -0700
Subject: [PATCH 10/15] CHB: output path for attributes representing
 preconditions, postconditions, etc.

---
 CodeHawk/CHB/bchlib/bCHFunctionInterface.ml   |   2 +-
 .../bchlib/bCHFunctionSemanticsAttributes.ml  | 266 +++++++++++++++++-
 CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml |   8 +-
 3 files changed, 267 insertions(+), 9 deletions(-)

diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml b/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml
index 68c1697c..677cc58e 100644
--- a/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml
+++ b/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml
@@ -1344,7 +1344,7 @@ let function_interface_to_bfuntype (fintf: function_interface_t): btype_t =
   let par_funarg (_, name, ty) = (name, ty, []) in
   let funargs =
     Some ((List.map par_funarg regPars) @ (List.map par_funarg stackPars)) in
-  TFun (fts.fts_returntype, funargs, false, [])
+  TFun (fts.fts_returntype, funargs, fts.fts_varargs, [])
 
 
 let function_type_resolvents_to_bfuntype
diff --git a/CodeHawk/CHB/bchlib/bCHFunctionSemanticsAttributes.ml b/CodeHawk/CHB/bchlib/bCHFunctionSemanticsAttributes.ml
index d284b449..fa876339 100644
--- a/CodeHawk/CHB/bchlib/bCHFunctionSemanticsAttributes.ml
+++ b/CodeHawk/CHB/bchlib/bCHFunctionSemanticsAttributes.ml
@@ -26,9 +26,17 @@
    ============================================================================= *)
 
 (* Output path: function semantics → attributes (for delegated preconditions,
-   side effects, postconditions in generated header files).
+   side effects, postconditions, error-postconditions, and qualifiers in
+   generated header files).
+
+   Emitted forms:
+   - chk_pre  : delegated proof obligations (preconditions)
+   - chk_se   : side effects (block-write, freed, modifies, invalidates)
+   - chk_post : postconditions on the return value or a parameter
+   - chk_epost: error-path postconditions
+   - chk_qual : CodeHawk-specific qualifiers (sets_errno)
+   - noreturn, pure, const, warn_unused_result: standard GCC qualifiers
 
-   Only canonical CodeHawk forms (chk_pre, chk_se, chk_post) are emitted.
    GCC compatibility forms (access, nonnull, format) are accepted on input
    but never generated here.
 
@@ -46,6 +54,7 @@ open BCHLibTypes
 
 module TR = CHTraceResult
 
+let (let*) x f = CHTraceResult.tbind f x
 
 let p2s = CHPrettyUtil.pretty_to_string
 
@@ -274,8 +283,257 @@ let convert_preconditions_to_attributes
       | _ -> acc) [] preconditions      
 
 
+let convert_xxpredicate_to_post_attrparams
+      (ctx: string)
+      (xpred: xxpredicate_t): b_attrparam_t list option =
+  let target_params target =
+    match target with
+    | ReturnValue _ -> Some []
+    | ArgValue par ->
+       (match par.apar_index with
+        | Some index -> Some [AInt index]
+        | None ->
+           begin
+             log_diagnostics_result
+               ~tag:"convert_xxpredicate_to_post_attrparams:no index"
+               ~msg:ctx
+               __FILE__ __LINE__
+               ["par: " ^ (bterm_to_string (ArgValue par))];
+             None
+           end)
+    | _ ->
+       begin
+         log_diagnostics_result
+           ~tag:"convert_xxpredicate_to_post_attrparams:unexpected target"
+           ~msg:ctx
+           __FILE__ __LINE__
+           ["target: " ^ (bterm_to_string target)];
+         None
+       end in
+  let make pred target =
+    match target_params target with
+    | None -> None
+    | Some argparams -> Some (ACons (pred, []) :: argparams) in
+  let zero = CHNumerical.numerical_zero in
+  let negone = CHNumerical.mkNumerical (-1) in
+  match xpred with
+  | XXNotNull target         -> make "not_null" target
+  | XXNull target            -> make "null" target
+  | XXNonNegative target     -> make "non_negative" target
+  | XXNotZero target         -> make "not_zero" target
+  | XXPositive target        -> make "positive" target
+  | XXNullTerminated target  -> make "null_terminated" target
+  | XXNewMemory (target, RunTimeValue) -> make "new_memory" target
+  | XXAllocationBase target  -> make "allocation_base" target
+  | XXTrustedString target   -> make "trusted_string" target
+  | XXTrustedOsCmdString target -> make "trusted_os_cmd_string" target
+  | XXTainted target         -> make "tainted" target
+  | XXRelationalExpr (PEquals, target, NumConstant n) when n#equal negone ->
+     make "negone" target
+  | XXRelationalExpr (PEquals, target, NumConstant n) when n#equal zero ->
+     make "zero" target
+  | XXRelationalExpr (PLessThan, target, NumConstant n) when n#equal zero ->
+     make "negative" target
+  | XXRelationalExpr (PLessEqual, target, NumConstant n) when n#equal zero ->
+     make "nonpositive" target
+  | _ ->
+     begin
+       log_diagnostics_result
+         ~tag:"convert_xxpredicate_to_post_attrparams:not representable"
+         ~msg:ctx
+         __FILE__ __LINE__
+         ["pred: " ^ (p2s (BCHExternalPredicate.xxpredicate_to_pretty xpred))];
+       None
+     end
+
+
+let convert_postconditions_to_attributes
+      (ctx: string)
+      (attrname: string)
+      (postconditions: xxpredicate_t list): b_attributes_t =
+  List.filter_map (fun xpred ->
+      match convert_xxpredicate_to_post_attrparams ctx xpred with
+      | None -> None
+      | Some params -> Some (Attr (attrname, params))) postconditions
+
+
+let convert_sideeffect_to_attribute
+      (ctx: string)
+      (xpred: xxpredicate_t): b_attribute_t option =
+  let par_index par =
+    match par.apar_index with
+    | Some index -> Ok index
+    | None ->
+       Error [(elocm __LINE__)
+              ^ "parameter has no index: "
+              ^ par.apar_name] in
+  match xpred with
+  | XXBlockWrite (_, ArgValue par, RunTimeValue) ->
+     TR.tfold
+       ~ok:(fun index ->
+         Some (Attr ("chk_se", [ACons ("deref_write", []); AInt index])))
+       ~error:(fun e ->
+         begin
+           log_diagnostics_result
+             ~tag:"convert_sideeffect_to_attribute:deref_write"
+             ~msg:ctx __FILE__ __LINE__ e;
+           None
+         end)
+       (par_index par)
+
+  | XXBlockWrite (_, ArgValue par, ArgValue sizepar) ->
+     TR.tfold
+       ~ok:(fun (index, sizeindex) ->
+         Some (Attr ("chk_se",
+                     [ACons ("deref_write", []); AInt index; AInt sizeindex])))
+       ~error:(fun e ->
+         begin
+           log_diagnostics_result
+             ~tag:"convert_sideeffect_to_attribute:deref_write(sized)"
+             ~msg:ctx __FILE__ __LINE__ e;
+           None
+         end)
+       (let* i = par_index par in
+        let* s = par_index sizepar in
+        Ok (i, s))
+
+  | XXBlockWrite (_, ArgValue par, NumConstant n) ->
+     TR.tfold
+       ~ok:(fun index ->
+         Some (Attr ("chk_se",
+                     [ACons ("deref_write", [AInt n#toInt]); AInt index])))
+       ~error:(fun e ->
+         begin
+           log_diagnostics_result
+             ~tag:"convert_sideeffect_to_attribute:deref_write(const)"
+             ~msg:ctx __FILE__ __LINE__ e;
+           None
+         end)
+       (par_index par)
+
+  | XXFreed (ArgValue par) ->
+     TR.tfold
+       ~ok:(fun index ->
+         Some (Attr ("chk_se", [ACons ("freed", []); AInt index])))
+       ~error:(fun e ->
+         begin
+           log_diagnostics_result
+             ~tag:"convert_sideeffect_to_attribute:freed"
+             ~msg:ctx __FILE__ __LINE__ e;
+           None
+         end)
+       (par_index par)
+
+  | XXModified (ArgValue par) ->
+     TR.tfold
+       ~ok:(fun index ->
+         Some (Attr ("chk_se", [ACons ("modifies", []); AInt index])))
+       ~error:(fun e ->
+         begin
+           log_diagnostics_result
+             ~tag:"convert_sideeffect_to_attribute:modifies"
+             ~msg:ctx __FILE__ __LINE__ e;
+           None
+         end)
+       (par_index par)
+
+  | XXInvalidated (ArgValue par) ->
+     TR.tfold
+       ~ok:(fun index ->
+         Some (Attr ("chk_se", [ACons ("invalidates", []); AInt index])))
+       ~error:(fun e ->
+         begin
+           log_diagnostics_result
+             ~tag:"convert_sideeffect_to_attribute:invalidates"
+             ~msg:ctx __FILE__ __LINE__ e;
+           None
+         end)
+       (par_index par)
+
+  | XXConditional (XXNotNull (ArgValue par),
+                   XXBlockWrite (_, ArgValue par', RunTimeValue))
+       when is_same_bterm_par (ArgValue par) (ArgValue par') ->
+     TR.tfold
+       ~ok:(fun index ->
+         Some (Attr ("chk_se", [ACons ("deref_write_null", []); AInt index])))
+       ~error:(fun e ->
+         begin
+           log_diagnostics_result
+             ~tag:"convert_sideeffect_to_attribute:deref_write_null"
+             ~msg:ctx __FILE__ __LINE__ e;
+           None
+         end)
+       (par_index par)
+
+  | XXConditional (XXNotNull (ArgValue par),
+                   XXBlockWrite (_, ArgValue par', ArgValue sizepar))
+       when is_same_bterm_par (ArgValue par) (ArgValue par') ->
+     TR.tfold
+       ~ok:(fun (index, sizeindex) ->
+         Some (Attr ("chk_se",
+                     [ACons ("deref_write_null", []); AInt index; AInt sizeindex])))
+       ~error:(fun e ->
+         begin
+           log_diagnostics_result
+             ~tag:"convert_sideeffect_to_attribute:deref_write_null(sized)"
+             ~msg:ctx __FILE__ __LINE__ e;
+           None
+         end)
+       (let* i = par_index par in
+        let* s = par_index sizepar in
+        Ok (i, s))
+
+  | _ ->
+     begin
+       log_diagnostics_result
+         ~tag:"convert_sideeffect_to_attribute:not representable"
+         ~msg:ctx
+         __FILE__ __LINE__
+         ["pred: " ^ (p2s (BCHExternalPredicate.xxpredicate_to_pretty xpred))];
+       None
+     end
+
+
+let convert_sideeffects_to_attributes
+      (ctx: string)
+      (sideeffects: xxpredicate_t list): b_attributes_t =
+  List.filter_map (convert_sideeffect_to_attribute ctx) sideeffects
+
+
+let convert_qualifiers_to_attributes
+      (qualifiers: function_qualifiers_t): b_attributes_t =
+  let attrs = [] in
+  let attrs =
+    match qualifiers.fq_noreturn with
+    | Some true -> Attr ("noreturn", []) :: attrs
+    | _ -> attrs in
+  let attrs =
+    match qualifiers.fq_functional with
+    | Some FPure  -> Attr ("pure", []) :: attrs
+    | Some FConst -> Attr ("const", []) :: attrs
+    | _ -> attrs in
+  let attrs =
+    match qualifiers.fq_sets_errno with
+    | Some true ->
+       Attr ("chk_qual", [ACons ("sets_errno", [])]) :: attrs
+    | _ -> attrs in
+  let attrs =
+    match qualifiers.fq_must_use_return with
+    | Some true -> Attr ("warn_unused_result", []) :: attrs
+    | _ -> attrs in
+  attrs
+
+
 let convert_semantics_to_attributes (finfo: function_info_int): b_attributes_t =
+  let ctx = finfo#get_name in
   let delegatedpos = finfo#proofobligations#delegated_proofobligations in
+  let sem = finfo#get_summary#get_function_semantics in
   let preattrs = convert_preconditions_to_attributes finfo delegatedpos in
-  preattrs
-  
+  let seattrs = convert_sideeffects_to_attributes ctx sem.fsem_sideeffects in
+  let postattrs =
+    convert_postconditions_to_attributes ctx "chk_post" sem.fsem_post in
+  let epostattrs =
+    convert_postconditions_to_attributes ctx "chk_epost" sem.fsem_errorpost in
+  let qualattrs = convert_qualifiers_to_attributes sem.fsem_qualifiers in
+  preattrs @ seattrs @ postattrs @ epostattrs @ qualattrs
+
diff --git a/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml b/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml
index e6f07e79..7e4e40fc 100644
--- a/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml
+++ b/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml
@@ -462,8 +462,8 @@ object (self)
     }
 
   method index_function_qualifiers (fq: function_qualifiers_t) =
-    let ibo = function Some true -> 1 | Some false -> 0 | None -> -1 in
-    let ifunc = function Some FConst -> 1 | Some FPure -> 0 | None -> -1 in
+    let ibo = function Some true -> 2 | Some false -> 1 | None -> -1 in
+    let ifunc = function Some FConst -> 2 | Some FPure -> 1 | None -> -1 in
     let args = [
         ibo fq.fq_noreturn;
         ifunc fq.fq_functional;
@@ -476,8 +476,8 @@ object (self)
     let name = "function-qualifiers" in
     let (_, args) = function_qualifiers_table#retrieve index in
     let a = a name args in
-    let gbo = function 1 -> Some true | 0 -> Some false | _ -> None in
-    let gfunc = function 1 -> Some FConst | 0 -> Some FPure | _ -> None in
+    let gbo = function 2 -> Some true | 1 -> Some false | _ -> None in
+    let gfunc = function 2 -> Some FConst | 1 -> Some FPure | _ -> None in
     { fq_noreturn = gbo (a 0);
       fq_functional = gfunc (a 1);
       fq_sets_errno = gbo (a 2);

From 5a9bc2fa0ab513dcbb8af126d96621603aa90b26 Mon Sep 17 00:00:00 2001
From: Henny Sipma 
Date: Wed, 10 Jun 2026 19:17:26 -0700
Subject: [PATCH 11/15] CHB: add formatstring capability to type inference

---
 CodeHawk/CHB/bchlib/bCHFunctionInterface.ml   |  7 ++--
 CodeHawk/CHB/bchlib/bCHFunctionInterface.mli  |  4 +-
 CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml   | 14 +++++++
 CodeHawk/CHB/bchlib/bCHLibTypes.mli           |  9 +++++
 CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml   |  9 +++--
 .../CHB/bchlib/bCHTypeConstraintDictionary.ml |  8 +++-
 CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml | 14 ++++++-
 CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml  | 29 ++++++++++++++
 CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.mli | 16 ++++++++
 CodeHawk/CHB/bchlib/bCHVersion.ml             |  4 +-
 .../CHB/bchlibarm32/bCHARMAnalysisResults.ml  |  2 +-
 .../bchlibarm32/bCHFnARMTypeConstraints.ml    | 40 +++++++++++++++++--
 12 files changed, 139 insertions(+), 17 deletions(-)

diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml b/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml
index 677cc58e..051c26fa 100644
--- a/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml
+++ b/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml
@@ -1350,9 +1350,10 @@ let function_interface_to_bfuntype (fintf: function_interface_t): btype_t =
 let function_type_resolvents_to_bfuntype
       (name: string)
       (resolvents: (register_t * btype_t option * b_attributes_t) list
-       * btype_t option): btype_t =
-  let fintf = default_function_interface name in
-  let (regtypes, returntype) = resolvents in
+       * btype_t option
+       * bool): btype_t =
+  let (regtypes, returntype, varargs) = resolvents in
+  let fintf = default_function_interface ~varargs name in
   let fintf =
     List.fold_left (fun fintf (reg, optty, _) ->
         match optty with
diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInterface.mli b/CodeHawk/CHB/bchlib/bCHFunctionInterface.mli
index 21db3390..2bf4ee18 100644
--- a/CodeHawk/CHB/bchlib/bCHFunctionInterface.mli
+++ b/CodeHawk/CHB/bchlib/bCHFunctionInterface.mli
@@ -117,7 +117,9 @@ val bvarinfo_to_function_interface: bvarinfo_t -> function_interface_t
 
 val function_type_resolvents_to_bfuntype:
   string
-  -> ((register_t * btype_t option * b_attributes_t) list * btype_t option)
+  -> ((register_t * btype_t option * b_attributes_t) list
+      * btype_t option
+      * bool)
   -> btype_t
 
 
diff --git a/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml b/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml
index 8e12895c..132d0753 100644
--- a/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml
+++ b/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml
@@ -432,6 +432,20 @@ let get_type_arg_mode
                | _ -> None) None predicates
       else
         mode in
+    let mode =
+      if Option.is_none mode then
+        List.fold_left (fun acc p ->
+            match acc with
+            | Some _ -> acc
+            | _ ->
+               match p with
+               | XXInputFormatString (ArgValue param)
+                    when Option.is_some param.apar_index
+                         && (Option.get param.apar_index) = argindex ->
+                  Some ArgInputFormatString
+               | _ -> None) None predicates
+      else
+        mode in
     let mode =
       if Option.is_none mode then
         List.fold_left (fun acc p ->
diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli
index 799f4801..1320314c 100644
--- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli
+++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli
@@ -3314,6 +3314,7 @@ type type_arg_mode_t =
   | ArgFunctionPointer
   | ArgScalarValue
   | ArgOutputFormatString
+  | ArgInputFormatString
 
 
 type type_operation_kind_t =
@@ -3334,6 +3335,11 @@ type type_cap_label_t =
   | FlowsToOperation of type_operation_kind_t * bterm_t option
   | FlowsFrom of bterm_t option
 
+  | FOutputFormatString
+  (** parameter is a printf-style format string; implies the function is variadic *)
+  | FInputFormatString
+  (** parameter is a scanf-style format string; implies the function is variadic *)
+
   | FReturn  (** for now limited to the default return register *)
   | Load
   | Store
@@ -3492,6 +3498,9 @@ class type type_constraint_store_int =
              string
              -> (register_t * btype_t option * b_attributes_t) list
                 * btype_t option
+                * bool
+             (** The bool is [true] if any parameter was identified as a
+                 format-string parameter, implying the function is variadic. *)
 
     method resolve_reglhs_type:
              register_t -> string -> string -> btype_t option
diff --git a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml
index 7ea171b4..58a398aa 100644
--- a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml
+++ b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml
@@ -549,8 +549,9 @@ object
     | ArgFunctionPointer -> "fp"
     | ArgScalarValue -> "s"
     | ArgOutputFormatString -> "fmt"
+    | ArgInputFormatString -> "ifs"
 
-  method !tags = ["d"; "fmt"; "fp"; "r"; "rw"; "s"; "w"]
+  method !tags = ["d"; "fmt"; "fp"; "ifs"; "r"; "rw"; "s"; "w"]
 
 end
 
@@ -593,6 +594,8 @@ object
     | FlowsToArg _ -> "fta"
     | FlowsToOperation _ -> "fto"
     | FlowsFrom _ -> "ffm"
+    | FOutputFormatString -> "fofs"
+    | FInputFormatString -> "fifs"
     | Load -> "l"
     | Store -> "s"
     | Deref -> "d"
@@ -602,8 +605,8 @@ object
     | OffsetAccessA _ -> "aa"
 
   method !tags = [
-      "a"; "aa"; "d"; "faw"; "ffm"; "fr"; "fs"; "fta"; "fto"; "fx"; "l";
-      "lsb"; "lsh"; "s"; "sa"]
+      "a"; "aa"; "d"; "faw"; "ffm"; "fifs"; "fofs"; "fr"; "fs"; "fta"; "fto";
+      "fx"; "l"; "lsb"; "lsh"; "s"; "sa"]
 
 end
 
diff --git a/CodeHawk/CHB/bchlib/bCHTypeConstraintDictionary.ml b/CodeHawk/CHB/bchlib/bCHTypeConstraintDictionary.ml
index f4ee9ce4..bf8a1b66 100644
--- a/CodeHawk/CHB/bchlib/bCHTypeConstraintDictionary.ml
+++ b/CodeHawk/CHB/bchlib/bCHTypeConstraintDictionary.ml
@@ -94,7 +94,8 @@ object (self)
       | ArgDeallocate
         | ArgFunctionPointer
         | ArgScalarValue
-        | ArgOutputFormatString -> (tags, []) in
+        | ArgOutputFormatString
+        | ArgInputFormatString -> (tags, []) in
     type_arg_mode_table#add key
 
   method get_type_arg_mode (index: int): type_arg_mode_t =
@@ -107,6 +108,7 @@ object (self)
     | "d" -> ArgDeallocate
     | "fmt" -> ArgOutputFormatString
     | "fp" -> ArgFunctionPointer
+    | "ifs" -> ArgInputFormatString
     | "r" -> ArgDerefRead (getsize ())
     | "rw" -> ArgDerefReadWrite (getsize ())
     | "s" -> ArgScalarValue
@@ -155,6 +157,8 @@ object (self)
       | FlowsFrom t ->
          (tags,
           [match t with Some t -> id#index_bterm t | _ -> (-1)])
+      | FOutputFormatString -> (tags, [])
+      | FInputFormatString -> (tags, [])
       | Load -> (tags, [])
       | Store -> (tags, [])
       | Deref -> (tags, [])
@@ -185,6 +189,8 @@ object (self)
     | "fto" ->
        FlowsToOperation (type_operation_kind_mfts#fs (t 1),
                          if (a 0) = (-1) then None else Some (id#get_bterm (a 0)))
+    | "fofs" -> FOutputFormatString
+    | "fifs" -> FInputFormatString
     | "a" -> OffsetAccess (a 0, a 1)
     | "aa" -> OffsetAccessA (a 0, a 1)
     | s -> raise_tag_error name s type_cap_label_mcts#tags
diff --git a/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml b/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml
index 06ec304b..371e1df4 100644
--- a/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml
+++ b/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml
@@ -564,7 +564,9 @@ object (self)
 
   method resolve_function_type
            (faddr: string)
-         : (register_t * btype_t option * b_attributes_t) list * btype_t option =
+         : (register_t * btype_t option * b_attributes_t) list
+           * btype_t option
+           * bool =
     let evaluation = self#evaluate_function_type faddr in
     let result = H.create 4 in
     let returnresult = ref None in
@@ -752,7 +754,15 @@ object (self)
          "return: " ^ (match !returnresult with
                        | Some ty -> btype_to_string ty
                        | _ -> "?")] in
-    (result, !returnresult)
+    let varargs =
+      H.fold (fun _k capslists acc ->
+          acc
+          || List.exists
+               (fun caps ->
+                 List.mem FOutputFormatString caps
+                 || List.mem FInputFormatString caps) capslists)
+        capresult false in
+    (result, !returnresult, varargs)
 
   method resolve_reglhs_type
            (reg: register_t) (faddr: string) (iaddr: string): btype_t option =
diff --git a/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml b/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml
index cbfb44a3..a8543069 100644
--- a/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml
+++ b/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml
@@ -74,6 +74,9 @@ let _type_arg_mode_compare (m1: type_arg_mode_t) (m2: type_arg_mode_t): int =
   | (ArgScalarValue, _) -> -1
   | (_, ArgScalarValue) -> 1
   | (ArgOutputFormatString, ArgOutputFormatString) -> 0
+  | (ArgOutputFormatString, _) -> -1
+  | (_, ArgOutputFormatString) -> 1
+  | (ArgInputFormatString, ArgInputFormatString) -> 0
 
 
 let type_cap_label_compare (c1: type_cap_label_t) (c2: type_cap_label_t) =
@@ -134,6 +137,12 @@ let type_cap_label_compare (c1: type_cap_label_t) (c2: type_cap_label_t) =
   | (_, OffsetAccess _) -> 1
   | (OffsetAccessA (n1, m1), OffsetAccessA (n2, m2)) ->
      Stdlib.compare (n1, m1) (n2, m2)
+  | (OffsetAccessA _, _) -> -1
+  | (_, OffsetAccessA _) -> 1
+  | (FOutputFormatString, FOutputFormatString) -> 0
+  | (FOutputFormatString, _) -> -1
+  | (_, FOutputFormatString) -> 1
+  | (FInputFormatString, FInputFormatString) -> 0
 
 
 let type_arg_mode_to_string (m: type_arg_mode_t) =
@@ -149,6 +158,7 @@ let type_arg_mode_to_string (m: type_arg_mode_t) =
   | ArgFunctionPointer -> "fp"
   | ArgScalarValue -> "sv"
   | ArgOutputFormatString -> "ofs"
+  | ArgInputFormatString -> "ifs"
 
 
 let type_operation_kind_to_string (op: type_operation_kind_t) =
@@ -180,6 +190,8 @@ let type_cap_label_to_string (c: type_cap_label_t) =
      ^ (type_operation_kind_to_string op)
      ^ (optbterm_to_string t)
   | FlowsFrom t -> "flowsfrom" ^ (optbterm_to_string t)
+  | FOutputFormatString -> "output-format-string"
+  | FInputFormatString -> "input-format-string"
   | Load -> "load"
   | Store -> "store"
   | Deref -> "deref"
@@ -469,6 +481,14 @@ let add_stack_address_capability (offset: int) (tv: type_variable_t)
   add_capability [FLocStackAddress offset] tv
 
 
+let add_output_format_string_capability (tv: type_variable_t): type_variable_t =
+  add_capability [FOutputFormatString] tv
+
+
+let add_input_format_string_capability (tv: type_variable_t): type_variable_t =
+  add_capability [FInputFormatString] tv
+
+
 let convert_function_capabilities_to_attributes
       (paramindex: int) (caps: type_cap_label_t list): b_attributes_t =
   let type_arg_mode_to_cons_attrparam (m: type_arg_mode_t) =
@@ -484,6 +504,7 @@ let convert_function_capabilities_to_attributes
     | ArgFunctionPointer -> ACons ("fp", [])
     | ArgScalarValue -> ACons ("sv", [])
     | ArgOutputFormatString -> ACons ("printf_format_string", [])
+    | ArgInputFormatString -> ACons ("scanf_format_string", [])
   in
   let result = new CHUtils.IntCollections.set_t in
   let _ =
@@ -498,6 +519,14 @@ let convert_function_capabilities_to_attributes
                     AInt argindex;
                     type_arg_mode_to_cons_attrparam mode]) in
            result#add (bcd#index_attribute attr)
+        | FOutputFormatString ->
+           let attr =
+             Attr ("format", [ACons ("printf", []); AInt paramindex; AInt 0]) in
+           result#add (bcd#index_attribute attr)
+        | FInputFormatString ->
+           let attr =
+             Attr ("format", [ACons ("scanf", []); AInt paramindex; AInt 0]) in
+           result#add (bcd#index_attribute attr)
         | _ -> ()) caps in
   List.map bcd#get_attribute result#toList
 
diff --git a/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.mli b/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.mli
index 25fddebe..70b1c490 100644
--- a/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.mli
+++ b/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.mli
@@ -245,6 +245,22 @@ val add_flows_from_capability:
 val add_stack_address_capability: int -> type_variable_t -> type_variable_t
 
 
+(** [add_output_format_string_capability tv] returns a new type variable that
+    appends an [FOutputFormatString] capability to [tv], which is expected to
+    already carry an [FRegParameter] prefix (set via [add_freg_param_capability]).
+    Indicates that the named parameter is a printf-style format string parameter
+    and thus the enclosing function is variadic. *)
+val add_output_format_string_capability: type_variable_t -> type_variable_t
+
+
+(** [add_input_format_string_capability tv] returns a new type variable that
+    appends an [FInputFormatString] capability to [tv], which is expected to
+    already carry an [FRegParameter] prefix (set via [add_freg_param_capability]).
+    Indicates that the named parameter is a scanf-style format string parameter
+    and thus the enclosing function is variadic. *)
+val add_input_format_string_capability: type_variable_t -> type_variable_t
+
+
 val drop_capability: type_cap_label_t -> type_variable_t -> type_variable_t
 
 
diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml
index f463a4e5..6d19fb6f 100644
--- a/CodeHawk/CHB/bchlib/bCHVersion.ml
+++ b/CodeHawk/CHB/bchlib/bCHVersion.ml
@@ -95,8 +95,8 @@ end
 
 
 let version = new version_info_t 
-  ~version:"0.6.0_20260601"
-  ~date:"2026-06-01"
+  ~version:"0.6.0_20260610"
+  ~date:"2026-06-10"
   ~licensee: None
   ~maxfilesize: None
   ()
diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml b/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml
index 4f824b87..843af983 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml
@@ -324,7 +324,7 @@ object (self)
               let ftype =
                 BCHFunctionInterface.function_type_resolvents_to_bfuntype
                   fname resolvents in
-              let (regtypes, _) = resolvents in
+              let (regtypes, _, _) = resolvents in
               let attrs = List.concat (List.map (fun (_, _, a) -> a) regtypes) in
               let attrs =
                 (BCHFunctionSemanticsAttributes.convert_semantics_to_attributes finfo)
diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml
index ca68abb5..26c1a079 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml
@@ -297,14 +297,14 @@ object (self)
                  let typevar = mk_function_typevar faddr in
                  TR.tfold
                    ~ok:(fun reg ->
-                     let typevar = add_freg_param_capability reg typevar in
+                     let typevar_param = add_freg_param_capability reg typevar in
                      let typevar =
                        add_flows_to_arg_capability
-                         iaddr call argindex argmode typevar in
+                         iaddr call argindex argmode typevar_param in
                      let rule = "BL-arg-param" in
                      let opttc =
                        mk_btype_constraint ~use_voidptr:true typevar argtype in
-                     match opttc with
+                     (match opttc with
                      | Some tc ->
                         if fndata#is_typing_rule_enabled iaddr rule then
                           begin
@@ -319,7 +319,39 @@ object (self)
                           ~msg:(p2s floc#l#toPretty)
                           __FILE__ __LINE__
                           ["x: " ^ (x2s x);
-                           "btype: " ^ (btype_to_string argtype)])
+                           "btype: " ^ (btype_to_string argtype)]);
+                     (match argmode with
+                      | ArgOutputFormatString ->
+                         let typevar_fmt =
+                           add_output_format_string_capability typevar_param in
+                         let opttc =
+                           mk_btype_constraint ~use_voidptr:true typevar_fmt argtype in
+                         (match opttc with
+                          | Some tc ->
+                             if fndata#is_typing_rule_enabled iaddr rule then
+                               begin
+                                 log_type_constraint __LINE__ rule tc;
+                                 store#add_constraint faddr iaddr rule tc
+                               end
+                             else
+                               log_type_constraint_rule_disabled __LINE__ rule tc
+                          | _ -> ())
+                      | ArgInputFormatString ->
+                         let typevar_fmt =
+                           add_input_format_string_capability typevar_param in
+                         let opttc =
+                           mk_btype_constraint ~use_voidptr:true typevar_fmt argtype in
+                         (match opttc with
+                          | Some tc ->
+                             if fndata#is_typing_rule_enabled iaddr rule then
+                               begin
+                                 log_type_constraint __LINE__ rule tc;
+                                 store#add_constraint faddr iaddr rule tc
+                               end
+                             else
+                               log_type_constraint_rule_disabled __LINE__ rule tc
+                          | _ -> ())
+                      | _ -> ()))
                    ~error:(fun e ->
                      log_diagnostics_result
                        ~tag:mnem

From 3fe75009b726cf61c1ead7be826aeb7c1e81d2cb Mon Sep 17 00:00:00 2001
From: Henny Sipma 
Date: Thu, 11 Jun 2026 11:39:16 -0700
Subject: [PATCH 12/15] CHB:ARM: use symbolic function name for exporting
 signatures

---
 CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml b/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml
index 843af983..85edb454 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml
@@ -318,8 +318,11 @@ object (self)
            fnadata#write_xml node;
            (if mksignature then
               let fname =
-                BCHFunctionData.get_default_functionsummary_name_dw
-                  fn#get_address in
+                if fndata#has_name then
+                  fndata#get_function_name
+                else
+                  BCHFunctionData.get_default_functionsummary_name_dw
+                    fn#get_address in
               let resolvents = typeconstraintstore#resolve_function_type faddr in
               let ftype =
                 BCHFunctionInterface.function_type_resolvents_to_bfuntype

From cfe935166f7f58bb75ba4637530b2394ea68ac15 Mon Sep 17 00:00:00 2001
From: Henny Sipma 
Date: Thu, 11 Jun 2026 11:39:56 -0700
Subject: [PATCH 13/15] CHB: add local delegation for trusted-os-cmd-fmt string

---
 CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml | 27 +++++++++++++++----
 1 file changed, 22 insertions(+), 5 deletions(-)

diff --git a/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml b/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml
index 16e4d1b0..830cf0a0 100644
--- a/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml
+++ b/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml
@@ -332,12 +332,29 @@ let trusted_os_cmd_fmt_string_va_list_delegate
   | _ -> Open
 
 
+let trusted_os_cmd_fmt_string_fmt_args_delegate
+      (finfo: function_info_int)
+      (loc: location_int)
+      (fmtargs: annotated_format_arg_t list): po_status_t =
+  let strargs =
+    List.filter (fun (conv, _, _) ->
+        match conv with
+        | CHFormatStringParser.StringConverter -> true
+        | _ -> false) fmtargs in
+  List.fold_left (fun _acc (_, _, argxpr) ->
+      let new_xpo = XPOTrustedOsCmdFmtArgString (argxpr, NO_QUOTES, None) in
+      finfo#proofobligations#add_proofobligation loc#ci new_xpo Open;
+      DelegatedLocal (loc#ci, new_xpo)
+    ) Open strargs
+
+
 let discharge_trusted_os_cmd_fmt_string
       (finfo: function_info_int)
       (loc: location_int)
       (x: xpr_t)
       (kind: format_args_kind_t)
-      (optlen: xpr_t option): po_status_t =
+      (optlen: xpr_t option)
+      (fmtargs: annotated_format_arg_t list): po_status_t =
   let status = trusted_os_cmd_fmt_string_no_string_conversions loc x in
   let status =
     match status with
@@ -345,8 +362,8 @@ let discharge_trusted_os_cmd_fmt_string
        (match kind with
         | VA_LIST ->
            trusted_os_cmd_fmt_string_va_list_delegate finfo loc x optlen
-        | FMT_ARGS -> status)
-        (* trusted_os_cmd_fmt_string_fmt_args_delegate_local finfo loc x optlen) *)
+        | FMT_ARGS ->
+           trusted_os_cmd_fmt_string_fmt_args_delegate finfo loc fmtargs)
     | _ -> status in
   match status with
   | Open ->
@@ -961,8 +978,8 @@ let discharge_one
   | XPOTrustedOsCmdString x ->
      discharge_trusted_os_cmd_string finfo po#loc x
 
-  | XPOTrustedOsCmdFmtString (x, kind, optlen, _) ->
-     discharge_trusted_os_cmd_fmt_string finfo po#loc x kind optlen
+  | XPOTrustedOsCmdFmtString (x, kind, optlen, fmtargs) ->
+     discharge_trusted_os_cmd_fmt_string finfo po#loc x kind optlen fmtargs
 
   | XPOOutputFormatString x ->
      discharge_output_format_string finfo po#loc x

From 11da1898d66b559dec8a47f086c8cacc2c2ca310 Mon Sep 17 00:00:00 2001
From: Henny Sipma 
Date: Thu, 11 Jun 2026 12:23:09 -0700
Subject: [PATCH 14/15] CHB: add proof obligation discharge for
 trusted-os-cmd-fmt-arg-string

---
 CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml | 73 +++++++++++++++++++
 1 file changed, 73 insertions(+)

diff --git a/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml b/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml
index 830cf0a0..8275358b 100644
--- a/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml
+++ b/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml
@@ -379,6 +379,76 @@ let discharge_trusted_os_cmd_fmt_string
      status
 
 
+(* -------------------------------------------------------------------------
+   XPOTrustedOsCmdFmtArgString
+   ------------------------------------------------------------------------- *)
+
+let trusted_os_cmd_fmt_arg_string_constant_string_stmt
+      (loc: location_int) (x: xpr_t) (_quotes: quote_status_t): po_status_t =
+  match get_constant_string loc x with
+  | Some s -> Discharged ("constant string: " ^ s)
+  | _ -> Open
+
+
+(** Discharge by matching a [XXTrustedOsCmdString] or [XXTrustedString]
+    postcondition on the call that produced [x] as its return value. *)
+let trusted_os_cmd_fmt_arg_string_return_value_postcondition
+      (finfo: function_info_int)
+      (_loc: location_int)
+      (x: xpr_t)
+      (_quotes: quote_status_t)
+      (_optlen: int option): po_status_t =
+  match x with
+  | XVar v when finfo#env#is_return_value v ->
+     TR.tfold
+       ~ok:(fun callsite ->
+         let ctinfo = finfo#get_call_target callsite in
+         let is_trusted post =
+           match post with
+           | XXTrustedOsCmdString (ReturnValue _) -> true
+           | XXTrustedString (ReturnValue _) -> true
+           | _ -> false in
+         if List.exists is_trusted ctinfo#get_postconditions then
+           Discharged ("return value of " ^ ctinfo#get_name ^ " is trusted")
+         else
+           Open)
+       ~error:(fun _ -> Open)
+       (finfo#env#get_call_site v)
+  | _ -> Open
+
+
+let trusted_os_cmd_fmt_arg_string_delegate_local
+      (_finfo: function_info_int)
+      (_loc: location_int)
+      (_x: xpr_t)
+      (_quotes: quote_status_t)
+      (_optlen: int option): po_status_t =
+  Open
+
+
+let discharge_trusted_os_cmd_fmt_arg_string
+      (finfo: function_info_int)
+      (loc: location_int)
+      (x: xpr_t)
+      (quotes: quote_status_t)
+      (optlen: int option): po_status_t =
+  let status =
+    trusted_os_cmd_fmt_arg_string_constant_string_stmt loc x quotes in
+  let status =
+    match status with
+    | Open ->
+       trusted_os_cmd_fmt_arg_string_return_value_postcondition
+         finfo loc x quotes optlen
+    | _ -> status in
+  let status =
+    match status with
+    | Open ->
+       trusted_os_cmd_fmt_arg_string_delegate_local
+         finfo loc x quotes optlen
+    | _ -> status in
+  status
+
+
 (* -------------------------------------------------------------------------
    XPOOutputFormatString
    ------------------------------------------------------------------------- *)
@@ -981,6 +1051,9 @@ let discharge_one
   | XPOTrustedOsCmdFmtString (x, kind, optlen, fmtargs) ->
      discharge_trusted_os_cmd_fmt_string finfo po#loc x kind optlen fmtargs
 
+  | XPOTrustedOsCmdFmtArgString (x, quotes, optlen) ->
+     discharge_trusted_os_cmd_fmt_arg_string finfo po#loc x quotes optlen
+
   | XPOOutputFormatString x ->
      discharge_output_format_string finfo po#loc x
 

From 24369a90101e2a913439d77faf55fbb27caf3339 Mon Sep 17 00:00:00 2001
From: Henny Sipma 
Date: Thu, 11 Jun 2026 18:44:20 -0700
Subject: [PATCH 15/15] CHB: violation discharge for tainted string

---
 CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml | 3 ++-
 CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml         | 6 ++++++
 CodeHawk/CHB/bchlib/bCHVersion.ml                     | 4 ++--
 3 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml
index 1663e3b3..592b7065 100644
--- a/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml
+++ b/CodeHawk/CHB/bchlib/bCHAttributesFunctionSemantics.ml
@@ -1117,7 +1117,8 @@ let convert_b_attributes_to_function_conditions
 
   List.fold_left (fun ((xpre, xside, xpost, xepost, xqual) as acc) attr ->
       match attr with
-      | Attr ("access", attrparams) ->
+      | Attr (("access" | "chk_access"), attrparams) ->
+         (* keep chk_access for now for back-compatibility reasons *)
          let pre = get_access_preconditions name fparameters attrparams in
          let side = get_access_sideeffect name fparameters attrparams in
          (pre @ xpre, side @ xside, xpost, xepost, xqual)
diff --git a/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml b/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml
index 8275358b..0bfeffdd 100644
--- a/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml
+++ b/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml
@@ -408,8 +408,14 @@ let trusted_os_cmd_fmt_arg_string_return_value_postcondition
            | XXTrustedOsCmdString (ReturnValue _) -> true
            | XXTrustedString (ReturnValue _) -> true
            | _ -> false in
+         let is_violated post =
+           match post with
+           | XXTainted (ReturnValue _) -> true
+           | _ -> false in
          if List.exists is_trusted ctinfo#get_postconditions then
            Discharged ("return value of " ^ ctinfo#get_name ^ " is trusted")
+         else if List.exists is_violated ctinfo#get_postconditions then
+           Violated ("return value of " ^ ctinfo#get_name ^ " is potentially tainted")
          else
            Open)
        ~error:(fun _ -> Open)
diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml
index 6d19fb6f..ff5e0060 100644
--- a/CodeHawk/CHB/bchlib/bCHVersion.ml
+++ b/CodeHawk/CHB/bchlib/bCHVersion.ml
@@ -95,8 +95,8 @@ end
 
 
 let version = new version_info_t 
-  ~version:"0.6.0_20260610"
-  ~date:"2026-06-10"
+  ~version:"0.6.0_20260611"
+  ~date:"2026-06-11"
   ~licensee: None
   ~maxfilesize: None
   ()