Proofobligations

CodeHawk/CHB/bchanalyze/bCHAnalyzeApp.ml

@@ -99,6 +99,45 @@ let no_lineq = ref []
 let add_no_lineq s = no_lineq := s :: !no_lineq
 
 
+(** Expands a list of function address hex strings with the direct application
+    callees of each function, as recorded in saved function info. Silently
+    skips functions whose info is not yet available (e.g. first analysis pass).
+    Emits a diagnostics log entry for every callee added. *)
+let expand_fns_with_callees (fns: string list) : string list =
+  List.fold_left
+    (fun acc faddr_str ->
+      match string_to_doubleword faddr_str with
+      | Error _ -> acc
+      | Ok faddr ->
+        let callees =
+          try
+            let finfo = load_function_info faddr in
+            List.filter_map
+              (fun ct ->
+                if ct#is_app_call then Some ct#get_app_address
+                else None)
+              finfo#get_callees
+          with _ -> []
+        in
+        List.fold_left
+          (fun acc2 callee ->
+            let s = callee#to_hex_string in
+            if List.mem s acc2 then
+              acc2
+            else
+              begin
+                log_diagnostics_result
+                  ~tag:"expand_fns_with_callees"
+                  __FILE__ __LINE__
+                  ["add callee: " ^ s ^ " of: " ^ faddr_str];
+                s :: acc2
+              end)
+          acc
+          callees)
+    fns
+    fns
+
+
 let analyze_x86_function faddr f count =
   let _ =
     if system_settings#show_function_timing then
@@ -173,7 +212,9 @@ let analyze_x86_function faddr f count =
 
 
 let analyze starttime =
-  let fns_included = included_functions () in
+  let fns_included =
+    let fns = included_functions () in
+    if fn_include_callees () then expand_fns_with_callees fns else fns in
   let fns_excluded = excluded_functions () in
   let count = ref 0 in
   let failedfunctions = ref [] in
@@ -409,7 +450,9 @@ let analyze_mips_function faddr f count =
 
 
 let analyze_mips starttime =
-  let fns_included = included_functions () in
+  let fns_included =
+    let fns = included_functions () in
+    if fn_include_callees () then expand_fns_with_callees fns else fns in
   let fns_excluded = excluded_functions () in
   let count = ref 0 in
   let failedfunctions = ref [] in
@@ -565,7 +608,9 @@ let analyze_arm_function faddr f count =
 
 
 let analyze_arm starttime =
-  let fns_included = included_functions () in
+  let fns_included =
+    let fns = included_functions () in
+    if fn_include_callees () then expand_fns_with_callees fns else fns in
   let fns_excluded = excluded_functions () in
   let count = ref 0 in
   let failedfunctions = ref [] in
@@ -678,7 +723,9 @@ let analyze_pwr_function
 
 
 let analyze_pwr (starttime: float) =
-  let fns_included = included_functions () in
+  let fns_included =
+    let fns = included_functions () in
+    if fn_include_callees () then expand_fns_with_callees fns else fns in
   let fns_excluded = excluded_functions () in
   let count = ref 0 in
   begin

CodeHawk/CHB/bchcmdline/bCHXBinaryAnalyzer.ml

@@ -6,7 +6,7 @@
 
    Copyright (c) 2005-2020 Kestrel Technology LLC
    Copyright (c) 2020      Henny Sipma
-   Copyright (c) 2021-2025 Aarno Labs LLC
+   Copyright (c) 2021-2026 Aarno Labs LLC
 
    Permission is hereby granted, free of charge, to any person obtaining a copy
    of this software and associated documentation files (the "Software"), to deal
@@ -189,6 +189,9 @@ let speclist =
      "exclude the function with the given address from the analysis");
     ("-fn_include", Arg.String (fun s -> include_function s),
      "include the function with the given address in the analysis");
+    ("-fn_include_callees",
+     Arg.Unit (fun () -> set_fn_include_callees ()),
+     "expand the set of functions to be analyzed with the callees of the included functions");
     ("-fn_no_lineq", Arg.String (fun s -> add_no_lineq s),
      "do not apply linear equality analysis to the function with the given address");
     ("-lineq_instr_cutoff",

CodeHawk/CHB/bchlib/bCHSystemSettings.ml

@@ -50,6 +50,11 @@ let exclude_function (s: string) = fns_excluded := s :: !fns_excluded
 let excluded_functions () = !fns_excluded
 
 
+let fn_include_callees = ref false
+let set_fn_include_callees () = fn_include_callees := true
+let fn_include_callees () = !fn_include_callees
+
+
 let arm_typingrules_settings = H.create 23
 
 let _ =

CodeHawk/CHB/bchlib/bCHSystemSettings.mli

@@ -42,3 +42,6 @@ val included_functions: unit -> string list
 
 val exclude_function: string -> unit
 val excluded_functions: unit -> string list
+
+val set_fn_include_callees: unit -> unit
+val fn_include_callees: unit -> bool

CodeHawk/CHB/bchlib/bCHVersion.ml

@@ -95,8 +95,8 @@ end
 
 
 let version = new version_info_t 
-  ~version:"0.6.0_20260418"
-  ~date:"2026-04-18"
+  ~version:"0.6.0_20260527"
+  ~date:"2026-05-27"
   ~licensee: None
   ~maxfilesize: None
   ()

CodeHawk/CHB/bchsummaries/so_functions/mkstemp64.xml

@@ -1,5 +1,4 @@
 <?xml version="1.0" encoding="utf-8"?>
-<?xml version="1.0" encoding="UTF-8"?>
 <codehawk-binary-analyzer>
   <reference href="http://pubs.opengroup.org/onlinepubs/000095399/"/>
   <header date="2020-04-28 23:28:35"/>

CodeHawk/CHB/bchsummaries/so_functions/popen.xml

@@ -33,7 +33,16 @@
     </api>
     <semantics>
       <io-actions/>
-      <preconditions/>
+      <preconditions>
+        <pre>
+          <math>
+            <apply>
+              <trusted-os-cmd-string/>
+              <ci>command</ci>
+            </apply>
+          </math>
+        </pre>
+      </preconditions>
       <postconditions>
 	<notnull-null/>
       </postconditions>