From fe6bdcba14bfc5c1225b21ad48605e0592c52108 Mon Sep 17 00:00:00 2001
From: Henny Sipma <hennysipma@mac.com>
Date: Mon, 9 Jun 2025 21:49:12 -0700
Subject: [PATCH 01/16] CHB:ARM:add disassembly support for FLDMIAX (arm)

---
 .../CHB/bchlibarm32/bCHDisassembleARMInstruction.ml  | 12 ++++++++++++
 .../bCHDisassembleARMInstructionTest.ml              |  4 ++++
 2 files changed, 16 insertions(+)

diff --git a/CodeHawk/CHB/bchlibarm32/bCHDisassembleARMInstruction.ml b/CodeHawk/CHB/bchlibarm32/bCHDisassembleARMInstruction.ml
index 64e1fb57..51d4faa7 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHDisassembleARMInstruction.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHDisassembleARMInstruction.ml
@@ -1703,6 +1703,18 @@ let parse_misc_6_type (instr: doubleword_int) (cond: int) =
      (* VMOV<c> <Dm>, <Rt>, <Rt2> *)
      VectorMoveDDS (c, VfpNone, rt WR, rt2 WR, rtd WR, dm RD)
 
+  (* FLDMIAX{<c>}{<q>}>Rn>{!},<dreglist> *)
+  (* <cc><6>01001DW1<rn><vd>1011<-imm7>1 *)
+  | (1, 1, 11) when (bv 22) = 0 && (bv 0) = 1 ->
+     let d = prefix_bit (bv 22) (b 15 12) in
+     let rnreg = get_arm_reg (b 19 16) in
+     let rn = arm_register_op rnreg in
+     let regs = (b 7 1) in
+     let rl = arm_extension_register_list_op XDouble d regs in
+     let mem = mk_arm_mem_multiple_op ~size:8 rnreg regs in
+     (* FLXMIAX<c>, <list> *)
+     FLoadMultipleIncrementAfter (false, c, rn RD, rl WR, mem RD)
+
   (* <cc><6>01D11<13><vd><10><-imm8-> *)   (* VPOP - A2 *)
   | (1, 3, 10) when (b 19 16) = 13 ->
      let d = postfix_bit (bv 22) (b 15 12) in
diff --git a/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHDisassembleARMInstructionTest.ml b/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHDisassembleARMInstructionTest.ml
index 279207be..3bf5e0c1 100644
--- a/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHDisassembleARMInstructionTest.ml
+++ b/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHDisassembleARMInstructionTest.ml
@@ -197,6 +197,10 @@ let arm_pc_relative () =
 
 let arm_vector () =
   let tests = [
+      ("FLDMIAX",                     "210b90ec",
+       "FLDMIAX        R0, {D0,D1,D2,D3,D4,D5,D6,D7,D8,D9,D10,D11,D12,D13,D14,D15}");
+      ("FSTMIAX",                     "210b80ec",
+       "FSTMIAX        R0, {D0,D1,D2,D3,D4,D5,D6,D7,D8,D9,D10,D11,D12,D13,D14,D15}");
       ("VDUP.32",                     "474cfcf3", "VDUP.32        Q10, D7[1]");
       ("VDUP.32-scalar",              "622cfcf3", "VDUP.32        Q9, D18[1]");
       ("VEOR-Q",                      "746106f3", "VEOR           Q3, Q3, Q10");

From a1ebec48d3f4857499dfcbb0a9c9778ac219845d Mon Sep 17 00:00:00 2001
From: Henny Sipma <hennysipma@mac.com>
Date: Mon, 9 Jun 2025 22:53:09 -0700
Subject: [PATCH 02/16] CHB:ARM:disassembly for STCL/STC2/LDC2

---
 .../bCHDisassembleARMInstruction.ml           | 38 +++++++++++++++++++
 .../bCHDisassembleThumbInstruction.ml         |  4 +-
 .../bCHDisassembleARMInstructionTest.ml       |  5 ++-
 3 files changed, 44 insertions(+), 3 deletions(-)

diff --git a/CodeHawk/CHB/bchlibarm32/bCHDisassembleARMInstruction.ml b/CodeHawk/CHB/bchlibarm32/bCHDisassembleARMInstruction.ml
index 51d4faa7..7482df6f 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHDisassembleARMInstruction.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHDisassembleARMInstruction.ml
@@ -1836,6 +1836,23 @@ let parse_misc_6_type (instr: doubleword_int) (cond: int) =
      (* FSTMIAX<c> <Rn>, <list> *)
      FStoreMultipleIncrementAfter (false, c, rn RD, rl RD, mem WR)
 
+  (* <cc><6>01D10<rn><cd><cp><-imm8-> *)   (* STCL - A1 *)
+  | (1, 2, 1) ->
+      let isindex = (bv 24) = 1 in
+      let isadd = (bv 23) = 1 in
+      let iswback = (bv 21) = 1 in
+      let islong = (bv 22) = 1 in
+      let crd = b 15 12 in
+      let coproc = b 11 8 in
+      let imm32 = 4 * (b 7 0) in
+      let offset = ARMImmOffset imm32 in
+      let rnreg = get_arm_reg (b 19 16) in
+      let mem =
+        mk_arm_offset_address_op
+          ~align:4 rnreg offset ~isadd ~isindex ~iswback in
+      (* STC{L}<c> <coproc>, <CRd>, [<Rn>, #+/-<imm>]{!} *)
+      StoreCoprocessor (islong, false, c, coproc, crd, mem WR, None)
+
   (* <cc><6>01D00<rn><vd><11><-imm8-> *)   (* VSTM - A1-wb *)
   | (1, 2, 11) when (bv 0) = 0 ->
      let d = prefix_bit (bv 22) (b 15 12) in
@@ -4750,6 +4767,27 @@ let parse_cond15 (instr: doubleword_int) (iaddr: doubleword_int) =
      (* BLX <label> *)
      BranchLinkExchange(cc, tgtop)
 
+  (* <15>110PUDW0<rn><cd><cp><-imm8-> *)(* STC2{L}<c> <coproc>,<CRd>,[<Rn>, #+/-imm] *)
+  | (25, (2 | 3), 1, 0, 0) ->
+      let isindex = (bv 24) = 1 in
+      let isadd = (bv 23) = 1 in
+      let iswback = (bv 21) = 1 in
+      let islong = (bv 22) = 1 in
+      let crd = b 15 12 in
+      let coproc = b 11 8 in
+      let imm32 = 4 * (b 7 0) in
+      let offset = ARMImmOffset imm32 in
+      let rnreg = get_arm_reg (b 19 16) in
+      let mem =
+        mk_arm_offset_address_op
+          ~align:4 rnreg offset ~isadd ~isindex ~iswback in
+      if (bv 20) = 0 then
+        (* STC{L}<c> <coproc>, <CRd>, [<Rn>, #+/-<imm>]{!} *)
+        StoreCoprocessor (islong, true, cc, coproc, crd, mem WR, None)
+      else
+        (* LDC{L}<c> <coproc>, <CRd>, [<Rn>, #+-<imm>}{!} *)
+        LoadCoprocessor (islong, true, cc, coproc, crd, mem RD, None)
+
   | (x, y, z, q, v) ->
      NotRecognized (
          "arm:cond15:"
diff --git a/CodeHawk/CHB/bchlibarm32/bCHDisassembleThumbInstruction.ml b/CodeHawk/CHB/bchlibarm32/bCHDisassembleThumbInstruction.ml
index a934dcb0..d4417dfe 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHDisassembleThumbInstruction.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHDisassembleThumbInstruction.ml
@@ -828,10 +828,10 @@ let parse_thumb32_29_2
           ~align:4 rnreg offset ~isadd ~isindex ~iswback in
       if (bv 20) = 0 then
         (* STC{L}<c> <coproc>, <CRd>, [<Rn>, #+/-<imm>]{!} *)
-        StoreCoprocessor (islong, false, cc, coproc, crd, mem WR, None)
+        StoreCoprocessor (islong, true, cc, coproc, crd, mem WR, None)
       else
         (* LDC{L}<c> <coproc>, <CRd>, [<Rn>, #+-<imm>}{!} *)
-        LoadCoprocessor (islong, false, cc, coproc, crd, mem RD, None)
+        LoadCoprocessor (islong, true, cc, coproc, crd, mem RD, None)
   else
     let selector = b 24 23 in
     let isz = b 21 20 in
diff --git a/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHDisassembleARMInstructionTest.ml b/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHDisassembleARMInstructionTest.ml
index 3bf5e0c1..7395fc64 100644
--- a/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHDisassembleARMInstructionTest.ml
+++ b/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHDisassembleARMInstructionTest.ml
@@ -48,7 +48,7 @@ open BCHDisassembleARMInstruction
 
 
 let testname = "bCHDisassembleARMInstructionTest"
-let lastupdated = "2024-10-31"
+let lastupdated = "2025-06-09"
 
 
 let make_dw (s: string) = TR.tget_ok (string_to_doubleword s)
@@ -78,6 +78,7 @@ let arm_basic () =
       ("CMP",    "010050e3", "CMP            R0, #1");
       ("CMPNE",  "00005111", "CMPNE          R1, R0");
       ("DMB",    "5bf07ff5", "DMB            ISH");
+      ("LDC2",   "0181b0fc", "LDC2           p1, c8, [R0],#4");
       ("LDCL",   "02a1f0ec", "LDCL           p1, c10, [R0],#8");
       ("LDM",    "1c5091e8", "LDM            R1, {R2,R3,R4,R12,LR}");
       ("LDR",    "001094e5", "LDR            R1, [R4]");
@@ -125,6 +126,8 @@ let arm_basic () =
       ("SMULL",  "9310c7e0", "SMULL          R1, R7, R3, R0");
       ("SMULWB", "a90523e1", "SMULWB         R3, R9, R5");
       ("SMULWT", "e00c23e1", "SMULWT         R3, R0, R12");
+      ("STC2",   "0181a0fc", "STC2           p1, c8, [R0],#4");
+      ("STCL",   "0201e0ec", "STCL           p1, c0, [R0],#8");
       ("STM",    "1a0080e8", "STM            R0, {R1,R3,R4}");
       ("STMDA",  "030003e8", "STMDA          R3, {R0,R1}");
       ("STMIB",  "21078de9", "STMIB          SP, {R0,R5,R8,R9,R10}");

From b1cb2688fd30013895373be07b9bc6914a51ebf4 Mon Sep 17 00:00:00 2001
From: Henny Sipma <hennysipma@mac.com>
Date: Fri, 13 Jun 2025 15:30:02 -0700
Subject: [PATCH 03/16] CHB: add support for global variable as memory base

---
 CodeHawk/CHB/bchlib/bCHFloc.ml | 106 +++++++++++++++++++--------------
 1 file changed, 61 insertions(+), 45 deletions(-)

diff --git a/CodeHawk/CHB/bchlib/bCHFloc.ml b/CodeHawk/CHB/bchlib/bCHFloc.ml
index c759e605..8da29235 100644
--- a/CodeHawk/CHB/bchlib/bCHFloc.ml
+++ b/CodeHawk/CHB/bchlib/bCHFloc.ml
@@ -1284,61 +1284,77 @@ object (self)
     else if self#env#is_memory_variable v then
       let memref_r = self#env#get_memory_reference v in
       let memoff_r = self#env#get_memvar_offset v in
-      let basevar_r =
-        TR.tbind
-          ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
-          (fun memref ->
-            match memref#get_base with
-            | BaseVar v -> Ok v
-            | b ->
-               Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
-                      ^ "memory-base: " ^ (p2s (memory_base_to_pretty b))])
-          memref_r in
-      let basevar_type_r =
-        TR.tbind
-          ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
-          self#get_variable_type
-          basevar_r in
       TR.tbind
         ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
-        (fun basevartype ->
-          TR.tbind
-            (fun memoff ->
-              match memoff with
-              | NoOffset when is_pointer basevartype ->
-                 Ok (ptr_deref basevartype)
-              | ConstantOffset (n, NoOffset) when is_pointer basevartype ->
-                 let symmemoff_r =
-                   address_memory_offset
-                     (ptr_deref basevartype) (num_constant_expr n) in
+        (fun memref ->
+          match memref#get_base with
+          | BGlobal ->
+             (match memoff_r with
+              | Ok (ConstantOffset (num, NoOffset)) ->
+                 let gvaddr = numerical_mod_to_doubleword num in
+                 if memmap#has_location gvaddr then
+                   let gloc = memmap#get_location gvaddr in
+                   Ok (gloc#btype)
+                 else
+                   Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                          ^ "no global location found for address "
+                          ^ gvaddr#to_hex_string]
+              | _ ->
+                 Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                        ^ "not a constant offset"])
+          | _ ->
+             let basevar_r =
+               match memref#get_base with
+               | BaseVar v -> Ok v
+               | b ->
+                  Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                         ^ "memory-base: " ^ (p2s (memory_base_to_pretty b))] in
+             let basevar_type_r =
+               TR.tbind
+                 ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+                 self#get_variable_type
+                 basevar_r in
+             TR.tbind
+               ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+               (fun basevartype ->
                  TR.tbind
-                   ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
-                         ^ "basevar type: " ^ (btype_to_string basevartype)
-                         ^ "; offset: " ^ n#toString)
-                   (fun off ->
-                     match off with
+                   (fun memoff ->
+                     match memoff with
+                     | NoOffset when is_pointer basevartype ->
+                        Ok (ptr_deref basevartype)
+                     | ConstantOffset (n, NoOffset) when is_pointer basevartype ->
+                        let symmemoff_r =
+                          address_memory_offset
+                            (ptr_deref basevartype) (num_constant_expr n) in
+                        TR.tbind
+                          ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                                ^ "basevar type: " ^ (btype_to_string basevartype)
+                                ^ "; offset: " ^ n#toString)
+                          (fun off ->
+                            match off with
+                            | FieldOffset ((fname, ckey), NoOffset) ->
+                               let cinfo = get_compinfo_by_key ckey in
+                               let finfo = get_compinfo_field cinfo fname in
+                               Ok finfo.bftype
+                            | _ ->
+                               Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                                      ^ "symbolic offset: "
+                                      ^ (memory_offset_to_string off)
+                                      ^ " with basevar type: "
+                                      ^ (btype_to_string basevartype)
+                                      ^ " not yet handled"])
+                          symmemoff_r
                      | FieldOffset ((fname, ckey), NoOffset) ->
                         let cinfo = get_compinfo_by_key ckey in
                         let finfo = get_compinfo_field cinfo fname in
                         Ok finfo.bftype
                      | _ ->
                         Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
-                               ^ "symbolic offset: "
-                               ^ (memory_offset_to_string off)
-                               ^ " with basevar type: "
-                               ^ (btype_to_string basevartype)
+                               ^ "memoff: " ^ (memory_offset_to_string memoff)
                                ^ " not yet handled"])
-                   symmemoff_r
-              | FieldOffset ((fname, ckey), NoOffset) ->
-                 let cinfo = get_compinfo_by_key ckey in
-                 let finfo = get_compinfo_field cinfo fname in
-                 Ok finfo.bftype
-              | _ ->
-                 Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
-                        ^ "memoff: " ^ (memory_offset_to_string memoff)
-                        ^ " not yet handled"])
-            memoff_r)
-        basevar_type_r
+                   memoff_r)
+               basevar_type_r)
+      memref_r
     else if self#f#env#is_return_value v then
       let callsite_r = self#f#env#get_call_site v in
       TR.tbind

From 3f08ad766147a3823260b0ba35ab206159373a12 Mon Sep 17 00:00:00 2001
From: Henny Sipma <hennysipma@mac.com>
Date: Mon, 23 Jun 2025 17:32:25 -0700
Subject: [PATCH 04/16] CHB:summaries: introduce more struct typedefs

---
 CodeHawk/CHB/bchsummaries/so_functions/getgrgid.xml | 2 +-
 CodeHawk/CHB/bchsummaries/so_functions/getgrnam.xml | 2 +-
 CodeHawk/CHB/bchsummaries/so_functions/getpwnam.xml | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/CodeHawk/CHB/bchsummaries/so_functions/getgrgid.xml b/CodeHawk/CHB/bchsummaries/so_functions/getgrgid.xml
index 1ffba995..8741f26b 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/getgrgid.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/getgrgid.xml
@@ -18,7 +18,7 @@
       <par loc="stack" name="gid" nr="1">
         <type>gid_t</type>
       </par>
-      <returntype><ptr>group</ptr></returntype>
+      <returntype><ptr>ch_group</ptr></returntype>
     </api>
     <semantics>
       <io-actions/>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/getgrnam.xml b/CodeHawk/CHB/bchsummaries/so_functions/getgrnam.xml
index 6da928e3..ef3c15d8 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/getgrnam.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/getgrnam.xml
@@ -21,7 +21,7 @@
         <type><ptr>char</ptr></type>
 	<pre><deref-read-nt/></pre>
       </par>
-      <returntype><ptr>group</ptr></returntype>
+      <returntype><ptr>ch_group</ptr></returntype>
     </api>
     <semantics>
       <io-actions/>
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/getpwnam.xml b/CodeHawk/CHB/bchsummaries/so_functions/getpwnam.xml
index 88fbb7f6..3f6617e6 100644
--- a/CodeHawk/CHB/bchsummaries/so_functions/getpwnam.xml
+++ b/CodeHawk/CHB/bchsummaries/so_functions/getpwnam.xml
@@ -19,7 +19,7 @@
         <type><ptr>char</ptr></type>
 	<pre><deref-read/></pre>
       </par>
-      <returntype><ptr>passwd</ptr></returntype>
+      <returntype><ptr>ch_passwd</ptr></returntype>
     </api>
     <semantics>
       <io-actions/>

From 4471615b4eb390f86409e3ec1295cc1609f2f92f Mon Sep 17 00:00:00 2001
From: Henny Sipma <hennysipma@mac.com>
Date: Mon, 23 Jun 2025 17:33:58 -0700
Subject: [PATCH 05/16] CHB:ARM: account for conditional return with BX

---
 CodeHawk/CHB/bchlibarm32/bCHConstructARMFunction.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CodeHawk/CHB/bchlibarm32/bCHConstructARMFunction.ml b/CodeHawk/CHB/bchlibarm32/bCHConstructARMFunction.ml
index 6c6ab00d..43fc688b 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHConstructARMFunction.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHConstructARMFunction.ml
@@ -163,7 +163,7 @@ let get_successors
         | Branch (_, op, _)
           | BranchExchange (_, op)
              when op#is_register && op#get_register = ARLR ->
-           (next ())
+           (next ()) @ [wordmax]
 
         (* return via Move *)
         | Move (_, ACCAlways, dst, src, _, _)

From b4d86519e467dce33b14d31117daf4ebac1ab4af Mon Sep 17 00:00:00 2001
From: Henny Sipma <hennysipma@mac.com>
Date: Mon, 23 Jun 2025 17:34:29 -0700
Subject: [PATCH 06/16] CHB:ARM:add c expressions to instruction predicate

---
 CodeHawk/CHB/bchlib/bCHVersion.ml             |  4 +-
 .../bchlibarm32/bCHARMInstructionAggregate.ml |  2 +
 .../CHB/bchlibarm32/bCHFnARMDictionary.ml     | 43 ++++++++++---------
 3 files changed, 27 insertions(+), 22 deletions(-)

diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml
index 4403b540..26730111 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_20250608"
-  ~date:"2025-06-08"
+  ~version:"0.6.0_20250623"
+  ~date:"2025-06-23"
   ~licensee: None
   ~maxfilesize: None
   ()
diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMInstructionAggregate.ml b/CodeHawk/CHB/bchlibarm32/bCHARMInstructionAggregate.ml
index 66b41a8f..7fed24c4 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHARMInstructionAggregate.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHARMInstructionAggregate.ml
@@ -149,6 +149,8 @@ object (self)
         STR "Aggregate of ";
         INT (List.length self#instrs);
         STR " with anchor ";
+        self#anchor#get_address#toPretty;
+        STR " ";
         self#anchor#toPretty;
         STR ": ";
         STR (arm_aggregate_kind_to_string self#kind)]
diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml
index 95d48570..d9b9afa4 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml
@@ -233,24 +233,6 @@ object (self)
         else
           xpr in
       simplify_xpr xpr in
-    let add_instr_condition
-          (tags: string list)
-          (args: int list)
-          (x: xpr_t): (string list) * (int list) =
-      let _ =
-        if (List.length tags) = 0 then
-          raise
-            (BCH_failure
-               (LBLOCK [STR "Empty tag list in add_instr_condition"])) in
-      let argslen = List.length args in
-      let xtag = (List.hd tags) ^ "xx" in
-      let ictag = "ic:" ^ (string_of_int argslen) in
-      let icrtag = "icr:" ^ (string_of_int (argslen + 1)) in
-      let tags = xtag :: ((List.tl tags) @ [ictag; icrtag]) in
-      let xneg = XOp (XLNot, [x]) in
-      let xneg = simplify_xpr xneg in
-      let args = args @ [xd#index_xpr x; xd#index_xpr xneg] in
-      (tags, args) in
 
     let flagrdefs: int list =
       let flags_used = get_arm_flags_used instr#get_opcode in
@@ -552,8 +534,29 @@ object (self)
       | _ when instr#is_condition_covered -> ([tagstring], args)
       | c when is_cond_conditional c && floc#has_test_expr ->
          let csetter = floc#f#get_associated_cc_setter floc#cia in
-         let tcond = rewrite_test_expr csetter floc#get_test_expr in
-         add_instr_condition [tagstring] args tcond
+         let txpr = floc#get_test_expr in
+         let fxpr = simplify_xpr (XOp (XLNot, [txpr])) in
+         let tcond = rewrite_test_expr csetter txpr in
+         let fcond = rewrite_test_expr csetter fxpr in
+         let ctcond_r = floc#convert_xpr_to_c_expr ~size:(Some 4) tcond in
+         let cfcond_r = floc#convert_xpr_to_c_expr ~size:(Some 4) fcond in
+         let rdefs = (get_all_rdefs txpr) @ (get_all_rdefs tcond) in
+         let argslen = List.length args in
+         let xtag = "xxcc" ^ (string_repeat "r" (List.length rdefs)) in
+         let xtag = tagstring ^ xtag in
+         let newargs = [
+             index_xpr (Ok tcond);
+             index_xpr (Ok fcond);
+             index_xpr ctcond_r;
+             index_xpr cfcond_r
+           ] @ rdefs in
+         let ictag = "ic:" ^ (string_of_int argslen) in
+         let icrtag = "icr:" ^ (string_of_int (argslen + 1)) in
+         let icctag = "icc:" ^ (string_of_int (argslen + 2)) in
+         let iccrtag = "iccr:" ^ (string_of_int (argslen + 3)) in
+         let tags = xtag :: [ictag; icrtag; icctag; iccrtag] in
+         let args = args @ newargs in
+         (tags, args)
       | _ -> (tagstring :: ["uc"], args) in
 
     let add_optional_subsumption (tags: string list): string list =

From 733bd84a445dc36dc62dc8899b2252b5ce5e80b4 Mon Sep 17 00:00:00 2001
From: Henny Sipma <hennysipma@mac.com>
Date: Wed, 25 Jun 2025 16:42:07 -0700
Subject: [PATCH 07/16] CHB:ARM: add conditional expressions

---
 .../CHB/bchlibarm32/bCHARMConditionalExpr.ml  | 26 +++++++++++++++++++
 1 file changed, 26 insertions(+)

diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMConditionalExpr.ml b/CodeHawk/CHB/bchlibarm32/bCHARMConditionalExpr.ml
index d804228f..8f2ba18b 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHARMConditionalExpr.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHARMConditionalExpr.ml
@@ -94,6 +94,20 @@ module TR = CHTraceResult
       CMP x, 0 GE            (x >= 0 & x < e31)                (N = 0, V = 0)
 
                HI            (x > y)   (C = 1 and Z = 0)
+
+
+   CMN x, y:
+   ---------
+       (result, carry, overflow) = AddWithCarry(x, y, 0)
+       N = result<31>    signed(x + y) < 0
+       Z = result == 0   x + y = 0 , mod(x + y) = e32
+       C = carry         unsigned(x + y) >= e32
+       V = overflow      signed(x + y) >= e31 \/ signed(x + y) <= -e31
+
+    setter     condition    predicate (on unsigned)
+    CMN x, 1   LE           x < 0
+    CMN x, 1   GT           x >= 0
+
  *)
 
 let x2p = xpr_formatter#pr_expr
@@ -178,6 +192,9 @@ let cc_expr
       (testopc: arm_opcode_t)
       (cc: arm_opcode_cc_t): (bool * xpr_t option * arm_operand_int list) =
   let found = ref true in
+  let is_one (x: xpr_t) =
+    match x with
+    | XConst (IntConst n) -> n#equal CHNumerical.numerical_one | _ -> false in
   let (expr, opsused) =
     match (testopc, cc) with
 
@@ -189,6 +206,9 @@ let cc_expr
     | (BitwiseAnd (true, ACCAlways, _, x, y, _), ACCEqual) ->
        (XOp (XEq, [XOp (XBAnd, [vu x; vu y]); zero_constant_expr]), [x; y])
 
+    | (BitwiseAnd (true, ACCAlways, _, x, y, _), ACCNotEqual) ->
+       (XOp (XNe, [XOp (XBAnd, [vu x; vu y]); zero_constant_expr]), [x; y])
+
     (* ---------------------------------------------------------- Compare --- *)
 
     | (Compare (ACCAlways, x, y, _), ACCEqual) ->
@@ -304,6 +324,12 @@ let cc_expr
     | (CompareNegative (ACCAlways, x, y), ACCUnsignedHigher) ->
        (XOp (XGt, [XOp (XPlus, [vu x; vu y]); max32_constant_expr]), [x; y])
 
+    | (CompareNegative (ACCAlways, x, y), ACCSignedGT) when (is_one (v y)) ->
+       (XOp (XGe, [v x; zero_constant_expr]), [x; y])
+
+    | (CompareNegative (ACCAlways, x, y), ACCSignedLE) when (is_one (v y)) ->
+       (XOp (XLt, [v x; zero_constant_expr]), [x; y])
+
     | (CompareNegative (ACCAlways, x, y), ACCCarryClear) ->
        (XOp (XLOr, [XOp (XLt, [XOp (XPlus, [v x; v y]); zero_constant_expr]);
                     XOp (XGe, [v x; zero_constant_expr])]), [x; y])

From 42fd6426be0510242cea3ff6d6705c7759852048 Mon Sep 17 00:00:00 2001
From: Henny Sipma <hennysipma@mac.com>
Date: Wed, 25 Jun 2025 16:46:10 -0700
Subject: [PATCH 08/16] CHB:ARM: record presence of instruction predicates in
 analysis results

---
 CodeHawk/CHB/bchlib/bCHVersion.ml             |  4 ++--
 .../CHB/bchlibarm32/bCHARMAnalysisResults.ml  | 22 ++++++++++++++++++-
 .../bchlibarm32/bCHARMAssemblyInstruction.ml  | 10 ++++++++-
 .../CHB/bchlibarm32/bCHARMOpcodeRecords.ml    |  2 +-
 CodeHawk/CHB/bchlibarm32/bCHARMTypes.mli      |  2 ++
 .../bchlibarm32/bCHFnARMTypeConstraints.ml    | 17 ++++++++++++++
 6 files changed, 52 insertions(+), 5 deletions(-)

diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml
index 26730111..9552c8de 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_20250623"
-  ~date:"2025-06-23"
+  ~version:"0.6.0_20250625"
+  ~date:"2025-06-25"
   ~licensee: None
   ~maxfilesize: None
   ()
diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml b/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml
index 97c8e8e5..287bc44a 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml
@@ -72,12 +72,32 @@ object (self)
     let loc = ctxt_string_to_location faddr ctxtiaddr in
     let floc = get_floc loc in
     let espoffset = floc#get_stackpointer_offset "arm" in
+    let has_control_flow =
+      instr#has_opcode_condition
+      && (match instr#get_opcode with
+          | Branch _ | BranchExchange _ -> false
+          | _ -> true)
+      && (Option.is_none instr#is_in_aggregate) in
     begin
       arm_dictionary#write_xml_arm_opcode node instr#get_opcode;
       id#write_xml_instr node instr floc;
       id#write_xml_sp_offset node espoffset;
       arm_dictionary#write_xml_arm_bytestring
-        node (byte_string_to_printed_string instr#get_instruction_bytes)
+        node (byte_string_to_printed_string instr#get_instruction_bytes);
+      (if has_control_flow then
+         let optcc = instr#get_opcode_condition in
+         match optcc with
+         | Some cc ->
+            let pcc = BCHARMOpcodeRecords.get_cond_mnemonic_extension cc in
+            let _ = node#setAttribute "brcc" pcc in
+            if floc#has_test_expr then
+              let csetter = floc#f#get_associated_cc_setter floc#cia in
+              node#setAttribute "brsetter" csetter
+            else
+              ()
+         | _ -> ()
+       else
+         ())
     end
 
   method private write_xml_instructions (node:xml_element_int) =
diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstruction.ml b/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstruction.ml
index c16982d8..1ca00f2b 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstruction.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstruction.ml
@@ -4,7 +4,7 @@
    ------------------------------------------------------------------------------
    The MIT License (MIT)
 
-   Copyright (c) 2021-2024  Aarno Labs, LLC
+   Copyright (c) 2021-2025  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
@@ -87,8 +87,16 @@ object (self)
 
   method is_in_aggregate = in_aggregate
 
+  method has_opcode_condition =
+    BCHARMOpcodeRecords.is_opcode_conditional opcode
+
+  method get_opcode_condition =
+    BCHARMOpcodeRecords.get_arm_opcode_condition opcode
+
+  (* applies only to Thumb IT instruction *)
   method set_block_condition = blockcondition <- true
 
+  (* applies only to Thumb IT instruction *)
   method is_block_condition = blockcondition
 
   method set_condition_covered_by (iaddr: doubleword_int) =
diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMOpcodeRecords.ml b/CodeHawk/CHB/bchlibarm32/bCHARMOpcodeRecords.ml
index e6d0d1d2..eea9de06 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHARMOpcodeRecords.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHARMOpcodeRecords.ml
@@ -198,7 +198,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t =
       operands = [ rd; rn; imm ];
       flags_set = if s then [APSR_N; APSR_Z; APSR_C] else [];
       ccode = Some c;
-      ida_asm = (fun f -> f#opscc ~thumbw:tw "AND" c [rd; rn; imm])
+      ida_asm = (fun f -> f#opscc ~thumbw:tw "AND" ~writeback:s c [rd; rn; imm])
     }
   | BitwiseBitClear (s, c, rd, rn, rm, tw) -> {
       mnemonic = "BIC";
diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMTypes.mli b/CodeHawk/CHB/bchlibarm32/bCHARMTypes.mli
index dae4ee32..b1c09332 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHARMTypes.mli
+++ b/CodeHawk/CHB/bchlibarm32/bCHARMTypes.mli
@@ -1423,6 +1423,7 @@ class type arm_assembly_instruction_int =
     method get_instruction_bytes: string
     method get_bytes_ashexstring: string
     method get_non_code_block: not_code_t
+    method get_opcode_condition: arm_opcode_cc_t option
     method condition_covered_by: doubleword_int
 
     (* predicates *)
@@ -1438,6 +1439,7 @@ class type arm_assembly_instruction_int =
     method is_aggregate_entry: bool
     method is_aggregate_exit: bool
     method is_aggregate_anchor: bool
+    method has_opcode_condition: bool
 
     (* i/o *)
     method write_xml: xml_element_int -> unit
diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml
index b02977d5..23e1af8a 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml
@@ -393,6 +393,23 @@ object (self)
 
        end
 
+    | BitwiseNot (_, _, rd, rm, _) ->
+       let rdreg = rd#to_register in
+       let lhstypevar = mk_reglhs_typevar rdreg faddr iaddr in
+       let rmdefs = get_variable_rdefs_r (rm#to_variable floc) in
+       let rmreg = rm#to_register in
+       begin
+         List.iter (fun rmsym ->
+             let rmaddr = rmsym#getBaseName in
+             let rmtypevar = mk_reglhs_typevar rmreg faddr rmaddr in
+             let rmtypeterm = mk_vty_term rmtypevar in
+             let lhstypeterm = mk_vty_term lhstypevar in
+             begin
+               log_subtype_constraint __LINE__ "MVN-rdef" rmtypeterm lhstypeterm;
+               store#add_subtype_constraint rmtypeterm lhstypeterm
+             end) rmdefs
+       end
+
     | BitwiseOr (_, _, rd, rn, _, _) ->
        let rdreg = rd#to_register in
        let lhstypevar = mk_reglhs_typevar rdreg faddr iaddr in

From efb71d7371133fe4f71eb96cbde0ae256e4b7533 Mon Sep 17 00:00:00 2001
From: Henny Sipma <hennysipma@mac.com>
Date: Mon, 30 Jun 2025 13:23:30 -0700
Subject: [PATCH 09/16] fix documentation issues

---
 CodeHawk/CH/chlib/cHNumerical.mli             |   2 +-
 CodeHawk/CH/chutil/cHPrettyUtil.mli           |   2 +-
 CodeHawk/CH/chutil/cHTraceResult.mli          |   4 +-
 CodeHawk/CHB/bchlib/bCHBCTypeUtil.mli         |   6 +-
 CodeHawk/CHB/bchlib/bCHBCTypes.mli            |   8 +-
 CodeHawk/CHB/bchlib/bCHBasicTypes.mli         |   1 +
 CodeHawk/CHB/bchlib/bCHByteUtilities.mli      |   4 +-
 CodeHawk/CHB/bchlib/bCHCPURegisters.mli       |   4 +-
 .../CHB/bchlib/bCHConstantDefinitions.mli     |   8 +-
 CodeHawk/CHB/bchlib/bCHDemangler.mli          |   6 +-
 CodeHawk/CHB/bchlib/bCHFtsParameter.mli       |   2 +-
 CodeHawk/CHB/bchlib/bCHFunctionInfo.mli       |   2 +-
 CodeHawk/CHB/bchlib/bCHImmediate.mli          |   2 +-
 CodeHawk/CHB/bchlib/bCHLibTypes.mli           | 104 ++++++++++--------
 CodeHawk/CHB/bchlib/bCHLocation.mli           |  11 +-
 CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.mli |   2 +-
 CodeHawk/CHB/bchlib/bCHUtilities.mli          |   4 +-
 .../bchlibmips32/bCHMIPSDisassemblyUtils.mli  |   2 +-
 CodeHawk/CHB/bchlibpower32/bCHPowerTypes.mli  |   2 +-
 .../CHB/bchlibx86/bCHAssemblyInstructions.mli |   2 +-
 .../CHB/bchlibx86/bCHConditionalJumpExpr.mli  |   6 +-
 .../bchlibx86/bCHDisassembleInstruction.mli   |   2 +-
 .../CHB/bchlibx86/bCHDisassemblyUtils.mli     |   2 +-
 CodeHawk/CHB/bchlibx86/bCHLibx86Types.mli     |  26 ++---
 CodeHawk/CHC/cchanalyze/cCHAnalysisTypes.mli  |  20 ++--
 CodeHawk/CHC/cchlib/cCHCAttributes.mli        |   2 +-
 CodeHawk/CHC/cchlib/cCHLibTypes.mli           |   4 +-
 CodeHawk/CHC/cchpre/cCHPreTypes.mli           |  18 +--
 28 files changed, 135 insertions(+), 123 deletions(-)

diff --git a/CodeHawk/CH/chlib/cHNumerical.mli b/CodeHawk/CH/chlib/cHNumerical.mli
index 5079710e..4db6ca00 100644
--- a/CodeHawk/CH/chlib/cHNumerical.mli
+++ b/CodeHawk/CH/chlib/cHNumerical.mli
@@ -138,7 +138,7 @@ val mkNumericalFromInt64 : int64 -> numerical_t
 val mkNumericalFromString: string -> numerical_t
 
 
-(** [mkNumericalPowerOf2 n] returns the numerical for 2^n] *)
+(** [mkNumericalPowerOf2 n] returns the numerical for [2^n] *)
 val mkNumericalPowerOf2: int -> numerical_t
 
 
diff --git a/CodeHawk/CH/chutil/cHPrettyUtil.mli b/CodeHawk/CH/chutil/cHPrettyUtil.mli
index 47f90bd9..489f20d0 100644
--- a/CodeHawk/CH/chutil/cHPrettyUtil.mli
+++ b/CodeHawk/CH/chutil/cHPrettyUtil.mli
@@ -70,7 +70,7 @@ val fixed_length_int_string: string -> int -> string
 (** [string_suffix s n] returns the suffix of [s] that starts at the n'th
     character of [s] (zero-based).
 
-    @raise Invalid_argument if [n] is larger than the length of [s]
+    raise Invalid_argument if [n] is larger than the length of [s]
  *)
 val string_suffix: string -> int -> string
 
diff --git a/CodeHawk/CH/chutil/cHTraceResult.mli b/CodeHawk/CH/chutil/cHTraceResult.mli
index 49dd40a0..26d0b22d 100644
--- a/CodeHawk/CH/chutil/cHTraceResult.mli
+++ b/CodeHawk/CH/chutil/cHTraceResult.mli
@@ -34,12 +34,12 @@ type 'a traceresult = ('a, string list) result
 
 
 (** [tget_ok r] is [v] if [r] is [Ok v] and
-    @raise [Invalid_argument] otherwise.*)
+    raise [Invalid_argument] otherwise.*)
 val tget_ok: 'a traceresult -> 'a
 
 
 (** [tget_error r] is [e] if [r] is [Error e] and
-    @raise [Invalid_argument] otherwise.*)
+    raise [Invalid_argument] otherwise.*)
 val tget_error: 'a traceresult -> string list
 
 
diff --git a/CodeHawk/CHB/bchlib/bCHBCTypeUtil.mli b/CodeHawk/CHB/bchlib/bCHBCTypeUtil.mli
index 22ec5506..035ffb46 100644
--- a/CodeHawk/CHB/bchlib/bCHBCTypeUtil.mli
+++ b/CodeHawk/CHB/bchlib/bCHBCTypeUtil.mli
@@ -85,16 +85,16 @@ val t_charptr: btype_t
 val ptr_deref: btype_t -> btype_t
 
 
-(** {2 Array types)*)
+(** {2 Array types} *)
 
 val t_array: btype_t -> int -> btype_t
 
 
-(** {2 Type definition}*)
+(** {2 Type definition} *)
 
 val t_named: string -> btype_t
 
-(** {2 Composite types}*)
+(** {2 Composite types} *)
 
 val t_comp: ?name_space:string list -> string -> btype_t
 val t_enum: ?name_space:string list -> string -> btype_t
diff --git a/CodeHawk/CHB/bchlib/bCHBCTypes.mli b/CodeHawk/CHB/bchlib/bCHBCTypes.mli
index b143f4ca..f6361466 100644
--- a/CodeHawk/CHB/bchlib/bCHBCTypes.mli
+++ b/CodeHawk/CHB/bchlib/bCHBCTypes.mli
@@ -604,7 +604,7 @@ class type bcfiles_int =
 
     (** [get_varinfo name] returns the varinfo with name [name].
 
-        @raise BCH_failure if no varinfo exists with name [name].*)
+        raise BCH_failure if no varinfo exists with name [name].*)
     method get_varinfo: ?prefix:bool -> string -> bvarinfo_t
 
     (** Returns all global varinfos (including functions) *)
@@ -622,7 +622,7 @@ class type bcfiles_int =
     (** [get_typedef name] returns the (not necessarily fully expanded) type
         definition associated with [name].
 
-        @raise BCH_failure if no typedef exists with name [name].
+        raise BCH_failure if no typedef exists with name [name].
      *)
     method get_typedef: string -> btype_t
 
@@ -640,7 +640,7 @@ class type bcfiles_int =
     (** [get_compinfo key] returns the compinfo structure associated with
         (CIL-assigned) key [key].
 
-        @raise BCH_failure if no compinfo definition or declaration exists
+        raise BCH_failure if no compinfo definition or declaration exists
         with key [key].
      *)
     method get_compinfo: int -> bcompinfo_t
@@ -655,7 +655,7 @@ class type bcfiles_int =
 
     (** [get_enuminfo name] returns the enuminfo structure with name [name].
 
-        @raise BCH_failure if no enuminfo definition or declaration exists with
+        raise BCH_failure if no enuminfo definition or declaration exists with
         name [name]
      *)
     method get_enuminfo: string -> benuminfo_t
diff --git a/CodeHawk/CHB/bchlib/bCHBasicTypes.mli b/CodeHawk/CHB/bchlib/bCHBasicTypes.mli
index 4fc62a8e..1dade856 100644
--- a/CodeHawk/CHB/bchlib/bCHBasicTypes.mli
+++ b/CodeHawk/CHB/bchlib/bCHBasicTypes.mli
@@ -40,6 +40,7 @@ open BCHLibTypes
 
 
 exception BCH_failure of pretty_t
+(** basic exception in all of CHB *)
 
 (* raised in cases an internal inconsistency is encountered *)
 exception Internal_error of string
diff --git a/CodeHawk/CHB/bchlib/bCHByteUtilities.mli b/CodeHawk/CHB/bchlib/bCHByteUtilities.mli
index 4f50e57a..97b1130c 100644
--- a/CodeHawk/CHB/bchlib/bCHByteUtilities.mli
+++ b/CodeHawk/CHB/bchlib/bCHByteUtilities.mli
@@ -51,8 +51,8 @@ val rawdata_to_string:
 
 
 (** [write_xml_raw_data elt s dw] writes byte string [s] to the xml element
-    [elt] in the form of sub elements with tag {aline} and attributes
-    {bytes} and {print} that contain 4 space-separated groups of 4 bytes in
+    [elt] in the form of sub elements with tag [aline] and attributes
+    [bytes] and [print] that contain 4 space-separated groups of 4 bytes in
     hexadecimal and a print represenation of those 16 bytes, respectively.
 
     This format is used in saving binary content of the sections to xml.*)
diff --git a/CodeHawk/CHB/bchlib/bCHCPURegisters.mli b/CodeHawk/CHB/bchlib/bCHCPURegisters.mli
index 097e5a67..a2aa07a0 100644
--- a/CodeHawk/CHB/bchlib/bCHCPURegisters.mli
+++ b/CodeHawk/CHB/bchlib/bCHCPURegisters.mli
@@ -127,13 +127,13 @@ val full_registers: cpureg_t list
 (** [mk_arm_sp_reg i] returns an ARM single-precision floating point register
     (S<i>)
 
-    @raise BCH_failure if [i] is negative or i is greater than 31.*)
+    raise BCHBasicTypes.BCH_failure if [i] is negative or i is greater than 31.*)
 val mk_arm_sp_reg: int -> arm_extension_register_t
 
 (** [mk_arm_dp_reg i] returns an ARM double-precision floating point register
     (D<i>)
 
-    @raise BCH_failure if [i] is negative or i is greater than 15.*)
+    raise BCH_failure if [i] is negative or i is greater than 15.*)
 val mk_arm_dp_reg: int -> arm_extension_register_t
 
 
diff --git a/CodeHawk/CHB/bchlib/bCHConstantDefinitions.mli b/CodeHawk/CHB/bchlib/bCHConstantDefinitions.mli
index edd790eb..2181c430 100644
--- a/CodeHawk/CHB/bchlib/bCHConstantDefinitions.mli
+++ b/CodeHawk/CHB/bchlib/bCHConstantDefinitions.mli
@@ -76,7 +76,7 @@ val has_symbolic_address: string -> bool
 (** [get_symbolic_address name] returns the address associated with name
     [name].
 
-    @raise BCH_failure if no address exists with name [name].
+    raise BCH_failure if no address exists with name [name].
  *)
 val get_symbolic_address: string -> doubleword_int
 
@@ -96,20 +96,20 @@ val get_untyped_symbolic_address_names: unit -> string list
 val update_symbolic_address_btype: string -> btype_t -> unit
 
 (** [has_symbolic_address_name dw] returns true if the address [dw] is
-    associated with a name.]*)
+    associated with a name.*)
 val has_symbolic_address_name: doubleword_int -> bool
 
 (** [get_symbolic_address_name dw] returns the name associated with address
     [dw].
 
-    @raise BCH_failure if no name is associated with address [dw]
+    raise BCH_failure if no name is associated with address [dw]
  *)
 val get_symbolic_address_name: doubleword_int -> string
 
 (** [get_symbolic_address_type dw] returns the btype of the symbolic address
     associated with address value [dw].
 
-    @raise BCH_failure if no symbolic address is associated with address [dw].
+    raise BCH_failure if no symbolic address is associated with address [dw].
  *)
 val get_symbolic_address_type: doubleword_int -> btype_t
 
diff --git a/CodeHawk/CHB/bchlib/bCHDemangler.mli b/CodeHawk/CHB/bchlib/bCHDemangler.mli
index 36ecb621..f49071eb 100644
--- a/CodeHawk/CHB/bchlib/bCHDemangler.mli
+++ b/CodeHawk/CHB/bchlib/bCHDemangler.mli
@@ -36,7 +36,7 @@ open BCHLibTypes
 
 
 (**
-   {[
+{v
    ==============================================================================
    Grammar
    ==============================================================================
@@ -164,13 +164,13 @@ open BCHLibTypes
      U    struct
      V    class
      W    enum
-  ]}
+v}
 
   currently not supported yet:
     - fields
     - function pointers
 
- *)
+*)
 
 val demangle: string -> string
 val has_demangled_name: string -> bool
diff --git a/CodeHawk/CHB/bchlib/bCHFtsParameter.mli b/CodeHawk/CHB/bchlib/bCHFtsParameter.mli
index 63376017..2c4a215c 100644
--- a/CodeHawk/CHB/bchlib/bCHFtsParameter.mli
+++ b/CodeHawk/CHB/bchlib/bCHFtsParameter.mli
@@ -237,7 +237,7 @@ val pld_position_to_string: pld_position_t -> string
 
 (** Returns a string representation of a parameter location detail, which,
     depending on what information is available, may include:
-    - location slice: {size[<start>, <size>]}
+    - location slice: [size\[<start>, <size>\]]
     - type of the location, if known
     - position list, in case of field positions or array positions.*)
 val parameter_location_detail_to_string: parameter_location_detail_t -> string
diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInfo.mli b/CodeHawk/CHB/bchlib/bCHFunctionInfo.mli
index d194ded5..772a4ac9 100644
--- a/CodeHawk/CHB/bchlib/bCHFunctionInfo.mli
+++ b/CodeHawk/CHB/bchlib/bCHFunctionInfo.mli
@@ -60,7 +60,7 @@ val po_anchor_to_pretty: po_anchor_t -> pretty_t
       otherwise
     - a new function-info is created
 
-    @raise [BCH_failure] if
+    raise BCH_failure if
     - an error occurs when loading a function-info from file, or
     - address [dw] is not known to be a function entry point
  *)
diff --git a/CodeHawk/CHB/bchlib/bCHImmediate.mli b/CodeHawk/CHB/bchlib/bCHImmediate.mli
index 32461810..a139353d 100644
--- a/CodeHawk/CHB/bchlib/bCHImmediate.mli
+++ b/CodeHawk/CHB/bchlib/bCHImmediate.mli
@@ -44,7 +44,7 @@ val make_immediate: bool -> int -> numerical_t -> immediate_result
 
 (** [signed_immedidate_from_int size v] returns an immediate value of [size]
     bytes and value [v]. If the value [v] is outside the range that can be
-    represented by a signed integer with width [size] bytes, {Error] is
+    represented by a signed integer with width [size] bytes, [Error] is
     returned.*)
 val signed_immediate_from_int: ?size:int -> int -> immediate_result
 
diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli
index 8863bf68..83148d7a 100644
--- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli
+++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli
@@ -111,7 +111,7 @@ object ('a)
       doubleword with value the nearest value less than or equal to the value of
       [dw] that is a multiple of [n], and [d] the difference [dw - dw'].
 
-      @raises Invalid_argument if [n <= 0]. *)
+      raise Invalid_argument if [n <= 0]. *)
   method to_aligned: ?up:bool -> int -> ('a * int)
 
   (* conversion *)
@@ -131,7 +131,7 @@ object ('a)
 
   (** Returns a date-time string by converting [dw#value] to a Unix.tm structure.
 
-      @raise Invalid_argument if the intermediate Unix.tm structure is invalid.*)
+      raise Invalid_argument if the intermediate Unix.tm structure is invalid.*)
   method to_time_date_string: string
 
   (** Returns a string representing a list of four characters if all four
@@ -168,7 +168,7 @@ object ('a)
   (** Returns a standard hexadecimal notation of [dw#value] (without
       leading zeroes).
 
-      Example: [dw(0)#to_hex_string] returns "0x0"; dw(255)#to_hex_string]
+      Example: [dw(0)#to_hex_string] returns "0x0"; [dw(255)#to_hex_string]
       returns "0xff".*)
   method to_hex_string: string
 
@@ -190,7 +190,7 @@ object ('a)
       returns Error.*)
   method subtract: 'a  -> 'a traceresult
 
-  (** [dw#subtract i] returns dw(dw#value - i)] if [dw#value] is greater
+  (** [dw#subtract i] returns [dw(dw#value - i)] if [dw#value] is greater
       than or equal to [i], otherwise returns Error.*)
   method subtract_int: int -> 'a traceresult
 
@@ -1205,9 +1205,9 @@ class type struct_tables_int =
 
     and associated userdata (in json):
     {[
-	"call-back-tables": {
-	   "0x4a5c30": "cgi_setobject_table"
-	}
+    "call-back-tables": {
+       "0x4a5c30": "cgi_setobject_table"
+    }
     ]}
 
     The call-back table addresses provided by the user-data are read in by
@@ -1229,12 +1229,12 @@ class type struct_tables_int =
 
     For example:
     {[
-	"call-targets": [
-	   {"ia": "0x40d5dc",
-	    "fa": "0x40d510",
-	    "tgts": [{"cba": "0x4a5c30:8"}]
-	   }
-         ]
+    "call-targets": [
+      {"ia": "0x40d5dc",
+      "fa": "0x40d510",
+      "tgts": [{"cba": "0x4a5c30:8"}]
+      }
+    ]
     ]}
     identifies the location of the indirect call instruction by its
     instruction address (ia) in function (fa), and indicates that the
@@ -1264,17 +1264,17 @@ class type call_back_table_record_int =
 
     (** [cbtr#stringvalue n] returns the string value ([CBTag]) at offset [n].
 
-    @raise BCH_failure if the field at offset [n] is not a [CBTag] value.*)
+    raise BCH_failure if the field at offset [n] is not a [CBTag] value.*)
     method stringvalue: int -> string
 
     (** [cbtr#intvalue n] returns the numerical value ([CBValue]) at offset [n].
 
-    @raise BCH_failure if the field at offset [n] is not a [CBValue] value.*)
+    raise BCH_failure if the field at offset [n] is not a [CBValue] value .*)
     method intvalue: int -> numerical_t
 
     (** [cbtr#addrvalue n] returns the address value ([CBAddress]) at offset [n].
 
-    @raise BCH_failure if the field at offset [n] is not a [CBAddress] value.*)
+    raise BCH_failure if the field at offset [n] is not a [CBAddress] value.*)
     method addrvalue: int -> string   (* address at offset *)
 
     (** [cbtr#write_xml xnode] writes the field values and offset to [xnode].*)
@@ -1308,12 +1308,12 @@ class type call_back_table_int =
 
     (** [cbt#type_at_offset n] returns the type of the field at offset [n].
 
-    @raise BCH_failure if there is no field at offset [n].*)
+    raise BCH_failure if there is no field at offset [n].*)
     method type_at_offset: int -> btype_t
 
     (** [cbt#fieldname_at_offset n] returns the name of the field at offset [n].
 
-    @raise BCH_failure if there is no field at offset [n].*)
+    raise BCH_failure if there is no field at offset [n].*)
     method fieldname_at_offset: int -> string
 
     (** Returns a list of field-offset, field-type pairs containing all fields.*)
@@ -1357,7 +1357,7 @@ class type call_back_tables_int =
     (** [cbts#get_table addr] returns the call-back table with base address
         [addr].
 
-    @raise BCH_failure if no call-back table is present at [addr].*)
+    raise BCH_failure if no call-back table is present at [addr].*)
     method get_table: string -> call_back_table_int
 
     (** [cbts#has_table addr] returns true if there is a call-back table with
@@ -2201,14 +2201,20 @@ type function_stub_t =
 
 (** Identification of a call target in a call instruction.*)
 type call_target_t =
-  | StubTarget of function_stub_t (** call to dynamically linked function
-  external to the executable *)
-  | StaticStubTarget of doubleword_int * function_stub_t (** call to a statically
-  linked library function, with its address in the executable *)
-  | AppTarget of doubleword_int (** call to application function with the given address
-  in the executable *)
-  | InlinedAppTarget of doubleword_int * string (** [InlinedAppTarget (dw, name) is
-  call to an inlined application function with address [dw] and name [name] *)
+  | StubTarget of function_stub_t
+  (** call to dynamically linked function external to the executable *)
+
+  | StaticStubTarget of doubleword_int * function_stub_t
+  (** call to a statically linked library function, with its address in
+      the executable *)
+
+  | AppTarget of doubleword_int
+  (** call to application function with the given address in the executable *)
+
+  | InlinedAppTarget of doubleword_int * string
+  (** [InlinedAppTarget (dw, name)] is
+      call to an inlined application function with address [dw] and name [name] *)
+
   | WrappedTarget of
       doubleword_int
       * function_interface_t
@@ -2218,18 +2224,22 @@ type call_target_t =
         is a thin wrapper for a call to another function with address [a] and api
         [fapi], (inner) call target [tgt], with [map] a map of the parameters of
         the inner function mapped to the values given to the outer call.*)
-  | VirtualTarget of function_interface_t (** call to a virtual function with a
-  known type signature *)
+
+  | VirtualTarget of function_interface_t
+  (** call to a virtual function with a known type signature *)
+
   | IndirectTarget of bterm_t option * call_target_t list
-  (** [IndirectTarget (t, tgts) is a call to a target expressed by
+  (** [IndirectTarget (t, tgts)] is a call to a target expressed by
       term [t] (if known, must be expressible by values
       external to the function, e.g., a global variable or
       a function argument, or a return value) and a list of
       concreate call targets.*)
+
   | CallbackTableTarget of doubleword_int * int
   (** [CallbackTableTarget (dw, index)]
       is an indirect call where the
       target is in a table of pointers *)
+
   | UnknownTarget (** indirect call to an unknown target *)
 
 
@@ -2889,26 +2899,26 @@ class type function_summary_library_int =
         summaries before they are used in analysis.*)
     method read_summary_files: unit
 
-    (** {Query and access function summaries} *)
+    (** {1 Query and access function summaries} *)
 
     (** [get_function_dll fname] returns the name of the dll that contains
         a function by this name
 
-        @raise BCH_failure if [fname] is not an imported function
+        raise BCH_failure if [fname] is not an imported function
      *)
     method get_function_dll: string -> string
 
     (** [get_dll_function dll fname] returns the function summary for the dll
         function [fname] imported from dynamically loaded library [dll]
 
-        @raise BCH_failure if no summary is available for [fname] from [dll].
+        raise BCH_failure if no summary is available for [fname] from [dll].
      *)
     method get_dll_function: string -> string -> function_summary_int
 
     (** [get_so_function fname] returns the function summary for the shared
         object function [fname].
 
-        @raise BCH_failure if no summary is available for [fname].
+        raise BCH_failure if no summary is available for [fname].
      *)
     method get_so_function: string -> function_summary_int
 
@@ -2923,7 +2933,7 @@ class type function_summary_library_int =
     (** [get_syscall_function index] returns the function summary for the
         system call with index [index].
 
-        @raise BCH_failure if no summary is available for the system call with
+        raise BCH_failure if no summary is available for the system call with
         index [index].
      *)
     method get_syscall_function: int -> function_summary_int
@@ -2931,7 +2941,7 @@ class type function_summary_library_int =
     (** [get_jni_function index] returns the function summary for the Java
         Native Method with index [index].
 
-        @raise BCH_failure if no summary is available for the JNI function with
+        raise BCH_failure if no summary is available for the JNI function with
         index [index].
      *)
     method get_jni_function: int -> function_summary_int
@@ -3524,7 +3534,7 @@ and constant_value_variable_t =
       ctxt_iaddress_t       (* callsite *)
       * string              (* argument description *)
       * bool                (* is-global address *)
-  (** [SideEffectValue (iaddr, name, is_global) represents the value
+  (** [SideEffectValue (iaddr, name, is_global)] represents the value
   assigned by the callee at call site [iaddr] to the argument with
   name [name].*)
 
@@ -3839,7 +3849,7 @@ object
   method make_initial_register_value: register_t -> int -> assembly_variable_int
 
   (** [make_initial_memory_value var] returns the variable representing the
-      initial value of memory variable [var] at function entry.]*)
+      initial value of memory variable [var] at function entry.*)
   method make_initial_memory_value  : variable_t -> assembly_variable_int
 
   (** [make_return_value addr] returns the variable representing the return
@@ -3997,7 +4007,7 @@ object
       a constant numerical value or an index offset with fixed value variables. *)
   method has_fixed_value_offset: variable_t -> bool
 
-  (** Returns [true if [var] is a memory variable and its offset is a constant
+  (** Returns [true] if [var] is a memory variable and its offset is a constant
       numerical value. *)
   method has_constant_offset: variable_t -> bool
 
@@ -4468,7 +4478,7 @@ class type global_memory_map_int =
 (* =========================================================== Function info === *)
 
 
-(** @Deprecated Currenly used only for x86 *)
+(** @deprecated Currently used only for x86 *)
 class type argument_values_int =
 object
   method add_argument_values : variable_t -> xpr_t list -> unit
@@ -4653,7 +4663,7 @@ class type function_environment_int =
     (** [mk_offset_memory_variable memref memoff] returns a memory variable
         with [memref] as basis and a generic memory offset.
 
-        @raise [BCH_failure] if [memref] is an unknown memory reference.
+        raise BCH_failure if [memref] is an unknown memory reference.
 
         Note: eventually unknown memory references should be eliminated. *)
     method mk_offset_memory_variable:
@@ -4751,7 +4761,7 @@ class type function_environment_int =
 
     (** {2 Memory offsets} *)
 
-    (** Returns [true if [var] is a memory variable and its offset is a constant
+    (** Returns [true] if [var] is a memory variable and its offset is a constant
         numerical value. *)
     method has_constant_offset: variable_t -> bool
 
@@ -4877,7 +4887,7 @@ class type function_environment_int =
 
     (** {2 Other symbolic values} *)
 
-    (** {3 Function-call related) *)
+    (** {3 Function-call related} *)
 
     (** Returns [true] if [var] is the return value of a function call. *)
     method is_return_value: variable_t -> bool
@@ -5372,7 +5382,7 @@ object
       representation of the instruction at address [iaddr] with that address.*)
   method set_instruction_bytes: ctxt_iaddress_t -> string -> unit
 
-  (** finfo#get_instruction_bytes iaddr] returns the hexadecimal
+  (** [finfo#get_instruction_bytes iaddr] returns the hexadecimal
       representation of the instruction bytes for the instruction at address
       [iaddr].*)
   method get_instruction_bytes: ctxt_iaddress_t -> string
@@ -5392,7 +5402,7 @@ object
   (** [finfo#get_constant var] returns the constant value registered
       earlier for auxiliary variable [var].
 
-      @raise [Invocation_error] if no constant is associated with [var].
+      raise !Stdlib.Invocation_error if no constant is associated with [var].
    *)
   method get_constant: variable_t -> numerical_t
 
@@ -5536,7 +5546,7 @@ object
       instruction that sets the condition code used by the instruction at
       [iaddr].
 
-      @raise [BCH_failure] if the instruction at [iaddr] does not have an
+      raise BCH_failure if the instruction at [iaddr] does not have an
       associated setter.*)
   method get_associated_cc_setter: ctxt_iaddress_t -> ctxt_iaddress_t
 
@@ -5548,7 +5558,7 @@ object
   (** [finfo#get_associated_cc_user iaddr] returns the address of the instruction
       that uses the condition set by the instruction at [iaddr].
 
-      @raise [BCH_failure] if the instruction at [iaddr] does not have an
+      raise BCH_failure if the instruction at [iaddr] does not have an
       associated user.*)
   method get_associated_cc_user: ctxt_iaddress_t -> ctxt_iaddress_t
 
diff --git a/CodeHawk/CHB/bchlib/bCHLocation.mli b/CodeHawk/CHB/bchlib/bCHLocation.mli
index db395b61..9686df65 100644
--- a/CodeHawk/CHB/bchlib/bCHLocation.mli
+++ b/CodeHawk/CHB/bchlib/bCHLocation.mli
@@ -50,11 +50,12 @@ makes the call to the inlined function ([ctxt_callsite]), and the address
 of the instruction where the inlined function should return to (usually
 the instruction following the call) ([ctxt_returnsite]):
 
-[type fcontext_t = {
+{[type fcontext_t = {
     ctxt_faddr: doubleword_int;
     ctxt_callsite: doubleword_int;
     ctxt_returnsite: doubleword_int
-  }]
+  }
+]}
 
 A base location can also be wrapped into a block context to facilitate
 creating a delayed join by duplicating blocks. In this case the context
@@ -67,7 +68,7 @@ holds the address of the block that is duplicated.
 A [ctxt_iaddress_t] is a string representation of an instruction address with
 context, with spec
 
-[   i  ( [], { faddr,iaddr } ) = iaddr
+{v   i  ( [], { faddr,iaddr } ) = iaddr
    i  ( [ F{ fa,cs,rs } ], { faddr,iaddr }) = iaddr
    i  ( [ B{ js } ], { faddr,iaddr }) = iaddr
 
@@ -81,7 +82,7 @@ context, with spec
    ci ( [ F{ fa1,cs1,rs1 },F{ fa2,cs2,rs2 } ], { faddr,iaddr } ) = F:cs1_F:cs2_iaddr
    ci ( [ B{ js } ], { faddr,iaddr }) = B:js_iaddr
    ci ( [ B{ js1 }, B{ js2 } ], { faddr,iaddr }) = B:js1_B:js2_iaddr
-]
+v}
 
 where [fa], [faddr] stand for function address, [cs] stands for call-site address,
 [rs] stands for return-site address, [js] stands for jump-site address (the
@@ -99,7 +100,7 @@ val mk_function_context:
   -> context_t
 
 
-(** [mk_base_location [faddr] [iaddr] creates a base_location from function
+(** [mk_base_location faddr iaddr] creates a base_location from function
     address [faddr] and instruction address [iaddr] *)
 val mk_base_location: doubleword_int -> doubleword_int -> base_location_t
 
diff --git a/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.mli b/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.mli
index f68f062f..50e4dbf1 100644
--- a/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.mli
+++ b/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.mli
@@ -85,7 +85,7 @@ val join_integer_btypes: btype_t list -> btype_t option
 val mk_function_typevar: string -> type_variable_t
 
 
-(** mk_data_address_typevar gaddr] returns a type variable for the global
+(** [mk_data_address_typevar gaddr] returns a type variable for the global
     address [gaddr] (in hex).
 
     Note that this address may be either the address of a global variable,
diff --git a/CodeHawk/CHB/bchlib/bCHUtilities.mli b/CodeHawk/CHB/bchlib/bCHUtilities.mli
index abcd7322..b91bbc71 100644
--- a/CodeHawk/CHB/bchlib/bCHUtilities.mli
+++ b/CodeHawk/CHB/bchlib/bCHUtilities.mli
@@ -49,14 +49,14 @@ val track_function:
 
 (** Return the current time represented as [day year-month-mday at hr:min].
 
-    @raise Invalid_argument if the time cannot be obtained or is invalid.
+    raise Invalid_argument if the time cannot be obtained or is invalid.
 *)
 val get_date_and_time: unit -> string
 
 
 (** Convert a Unix [tm] type into a string [weekday month mday hr:min:sec year].
 
-    @raise Invalid_argument if the [tm] structure is invalid.*)
+    raise Invalid_argument if the [tm] structure is invalid.*)
 val make_date_and_time_string: Unix.tm -> string (* raises Invalid_argument *)
 
 
diff --git a/CodeHawk/CHB/bchlibmips32/bCHMIPSDisassemblyUtils.mli b/CodeHawk/CHB/bchlibmips32/bCHMIPSDisassemblyUtils.mli
index 1e745b22..686dbfc7 100644
--- a/CodeHawk/CHB/bchlibmips32/bCHMIPSDisassemblyUtils.mli
+++ b/CodeHawk/CHB/bchlibmips32/bCHMIPSDisassemblyUtils.mli
@@ -39,7 +39,7 @@ open BCHMIPSTypes
 (** [select_mips_reg i] returns the MIPS register with sequence number [i]
     (e.g., [$a0] for [4], [$s0] for [16], etc.)
 
-    @raise [BCH_failure] if [i] is outside the range [0 - 31]
+    raise BCH_failure if [i] is outside the range [0 - 31]
 *)
 val select_mips_reg: int -> mips_reg_t
 
diff --git a/CodeHawk/CHB/bchlibpower32/bCHPowerTypes.mli b/CodeHawk/CHB/bchlibpower32/bCHPowerTypes.mli
index 39dd2ab9..133ed021 100644
--- a/CodeHawk/CHB/bchlibpower32/bCHPowerTypes.mli
+++ b/CodeHawk/CHB/bchlibpower32/bCHPowerTypes.mli
@@ -212,7 +212,7 @@ type pwr_instruction_type_t = | PWR | VLE16 | VLE32
 
 (** {1 Operands}
 
-defined in {! bchlib/bCHLibTypes}:
+defined in bchlib/BCHLibTypes:
 
 {[
 type pwr_special_reg_t =
diff --git a/CodeHawk/CHB/bchlibx86/bCHAssemblyInstructions.mli b/CodeHawk/CHB/bchlibx86/bCHAssemblyInstructions.mli
index e7c02088..501c3fdd 100644
--- a/CodeHawk/CHB/bchlibx86/bCHAssemblyInstructions.mli
+++ b/CodeHawk/CHB/bchlibx86/bCHAssemblyInstructions.mli
@@ -48,7 +48,7 @@ val assembly_instructions: assembly_instructions_int ref
 
 (** Create an array of the given size to hold the assembly instructions.
 
-    @raises [BCH_failure] if not sufficient array space is available to
+    raises BCH_failure if not sufficient array space is available to
     store all instructions.*)
 val initialize_instructions: int -> unit
 
diff --git a/CodeHawk/CHB/bchlibx86/bCHConditionalJumpExpr.mli b/CodeHawk/CHB/bchlibx86/bCHConditionalJumpExpr.mli
index a8494023..ced28620 100644
--- a/CodeHawk/CHB/bchlibx86/bCHConditionalJumpExpr.mli
+++ b/CodeHawk/CHB/bchlibx86/bCHConditionalJumpExpr.mli
@@ -50,10 +50,10 @@ open BCHLibx86Types
     instruction and branch instruction, None is returned for the predicate,
     and a message is logged about the missing predicate.
 
-    If the predicate constructed simplifies to {false], None is returned
+    If the predicate constructed simplifies to [false], None is returned
     and a message is logged that the condition is ignored.
 
-    @raises [BCH_failure] if [jumpopc] is not a jump instruction (i.e.,
+    raises BCH_failure if [jumpopc] is not a jump instruction (i.e.,
     [Jexz], [DirectLoop], or [Jcc]).
  *)
 val conditional_jump_expr:
@@ -70,7 +70,7 @@ val conditional_jump_expr:
     [setopc] at location [setloc]. If no condition can be established
     [random_constant_expr] is returned.
 
-    @raises [BCH_failure] if [setopc] is not a set instruction (i.e.,
+    raises BCH_failure if [setopc] is not a set instruction (i.e.,
     [Setcc]).
  *)
 val conditional_set_expr:
diff --git a/CodeHawk/CHB/bchlibx86/bCHDisassembleInstruction.mli b/CodeHawk/CHB/bchlibx86/bCHDisassembleInstruction.mli
index cbd42868..3d7c429f 100644
--- a/CodeHawk/CHB/bchlibx86/bCHDisassembleInstruction.mli
+++ b/CodeHawk/CHB/bchlibx86/bCHDisassembleInstruction.mli
@@ -39,7 +39,7 @@ open BCHLibx86Types
     inputstream [ch]. The [base] argument is provided to enable the compuatation
     of an absolute target address for a relative jump or call, that is,
 
-    {absolute_address = base + position}
+    [absolute_address = base + position]
 
     so [base] should be the base of the code section being disassembled, not
     necessarily the code base, if there are multiple code sections.
diff --git a/CodeHawk/CHB/bchlibx86/bCHDisassemblyUtils.mli b/CodeHawk/CHB/bchlibx86/bCHDisassemblyUtils.mli
index 4cc7bac7..a2d79499 100644
--- a/CodeHawk/CHB/bchlibx86/bCHDisassemblyUtils.mli
+++ b/CodeHawk/CHB/bchlibx86/bCHDisassemblyUtils.mli
@@ -76,7 +76,7 @@ val get_jump_operand: opcode_t -> operand_int
        | 7     | Di              | Edi             |
     }
 
-    @raises [InconsistentInstruction] if [index] is outside the range
+    raises InconsistentInstruction if [index] is outside the range
     0 - 7.
  *)
 val select_word_or_dword_reg: bool -> int -> cpureg_t
diff --git a/CodeHawk/CHB/bchlibx86/bCHLibx86Types.mli b/CodeHawk/CHB/bchlibx86/bCHLibx86Types.mli
index 5bd92535..dc9f0f43 100644
--- a/CodeHawk/CHB/bchlibx86/bCHLibx86Types.mli
+++ b/CodeHawk/CHB/bchlibx86/bCHLibx86Types.mli
@@ -96,9 +96,9 @@ object ('a)
   (** Returns true if a function argument has been recorded for this operand.*)
   method is_function_argument: bool
 
-  (** [Retrieves the address and argument index (starting at 1).
+  (** Retrieves the address and argument index (starting at 1).
 
-      @raises BCH_failure if no function argument has been set.*)
+      raises BCH_failure if no function argument has been set.*)
   method get_function_argument: ctxt_iaddress_t * int
 
   (** removes the function argument, if one is set.*)
@@ -118,29 +118,29 @@ object ('a)
 
   (** Returns the register.
 
-      @raises BCH_failure if this operand is not a register operand.*)
+      raises BCH_failure if this operand is not a register operand.*)
   method get_cpureg: cpureg_t
 
   (** Returns the absolute address associated with this operand.
 
-      @raises Invocation_error if this operand is not an absolute address
+      raises Invocation_error if this operand is not an absolute address
       operand.*)
   method get_absolute_address: doubleword_int
 
   (** Returns the immediate value associated with this operand.
 
-      @raises Invocation_error if this operand is not an immediate value.*)
+      raises Invocation_error if this operand is not an immediate value.*)
   method get_immediate_value: immediate_int
 
   (** Returns the offset part of an indirect register operand.
 
-      @raises Invocation_error if this operand is not an indirect register.*)
+      raises Invocation_error if this operand is not an indirect register.*)
   method get_esp_offset: numerical_t
 
   (** Returns the register and offset that may be used as the operand in a
       jumptable (scaled index register with scale 4).
 
-      @raises Invocation_error if this operand is not a scaled indirect
+      raises Invocation_error if this operand is not a scaled indirect
       register with scale factor 4.*)
   method get_jump_table_target: (numerical_t * register_t)
 
@@ -150,17 +150,17 @@ object ('a)
 
   (** Returns the base register of an indirect register operand.
 
-      @raises BCH_failure if this operand is not an indirect register.*)
+      raises BCH_failure if this operand is not an indirect register.*)
   method get_indirect_register: cpureg_t
 
   (** Returns the offset of indirect register operand.
 
-      @raises BCH_failure if this operand is not an indirect register.*)
+      raises BCH_failure if this operand is not an indirect register.*)
   method get_indirect_register_offset: numerical_t
 
   (** Returns the segment of a segment register operand.
 
-      @raises Invocation_error if this operand is not a segment register.*)
+      raises Invocation_error if this operand is not a segment register.*)
   method get_segment_register: segment_t
 
   (** {1 Converters}
@@ -172,7 +172,7 @@ object ('a)
       or a random constant if the address cannot be determined from the
       invariants available.
 
-      @raises Invocation_error if the operand is an immediate or register,
+      raises Invocation_error if the operand is an immediate or register,
       which do not have an address.*)
   method to_address: floc_int -> xpr_t
 
@@ -186,7 +186,7 @@ object ('a)
       determine the associated memory variable, an unknown memory variable
       is returned.
 
-      @raises Invocation_error if the operand is an immediate value, which
+      raises Invocation_error if the operand is an immediate value, which
       does not have an associated storage location (variable).*)
   method to_variable: floc_int -> variable_t
 
@@ -197,7 +197,7 @@ object ('a)
   (** Returns the lhs-variable (CHIF variable) associated with this operand
       together with the CHIF commands required to create this operand.
 
-      @raises Invocation_error if the operand is an immediate value, which
+      raises Invocation_error if the operand is an immediate value, which
       cannot be converted to a lhs.*)
   method to_lhs: ?_size:int -> floc_int -> variable_t * cmd_t list
 
diff --git a/CodeHawk/CHC/cchanalyze/cCHAnalysisTypes.mli b/CodeHawk/CHC/cchanalyze/cCHAnalysisTypes.mli
index ac944b85..afb4b2de 100644
--- a/CodeHawk/CHC/cchanalyze/cCHAnalysisTypes.mli
+++ b/CodeHawk/CHC/cchanalyze/cCHAnalysisTypes.mli
@@ -543,7 +543,7 @@ class type po_query_int =
     (** [get_command_line_argument_index exp] returns the (0-based) function
         argument index if exp is a function argument.
 
-        @raise [CCHFailure] if [exp] is not a command-line argument.*)
+        raise [CCHFailure] if [exp] is not a command-line argument.*)
     method get_command_line_argument_index: exp -> int
 
 
@@ -681,7 +681,7 @@ class type po_query_int =
         otherwise the postconditions assumptions are retrieved from the proof
         callcontext in the proof scaffolding.
 
-        @raise [CCHFailure] if [var] is not a function return value variable.*)
+        raise [CCHFailure] if [var] is not a function return value variable.*)
     method get_postconditions:
              variable_t
              -> annotated_xpredicate_t list * annotated_xpredicate_t list
@@ -699,23 +699,23 @@ class type po_query_int =
         otherwise the postassumes are retrieved from the proof callcontext in
         the proof scaffolding.
 
-        @raise [CCHFailure] if [var] is not a function return value variable.*)
+        raise [CCHFailure] if [var] is not a function return value variable.*)
     method get_sideeffects: variable_t -> annotated_xpredicate_t list
 
-    (** [same as [get_sideeffects var] with the symbol component of [var].*)
+    (** same as [get_sideeffects var] with the symbol component of [var].*)
     method get_sym_sideeffects: symbol_t -> annotated_xpredicate_t list
 
     (** [get_function_return_callee xpr] returns the varinfo representing the
         callee associated with return value variable expression [xpr].
 
-        @raise [CCHFailure] if [xpr] is not a return value variable expression.*)
+        raise [CCHFailure] if [xpr] is not a return value variable expression.*)
     method get_function_return_callee: xpr_t -> varinfo
 
     (** [get_tainted_value_origin var] returns a tuple of an explanation, the
         vinfo for the callee that conferred the taint on [var] and the
         postcondition or sideeffect through which the taint was transmitted.
 
-        @raise [CCHFailure] if [var] is not a tainted value.*)
+        raise [CCHFailure] if [var] is not a tainted value.*)
     method get_tainted_value_origin:
              variable_t -> (string * varinfo * xpredicate_t)
 
@@ -750,7 +750,7 @@ class type po_query_int =
         returned.*)
     method e2x: exp -> xpr_t
 
-    (** [get_external_value exp] attempts to convert [exp to an [xpr_t] using
+    (** [get_external_value exp] attempts to convert [exp] to an [xpr_t] using
         the [num_exp_translator] with location invariants provided to aid in the
         conversion. If [exp] cannot be converted against the invariants, a random
         constant is returned.*)
@@ -765,7 +765,7 @@ class type po_query_int =
     (** [get_api_expression xpr] returns a c expression that can represent xpr
         in an api assumption.
 
-        @raise [CCHFailure] if [xpr] cannot be thus converted.*)
+        raise [CCHFailure] if [xpr] cannot be thus converted.*)
     method get_api_expression: xpr_t -> exp
 
     (** [x2global xpr] attempts to convert expression [xpr] into a global c
@@ -777,14 +777,14 @@ class type po_query_int =
         if [xpr] is a constant value or the initial value of a global variable (or
         some combination of the two).
 
-        @raise [CCHFailure if [xpr] is not a constant value or initial value of a
+        raise [CCHFailure] if [xpr] is not a constant value or initial value of a
         global variable.*)
     method get_global_expression: xpr_t -> exp
 
     (** [remove_null_syms syms] returns the sublist of memory region symbols
         [syms] that are not NULL.
 
-        @raise [CCHFailure] if one or more of the symbols in [syms] are not memory
+        raise [CCHFailure] if one or more of the symbols in [syms] are not memory
         region symbols.*)
     method remove_null_syms: symbol_t list -> symbol_t list
 
diff --git a/CodeHawk/CHC/cchlib/cCHCAttributes.mli b/CodeHawk/CHC/cchlib/cCHCAttributes.mli
index 2bf4207c..20ddb3df 100644
--- a/CodeHawk/CHC/cchlib/cCHCAttributes.mli
+++ b/CodeHawk/CHC/cchlib/cCHCAttributes.mli
@@ -367,7 +367,7 @@ val convert_attribute_to_function_conditions:
     The [chkc_static] attribute specifies that the visibility of the global
     variable is limited to the current compilation unit.
 
-    {3 chkc_not_null__]}
+    {[chkc_not_null__]}
 
     The [chkc_not_null] attribute specifies that the value of the global 
     variable is not null.
diff --git a/CodeHawk/CHC/cchlib/cCHLibTypes.mli b/CodeHawk/CHC/cchlib/cCHLibTypes.mli
index 4ffae738..529beca1 100644
--- a/CodeHawk/CHC/cchlib/cCHLibTypes.mli
+++ b/CodeHawk/CHC/cchlib/cCHLibTypes.mli
@@ -6,7 +6,7 @@
 
    Copyright (c) 2005-2019 Kestrel Technology LLC
    Copyright (c) 2020-2022 Henny B. Sipma
-   Copyright (c) 2023-2024 Aarno Labs LLC
+   Copyright (c) 2023-2025 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
@@ -867,7 +867,7 @@ class type system_settings_int =
     method is_implementation_defined: bool
     method is_value_wrap_around: bool
 
-    (** {1 Other settings*)
+    (** {1 Other settings} *)
 
     method set_verbose: bool -> unit
     method verbose: bool
diff --git a/CodeHawk/CHC/cchpre/cCHPreTypes.mli b/CodeHawk/CHC/cchpre/cCHPreTypes.mli
index 3f9cd9eb..c7c25825 100644
--- a/CodeHawk/CHC/cchpre/cCHPreTypes.mli
+++ b/CodeHawk/CHC/cchpre/cCHPreTypes.mli
@@ -424,7 +424,7 @@ object
 
   method mk_symbolic_value: xpr_t -> typ -> c_variable_int
 
-  (** mk_memory_address memindex offset] returns a memory address from memory
+  (** mk_memory_address memindex [offset] returns a memory address from memory
       reference index [memindex] and an offset*)
   method mk_memory_address: int -> offset -> c_variable_int
 
@@ -484,21 +484,21 @@ object
       the initial-value variable with index [varindex] of either a local
       variable or a memory variable with an external base variable.
 
-      @raise CCHFailure if [varindex] does not belong to such a variable.
+      raise CCHFailure if [varindex] does not belong to such a variable.
    *)
   method get_parameter_exp: int -> exp
 
   (** [get_global_exp varindex] returns the expression associated with the
       initial-value variable with index [varindex] of a global variable.
 
-      @raise CCHFailure if [varindex] does not belong to such a variable.
+      raise CCHFailure if [varindex] does not belong to such a variable.
    *)
   method get_global_exp: int -> exp
 
   (** [get_callee varindex] returns the varinfo of the function belonging
       to the return variable or side-effect variable with index [varindex].
 
-      @raise CCHFailure if [varindex] does not belong to a function-return
+      raise CCHFailure if [varindex] does not belong to a function-return
       of function-side-effect variable.
    *)
   method get_callee: int -> varinfo
@@ -514,7 +514,7 @@ object
   (** [get_tainted_value_bounds varindex] returns the optional lower and upper
       bounds of a tainted variable with index index [varindex].
 
-      @raise CCHFailure if [varindex] does not belong to a tainted variable.
+      raise CCHFailure if [varindex] does not belong to a tainted variable.
    *)
   method get_tainted_value_bounds: int -> xpr_t option * xpr_t option
 
@@ -534,7 +534,7 @@ object
   (** [get_purpose varindex] returns the purpose associated with the
       augmentation variable with index [varindex]
 
-      @raise CCHFailure if [varindex] does not belong to an augmentation
+      raise CCHFailure if [varindex] does not belong to an augmentation
       variable.
    *)
   method get_purpose: int -> string
@@ -542,7 +542,7 @@ object
   (** [get_indicator varindex] returns the indicator associated with the
       augmentation variable with index [varindex]
 
-      @raise CCHFailure if [varindex] does not belong to an augmentation
+      raise CCHFailure if [varindex] does not belong to an augmentation
       variable.
    *)
   method get_indicator: int -> int
@@ -551,7 +551,7 @@ object
       represents the same function-return value or side-effect variable as the
       variable with [varindex], but without arguments.
 
-      @raise CCHFailure if [varindex] does not belong to a function-return or
+      raise CCHFailure if [varindex] does not belong to a function-return or
       side-effect value variable.
    *)
   method get_canonical_fnvar_index: int -> int
@@ -717,7 +717,7 @@ type po_predicate_t =
       equal to zero. *)
 
   | PUpperBound of typ * exp
-  (** {Pointer expression [exp] has a value that is less than or equal to the
+  (** Pointer expression [exp] has a value that is less than or equal to the
       highest address that can be dereferenced for type [typ].*)
 
   | PIndexLowerBound of exp

From 460c5b03d07637b950fbebd13de5569af5fbc073 Mon Sep 17 00:00:00 2001
From: Henny Sipma <hennysipma@mac.com>
Date: Wed, 2 Jul 2025 12:59:10 -0700
Subject: [PATCH 10/16] CHB: allow for address roll-over in simplification of
 preconditions

---
 .../CHB/bchlib/bCHCallSemanticsRecorder.ml    | 19 ++++++++++---------
 1 file changed, 10 insertions(+), 9 deletions(-)

diff --git a/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml b/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml
index 58795e47..fb674b29 100644
--- a/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml
+++ b/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml
@@ -99,6 +99,7 @@ object (self)
     | XPONotNull x ->
        (match x with
         | XConst (IntConst n) when n#gt numerical_zero ->
+           let n = n#modulo numerical_e32 in
            Discharged
              ("non-null constant address: "
               ^ TR.tget_ok (numerical_to_hex_string n))
@@ -109,7 +110,7 @@ object (self)
     | XPONullTerminated x ->
        (match x with
         | XConst (IntConst n) ->
-           let dw = TR.tget_ok (numerical_to_doubleword n) in
+           let dw = numerical_mod_to_doubleword n in
            if string_table#has_string dw then
              Discharged ("constant string: " ^ (string_table#get_string dw))
            else
@@ -119,7 +120,7 @@ object (self)
        (match (ptr, size) with
         | (XConst (IntConst n1), XOp ((Xf "ntpos"), [XConst (IntConst n2)]))
              when n1#equal n2 ->
-           let dw = TR.tget_ok (numerical_to_doubleword n1) in
+           let dw = numerical_mod_to_doubleword n1 in
            if string_table#has_string dw then
              Discharged ("constant string: " ^ (string_table#get_string dw))
            else
@@ -129,7 +130,7 @@ object (self)
        (match (ptr, size) with
         | (XConst (IntConst n1), XOp ((Xf "ntpos"), [XConst (IntConst n2)]))
              when n1#equal n2 ->
-           let dw = TR.tget_ok (numerical_to_doubleword n1) in
+           let dw = numerical_mod_to_doubleword n1 in
            if string_table#has_string dw then
              Discharged ("constant string: " ^ (string_table#get_string dw))
            else
@@ -138,7 +139,7 @@ object (self)
     | XPOOutputFormatString x ->
        (match x with
         | XConst (IntConst n) ->
-           let dw = TR.tget_ok (numerical_to_doubleword n) in
+           let dw = numerical_mod_to_doubleword n in
            if string_table#has_string dw then
              Discharged ("constant string: " ^ (string_table#get_string dw))
            else
@@ -170,7 +171,7 @@ object (self)
        let x = simplify_xpr x in
        (match self#xprxt#xpr_to_bterm t_voidptr x with
         | Some (NumConstant n) when n#gt numerical_zero ->
-           let dw = TR.tget_ok (numerical_to_doubleword n) in
+           let dw = numerical_mod_to_doubleword n in
            DelegatedGlobal (dw, XXNotNull (NumConstant n))
         | Some t -> Delegated (XXNotNull t)
         | _ -> Open)
@@ -178,14 +179,14 @@ object (self)
        let x = simplify_xpr x in
        (match self#xprxt#xpr_to_bterm t_voidptr x with
         | Some (NumConstant n) when n#gt numerical_zero ->
-           let dw = TR.tget_ok (numerical_to_doubleword n) in
+           let dw = numerical_mod_to_doubleword n in
            DelegatedGlobal (dw, XXNullTerminated (NumConstant n))
         | Some t -> Delegated (XXNullTerminated t)
         | _ -> Open)
     | XPOBlockWrite (ty, ptr, size) ->
        (match self#xprxt#xpr_to_bterm t_voidptr ptr with
         | Some (NumConstant n) when n#gt numerical_zero ->
-           let dw = TR.tget_ok (numerical_to_doubleword n) in
+           let dw = numerical_mod_to_doubleword n in
            (match self#xprxt#xpr_to_bterm t_int size with
             | Some (NumConstant ns) ->
                DelegatedGlobal
@@ -200,7 +201,7 @@ object (self)
     | XPOBuffer (ty, ptr, size) ->
        (match self#xprxt#xpr_to_bterm t_voidptr ptr with
         | Some (NumConstant n) when n#gt numerical_zero ->
-           let dw = TR.tget_ok (numerical_to_doubleword n) in
+           let dw = numerical_mod_to_doubleword n in
            (match self#xprxt#xpr_to_bterm t_int size with
             | Some (NumConstant ns) ->
                DelegatedGlobal
@@ -215,7 +216,7 @@ object (self)
     | XPOInitializedRange (ty, ptr, size) ->
        (match self#xprxt#xpr_to_bterm t_voidptr ptr with
         | Some (NumConstant n) when n#gt numerical_zero ->
-           let dw = TR.tget_ok (numerical_to_doubleword n) in
+           let dw = numerical_mod_to_doubleword n in
            (match self#xprxt#xpr_to_bterm t_int size with
             | Some (NumConstant ns) ->
                DelegatedGlobal

From fa3c09f219498b5725d77fafa44e68e6e0b0d398 Mon Sep 17 00:00:00 2001
From: Henny Sipma <hennysipma@mac.com>
Date: Wed, 2 Jul 2025 13:01:32 -0700
Subject: [PATCH 11/16] CHB: don't replace variables associated with tests

---
 CodeHawk/CHB/bchlib/bCHFunctionInfo.ml | 16 +++++++++++++++-
 CodeHawk/CHB/bchlib/bCHVersion.ml      |  4 ++--
 2 files changed, 17 insertions(+), 3 deletions(-)

diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml
index 90848ebb..eb6ad7c7 100644
--- a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml
+++ b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml
@@ -2021,7 +2021,21 @@ object (self)
   method set_test_variables
            (test_iaddr: ctxt_iaddress_t)
            (vars: (variable_t * variable_t) list) =
-    H.replace test_variables test_iaddr vars
+    (* Multiple jump (or other use) sites may be using the same test, so we
+       cannot just replace the set of test_variables, when a new set comes in.
+     *)
+    let entry =
+      if H.mem test_variables test_iaddr then
+        H.find test_variables test_iaddr
+      else
+        [] in
+    let newentry =
+      List.fold_left (fun acc (v1, v2) ->
+          if (List.exists (fun (v1', v2') -> v1#equal v1' && v2#equal v2') acc) then
+            acc
+          else
+            (v1, v2) :: acc) entry vars in
+    H.replace test_variables test_iaddr newentry
 
   method get_test_variables (test_iaddr:ctxt_iaddress_t) =
     if H.mem test_variables test_iaddr then
diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml
index 9552c8de..427a45c8 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_20250625"
-  ~date:"2025-06-25"
+  ~version:"0.6.0_20250702"
+  ~date:"2025-07-02"
   ~licensee: None
   ~maxfilesize: None
   ()

From 8e6ad58584ee027dcbe1bda5563d84c521e8b00a Mon Sep 17 00:00:00 2001
From: Henny Sipma <hennysipma@mac.com>
Date: Wed, 2 Jul 2025 13:06:31 -0700
Subject: [PATCH 12/16] CHB:ARM: add documentation for conditional expressions

---
 .../CHB/bchlibarm32/bCHARMConditionalExpr.ml  |  9 +++-
 .../CHB/bchlibarm32/bCHARMConditionalExpr.mli | 45 ++++++++++++++++++-
 2 files changed, 51 insertions(+), 3 deletions(-)

diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMConditionalExpr.ml b/CodeHawk/CHB/bchlibarm32/bCHARMConditionalExpr.ml
index 8f2ba18b..e34627eb 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHARMConditionalExpr.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHARMConditionalExpr.ml
@@ -433,7 +433,11 @@ let arm_conditional_expr
        else
 	 begin
            (if collect_diagnostics () then
-              ch_diagnostics_log#add "condition" (x2p expr));
+              ch_diagnostics_log#add
+                "condition"
+                (LBLOCK [condloc#toPretty; STR ": "; (x2p expr); STR ". ";
+                         pretty_print_list frozenVars#listOfValues
+                           (fun v -> v#toPretty) "[" ", " "]" ]));
 	   condfloc#set_test_expr expr;
 	   testfloc#set_test_variables frozenVars#listOfPairs;
 	   (frozenVars#listOfValues, (Some expr), opsused)
@@ -504,7 +508,8 @@ let arm_conditional_conditional_expr
                 STR "; cond3: ";
                 x2p cond3]) in
 
-     let xpr = XOp (XLOr, [XOp (XLAnd, [XOp (XLNot, [cond1]); cond3]); cond2]) in
+     let xpr = XOp (XLOr, [XOp (XLAnd, [XOp (XLNot, [cond1]); cond3]);
+                           XOp (XLAnd, [cond1; cond2])]) in
      begin
        (if collect_diagnostics () then
           ch_diagnostics_log#add "condition" (x2p xpr));
diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMConditionalExpr.mli b/CodeHawk/CHB/bchlibarm32/bCHARMConditionalExpr.mli
index 965b679f..96f0fa8b 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHARMConditionalExpr.mli
+++ b/CodeHawk/CHB/bchlibarm32/bCHARMConditionalExpr.mli
@@ -4,7 +4,7 @@
    ------------------------------------------------------------------------------
    The MIT License (MIT)
 
-   Copyright (c) 2021-2024 Aarno Labs LLC
+   Copyright (c) 2021-2025 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
@@ -37,6 +37,21 @@ open BCHLibTypes
 (* bchlibarm32 *)
 open BCHARMTypes
 
+
+(** Returns the predicate condition and associated info for a condidional,
+    in particular it returns a tuple consisting of:
+    - a list of temporary variables created to preserve the (frozen) values at
+      the test location (testloc) for the location of the conditional (condloc)
+    - the predicate that expresses the joint condition of test and condition
+      code (cc, e.g., EQ), and
+    - a list of the operands used in the creation of the predicate.
+
+    The arguments to the function are:
+    - [condopc]: the opcode of the conditional instruction (e.g., Branch)
+    - [testopc]: the opcode of the test instruction (e.g., Compare)
+    - [condloc]: the location of conditional instruction
+    - [testloc]: the location of the test instruction.
+ *)
 val arm_conditional_expr:
   condopc: arm_opcode_t
   -> testopc:arm_opcode_t
@@ -45,6 +60,34 @@ val arm_conditional_expr:
   -> (variable_t list * xpr_t option * arm_operand_int list)
 
 
+(** Returns the predicate condition and associated info as above for a composite
+    condtitional of the form
+{v
+    I1: <test1>            CMP    x, #0
+    I2: <test2-cc1>        CMPEQ  y, z
+    I3: <cond-cc2>         BGT
+v}
+    where the ultimate predicate condition depends is a composite of potentially
+    three test - cc combinations:
+    - if test1-cc1 is true, I2 is executed and the branch predicate is test2-cc2
+    - if test2-cc1 is false I2 is not executed and branch predicate is test2-cc1
+    leading to the composite expression
+{v
+     (test1-cc1 /\ test2-cc2) \/ ((not test1-cc1) /\ test1-cc2)
+v}
+    or, in the case of the example above:
+{v
+     (x = 0 /\ y > z) \/ (x != 0 /\ x > 0)
+or
+     (x = 0 /\ y > z) \/ (x > 0)
+v}
+    - [condopc]: the opcode of the conditional instruction (above: BGT)
+    - [testopc] the opcode of the second test instruction (above: CMPEQ)
+    - [testtestopc]: the opcode of the first test instruction (above: CMP)
+    - [condloc]: the location of [condopc]
+    - [testloc]: the location of [testopc]
+    - [testtestloc]: the location of [testtestopc]
+ *)
 val arm_conditional_conditional_expr:
   condopc: arm_opcode_t
   -> testopc: arm_opcode_t

From d0cc1cd2af68301d50c267da68b5bc8c75286bed Mon Sep 17 00:00:00 2001
From: Henny Sipma <hennysipma@mac.com>
Date: Wed, 2 Jul 2025 13:56:02 -0700
Subject: [PATCH 13/16] CHB:ARM: add jumptable pattern found in clang-18.1.3
 compiled binary

---
 CodeHawk/CHB/bchlibarm32/bCHARMJumptable.ml  | 168 +++++++++++++++++++
 CodeHawk/CHB/bchlibarm32/bCHARMJumptable.mli |   8 +-
 2 files changed, 175 insertions(+), 1 deletion(-)

diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMJumptable.ml b/CodeHawk/CHB/bchlibarm32/bCHARMJumptable.ml
index 1b315804..a02b6461 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHARMJumptable.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHARMJumptable.ml
@@ -240,6 +240,40 @@ let ldrtest
   | _ -> false
 
 
+let ldrs2test
+      (tmpreg: arm_reg_t)
+      (basereg: arm_reg_t)
+      (indexreg: arm_reg_t)
+      (instr: arm_assembly_instruction_int) =
+  match instr#get_opcode with
+  | LoadRegister (ACCAlways, rt, rn, rm, mem, false) ->
+     let _ =
+       chlog#add "ldrs2-test"
+         (LBLOCK [instr#get_address#toPretty;
+                  STR ": ";
+                  STR (BCHARMOpcodeRecords.arm_opcode_to_string instr#get_opcode);
+                  STR " with ";
+                  STR (BCHCPURegisters.armreg_to_string tmpreg);
+                  STR ", ";
+                  STR (BCHCPURegisters.armreg_to_string basereg);
+                  STR ", ";
+                  STR (BCHCPURegisters.armreg_to_string indexreg)
+         ]) in
+     rt#is_register
+     && rt#get_register = tmpreg
+     && rn#is_register
+     && rn#get_register = basereg
+     && rm#is_register
+     && rm#get_register = indexreg
+     && (match mem#get_kind with
+         | ARMOffsetAddress (_, _, offset, _, _, _, _) ->
+            (match offset with
+             | ARMShiftedIndexOffset (_, ARMImmSRT (SRType_LSL, 2), _) -> true
+             | _ -> false)
+         | _ -> false)
+  | _ -> false
+
+
 let ldrbtest
       (basereg: arm_reg_t)
       (indexreg: arm_reg_t)
@@ -899,6 +933,140 @@ let create_arm_add_pc_jumptable
      create_arm_add_pc_h_jumptable ch addpcinstr
 
 
+(* ADD-PC-LDR patterns (in ARM)
+
+   size is obtained from CMP instruction's immediate value
+   table start address is obtained from the ADR instruction
+
+   [4 bytes] CMP indexreg, maxcase
+   [4 bytes] BHI default address
+   [4 bytes] ADR basereg, start_address
+   [4 bytes] LDR scindexreg, [basereg, indexreg, LSL#2]
+   [4 bytes] ADD PC, basereg, scindexreg
+
+   Notes: These instructions always appear in the same order, but they may
+   be arbitrarily interleaved with other instructions, hence the large number
+   of offsets in finding the various instructions below.
+
+   Notes: encountered in a binary compiled with clang 18.1.3 on an arm64 host,
+   cross-compiled to arm32.
+ *)
+let is_arm_add_pc_adr_jumptable
+      (addpcinstr: arm_assembly_instruction_int):
+      (arm_assembly_instruction_int               (* CMP instr *)
+       * arm_assembly_instruction_int             (* BHI instr *)
+       * arm_assembly_instruction_int             (* ADR instr *)
+       * arm_assembly_instruction_int) option =   (* LDR instr *)
+  match addpcinstr#get_opcode with
+  | Add (_, ACCAlways, rd, baseregop, scindexregop, false)
+       when rd#is_pc_register
+            && baseregop#is_register
+            && scindexregop#is_register ->
+     let addr = addpcinstr#get_address in
+     let basereg = baseregop#get_register in
+     let scindexreg = scindexregop#get_register in  (* scaled index register *)
+     let cmptestf (instr: arm_assembly_instruction_int) =
+       match instr#get_opcode with
+       | Compare (_, rn, imm, _) -> rn#is_register && imm#is_immediate
+       | _ -> false in
+     let cmpinstr_o =
+       find_instr cmptestf [(-16); (-20); (-24); (-28); (-32); (-36)] addr in
+     (match cmpinstr_o with
+      | Some cmpinstr ->
+         (match cmpinstr#get_opcode with
+          | Compare (_, indexregop, _imm, _)  ->
+             let indexreg = indexregop#get_register in
+             let adrtestf = adr_reg_test basereg in
+             let ldrs2testf = ldrs2test scindexreg basereg indexreg in
+             let adrinstr_o = find_instr adrtestf [(-8); (-12)] addr in
+             let bhiinstr_o = find_instr bhi_test [(-12); (-16)] addr in
+             let ldrs2instr_o = find_instr ldrs2testf [(-4); (-8)] addr in
+             let _ =
+               if Option.is_none adrinstr_o then
+                 chlog#add "adr-jump table failure"
+                   (LBLOCK [addpcinstr#get_address#toPretty; STR ": adrinstr"]) in
+             let _ =
+               if Option.is_none bhiinstr_o then
+                 chlog#add "adr-jump table failure"
+                   (LBLOCK [addpcinstr#get_address#toPretty; STR ": bhiinstr"]) in
+             let _ =
+               if Option.is_none ldrs2instr_o then
+                 chlog#add "adr-jump table failure"
+                   (LBLOCK [addpcinstr#get_address#toPretty; STR ": ldrs2instr"]) in
+             (match (bhiinstr_o, adrinstr_o, ldrs2instr_o) with
+              | (Some bhiinstr, Some adrinstr, Some ldrs2instr) ->
+                 Some (cmpinstr, bhiinstr, adrinstr, ldrs2instr)
+              | _ -> None)
+          | _ ->
+             let _ =
+               chlog#add "arm-jumptable cmpinstr failure"
+                 (LBLOCK [addpcinstr#get_address#toPretty]) in
+             None)
+      | _ ->
+         let _ =
+           chlog#add "arm-jumptable cmpinstr failure (not found)"
+             (LBLOCK [addpcinstr#get_address#toPretty]) in
+         None)
+  | _ -> None
+
+
+let create_arm_add_pc_adr_jumptable
+      (ch: pushback_stream_int)
+      (addpcinstr: arm_assembly_instruction_int):
+      (arm_assembly_instruction_int list * arm_jumptable_int) option =
+  match is_arm_add_pc_adr_jumptable addpcinstr with
+  | None ->
+     begin
+       chlog#add "arm-jumptable: add-pc-addr (None)"
+         (LBLOCK [addpcinstr#get_address#toPretty]);
+       None
+     end
+  | Some (cmpinstr, bhiinstr, adrinstr, ldrinstr) ->
+     match (cmpinstr#get_opcode,
+            bhiinstr#get_opcode,
+            adrinstr#get_opcode,
+            ldrinstr#get_opcode) with
+     | (Compare (_, _, imm, _),
+        Branch (_, tgtop, _),
+        Adr (_, _, adrop),
+        LoadRegister (_, dstregop, _, _, _, _))
+          when tgtop#is_absolute_address && adrop#is_absolute_address ->
+        let iaddr = addpcinstr#get_address in
+        let defaulttgt = tgtop#get_absolute_address in
+        let size = imm#to_numerical#toInt in
+        let jtaddr = adrop#get_absolute_address in
+        let targets = ref [] in
+        let _ =
+          for i = 0 to size do
+            let offset = ch#read_num_signed_doubleword in
+            targets := (iaddr#add_int (4 + offset#toInt), i) :: !targets
+          done in
+        let endaddr = jtaddr#add_int (4 + (4 * size)) in
+        let jt:arm_jumptable_int =
+          make_arm_jumptable
+            ~end_address:endaddr
+            ~start_address:jtaddr
+            ~default_target:defaulttgt
+            ~targets:(List.rev !targets)
+            ~index_operand:dstregop
+            () in
+        let instrs =
+          [cmpinstr; bhiinstr; adrinstr; ldrinstr; addpcinstr] in
+        begin
+          chlog#add "arm-jumptable: add_pc_addr"
+            (LBLOCK [addpcinstr#get_address#toPretty;
+                     STR ": of size: ";
+                     INT size]);
+          Some (instrs, jt)
+        end
+     | _ ->
+        begin
+          chlog#add "arm-jumptable: add_pc_addr"
+            (LBLOCK [addpcinstr#get_address#toPretty;
+                     STR ": unsuccesful"]);
+          None
+        end
+
 (* format of BX-based jumptable (in Thumb-22):
 
    Type 1
diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMJumptable.mli b/CodeHawk/CHB/bchlibarm32/bCHARMJumptable.mli
index e060b0fa..64ff5c89 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHARMJumptable.mli
+++ b/CodeHawk/CHB/bchlibarm32/bCHARMJumptable.mli
@@ -4,7 +4,7 @@
    ------------------------------------------------------------------------------
    The MIT License (MIT)
 
-   Copyright (c) 2022-2024  Aarno Labs LLC
+   Copyright (c) 2022-2025  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
@@ -80,6 +80,12 @@ val create_arm_add_pc_jumptable:
   -> (arm_assembly_instruction_int list * arm_jumptable_int) option
 
 
+val create_arm_add_pc_adr_jumptable:
+  pushback_stream_int
+  -> arm_assembly_instruction_int
+  -> (arm_assembly_instruction_int list * arm_jumptable_int) option
+
+
 (** [create_bx_jumptable ch instr] creates a jump table targeted by a BX
     instruction [instr] by processing the associated list of addresses from
     stream [ch].*)

From d90912456b4ae942549249b902b2b7e754255cbb Mon Sep 17 00:00:00 2001
From: Henny Sipma <hennysipma@mac.com>
Date: Wed, 2 Jul 2025 14:09:33 -0700
Subject: [PATCH 14/16] CHB:ARM: add convenience function to access test
 instructions

---
 .../bchlibarm32/bCHARMAssemblyInstructions.ml | 23 ++++++++++++++++++-
 .../bCHARMAssemblyInstructions.mli            | 13 ++++++++++-
 2 files changed, 34 insertions(+), 2 deletions(-)

diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstructions.ml b/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstructions.ml
index c19c1bb3..d2fe2a89 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstructions.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstructions.ml
@@ -4,7 +4,7 @@
    ------------------------------------------------------------------------------
    The MIT License (MIT)
 
-   Copyright (c) 2021-2024  Aarno Labs, LLC
+   Copyright (c) 2021-2025  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
@@ -1138,3 +1138,24 @@ let get_aggregate (iaddr: doubleword_int): arm_instruction_aggregate_int =
 
 let get_arm_jumptables (): (doubleword_int * arm_jumptable_int) list =
   !arm_assembly_instructions#get_jumptables
+
+
+let get_associated_test_instr
+      (finfo: function_info_int)
+      (ctxtiaddr: ctxt_iaddress_t)
+    : (location_int * arm_assembly_instruction_int) option =
+  if finfo#has_associated_cc_setter ctxtiaddr then
+    let faddr = finfo#get_address in
+    let testiaddr = finfo#get_associated_cc_setter ctxtiaddr in
+    let testloc = BCHLocation.ctxt_string_to_location faddr testiaddr in
+    let testaddr = testloc#i in
+    TR.tfold
+      ~ok:(fun testinstr -> Some (testloc, testinstr))
+      ~error:(fun e ->
+        begin
+          log_error_result __FILE__ __LINE__ e;
+          None
+        end)
+      (get_arm_assembly_instruction testaddr)
+  else
+    None
diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstructions.mli b/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstructions.mli
index 99652843..7f1307b9 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstructions.mli
+++ b/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstructions.mli
@@ -102,9 +102,20 @@ val has_aggregate: doubleword_int -> bool
 
 (** [get_aggregate iaddr] returns the aggregate registered at virtual address [iaddr].
 
-    @raises [BCH_failure] if no aggregate is registered at [iaddr].*)
+    raise BCH_failure if no aggregate is registered at [iaddr].*)
 val get_aggregate: doubleword_int -> arm_instruction_aggregate_int
 
 
 
 val get_arm_jumptables: unit -> (doubleword_int * arm_jumptable_int) list
+
+
+(** [get_associated_test_instr finfo iaddr] returns the location and instruction
+    that provides the test that is associated with the condition code of the
+    instruction at address [iaddr]
+
+    If no test instruction is associated with the instruction at [iaddr] [None]
+    is returned.
+ *)
+val get_associated_test_instr:
+  function_info_int -> ctxt_iaddress_t -> (location_int * arm_assembly_instruction_int) option

From 6e697bc153a8aef75eb0caee78935902ecf716db Mon Sep 17 00:00:00 2001
From: Henny Sipma <hennysipma@mac.com>
Date: Tue, 8 Jul 2025 08:42:15 -0700
Subject: [PATCH 15/16] CHB: support for ternary assignment aggregate

---
 CodeHawk/CH/xprlib/xsimplify.ml               |   5 +-
 .../bchlibarm32/bCHARMInstructionAggregate.ml | 100 ++-
 .../bCHARMInstructionAggregate.mli            | 185 +++++-
 CodeHawk/CHB/bchlibarm32/bCHARMTypes.mli      |  18 +-
 .../CHB/bchlibarm32/bCHFnARMDictionary.ml     | 177 +++--
 .../bchlibarm32/bCHFnARMTypeConstraints.ml    |  15 +-
 .../CHB/bchlibarm32/bCHTranslateARMToCHIF.ml  | 605 +++++++++---------
 CodeHawk/CHT/tchlib/tCHTest.mli               |   4 +-
 8 files changed, 748 insertions(+), 361 deletions(-)

diff --git a/CodeHawk/CH/xprlib/xsimplify.ml b/CodeHawk/CH/xprlib/xsimplify.ml
index 9b5d77cd..04f73bec 100644
--- a/CodeHawk/CH/xprlib/xsimplify.ml
+++ b/CodeHawk/CH/xprlib/xsimplify.ml
@@ -175,7 +175,8 @@ and reduce_neg (m: bool) (e1: xpr_t): (bool * xpr_t) =
   | _ -> default ()
 
 
-(* Note that for values other than zero the result depends on word size.*)
+(* Note that, in general, for values other than zero the result depends on word
+   size. Here we assume that the word is at least 8 bits wide. *)
 and reduce_bitwise_not (m: bool) (e1: xpr_t): (bool * xpr_t) =
   let default () = (m, XOp (XBNot, [e1])) in
   match e1 with
@@ -183,6 +184,8 @@ and reduce_bitwise_not (m: bool) (e1: xpr_t): (bool * xpr_t) =
      (true, XConst (IntConst numerical_one#neg))
   | XConst (IntConst num) when num#equal numerical_one ->
      (true, XConst (IntConst (mkNumerical 2)#neg))
+  | XConst (IntConst n) when n#lt numerical_e8 ->
+     (true, XConst (IntConst (n#neg#sub numerical_one)))
   | _ -> default ()
 
 
diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMInstructionAggregate.ml b/CodeHawk/CHB/bchlibarm32/bCHARMInstructionAggregate.ml
index 7fed24c4..9c2bbadb 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHARMInstructionAggregate.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHARMInstructionAggregate.ml
@@ -4,7 +4,7 @@
    ------------------------------------------------------------------------------
    The MIT License (MIT)
 
-   Copyright (c) 2022-2024  Aarno Labs, LLC
+   Copyright (c) 2022-2025  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
@@ -66,6 +66,13 @@ let arm_aggregate_kind_to_string (k: arm_aggregate_kind_t) =
   | ARMPredicateAssignment (inverse, op) ->
      let inv = if inverse then " (inverse)" else "" in
      "predicate assignment to " ^ op#toString ^ inv
+  | ARMTernaryAssignment (dst, op1, op2) ->
+     "ternary assignment: "
+     ^ dst#toString
+     ^ " = cond ? "
+     ^ op1#toString
+     ^ " : "
+     ^ op2#toString
   | BXCall (_, i2) -> "BXCall at " ^ i2#get_address#to_hex_string
 
 
@@ -140,6 +147,11 @@ object (self)
     | ARMPredicateAssignment _ -> true
     | _ -> false
 
+  method is_ternary_assign =
+    match self#kind with
+    | ARMTernaryAssignment _ -> true
+    | _ -> false
+
   method write_xml (_node: xml_element_int) = ()
 
   method toCHIF (_faddr: doubleword_int) = []
@@ -258,6 +270,21 @@ let make_predassign_aggregate
     ~anchor:mov2
 
 
+let make_ternassign_aggregate
+      (mov1: arm_assembly_instruction_int)
+      (mov2: arm_assembly_instruction_int)
+      (dstop: arm_operand_int)
+      (n1: numerical_t)
+      (n2: numerical_t): arm_instruction_aggregate_int =
+  let kind = ARMTernaryAssignment(dstop, n1, n2) in
+  make_arm_instruction_aggregate
+    ~kind
+    ~instrs:[mov1; mov2]
+    ~entry:mov1
+    ~exitinstr:mov2
+    ~anchor:mov2
+
+
 let disassemble_arm_instructions
       (ch: pushback_stream_int) (iaddr: doubleword_int) (n: int) =
   for _i = 1 to n do
@@ -293,6 +320,8 @@ let identify_jumptable
   | Add (_, ACCNotUnsignedHigher, rd, rn, _, false)
        when rd#is_pc_register && rn#is_pc_register ->
      create_addls_pc_jumptable ch instr
+  | Add (_, ACCAlways, rd, _, _, false) when rd#is_pc_register ->
+     create_arm_add_pc_adr_jumptable ch instr
   | BranchExchange (ACCAlways, regop) when regop#is_register ->
      create_arm_bx_jumptable ch instr
   | _ -> None
@@ -494,6 +523,67 @@ let identify_predicate_assignment
   | _ -> None
 
 
+(* format of ternary assignment (in ARM): assigns one value or another depending
+   on the result of a test:
+
+  MOVNE Rx, imm1
+  MOVEQ Rx, imm2
+
+or
+
+  MVNEQ Rx, imm1
+  MOVNE Rx, imm2
+ *)
+let identify_ternary_assignment
+      (_ch: pushback_stream_int)
+      (instr: arm_assembly_instruction_int):
+      (arm_assembly_instruction_int
+       * arm_assembly_instruction_int
+       * arm_operand_int
+       * numerical_t
+       * numerical_t) option =
+  let negval (n: numerical_t) =
+    match Xsimplify.simplify_xpr (XOp (XBNot, [Xprt.num_constant_expr n])) with
+    | XConst (IntConst nn) -> Some nn
+    | _ -> None in
+  match instr#get_opcode with
+  | Move (false, c2, rd, imm2, _, _)
+    | BitwiseNot (false, c2, rd, imm2, _)
+       when imm2#is_immediate && (has_inverse_cc c2) ->
+     let optn2 =
+       let n2 = imm2#to_numerical in
+       match instr#get_opcode with
+       | Move _ -> Some n2
+       | BitwiseNot _ -> negval n2
+       | _ -> None in
+     (match optn2 with
+      | Some n2 ->
+         let rdreg = rd#get_register in
+         let addr = instr#get_address in
+         let movinstr_r = get_arm_assembly_instruction (addr#add_int (-4)) in
+         (match TR.to_option movinstr_r with
+          | Some movinstr ->
+             (match movinstr#get_opcode with
+              | Move (false, c1, rd, imm1, _, _)
+                   when imm1#is_immediate
+                        && (rd#get_register = rdreg)
+                        && (has_inverse_cc c1)
+                        && ((Option.get (get_inverse_cc c1)) = c2) ->
+                 Some (movinstr, instr, rd, imm1#to_numerical, n2)
+              | BitwiseNot (false, c1, rd, imm1, _)
+                   when imm1#is_immediate
+                        && (rd#get_register = rdreg)
+                        && (has_inverse_cc c1)
+                        && ((Option.get (get_inverse_cc c1)) = c2) ->
+                 (match (negval imm1#to_numerical) with
+                  | Some n1 -> Some (movinstr, instr, rd, n1, n2)
+                  | _ -> None)
+              | _ -> None)
+          | _ -> None)
+      | _ -> None)
+  | _ -> None
+
+
 let identify_arm_aggregate
       (ch: pushback_stream_int)
       (instr: arm_assembly_instruction_int):
@@ -558,4 +648,12 @@ let identify_arm_aggregate
        | Some (inverse, mov1, mov2, dstop) ->
           Some (make_predassign_aggregate inverse mov1 mov2 dstop)
        | _ -> None in
+  let result =
+    match result with
+    | Some _ -> result
+    | _ ->
+       match identify_ternary_assignment ch instr with
+       | Some (mov1, mov2, dstop, n1, n2) ->
+          Some (make_ternassign_aggregate mov1 mov2 dstop n1 n2)
+       | _ -> None in
   result
diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMInstructionAggregate.mli b/CodeHawk/CHB/bchlibarm32/bCHARMInstructionAggregate.mli
index d4a1ad78..9022b112 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHARMInstructionAggregate.mli
+++ b/CodeHawk/CHB/bchlibarm32/bCHARMInstructionAggregate.mli
@@ -1,10 +1,10 @@
 (* =============================================================================
-   CodeHawk Binary Analyzer 
+   CodeHawk Binary Analyzer
    Author: Henny Sipma
    ------------------------------------------------------------------------------
    The MIT License (MIT)
- 
-   Copyright (c) 2022-2024  Aarno Labs, LLC
+
+   Copyright (c) 2022-2025  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
@@ -12,10 +12,10 @@
    to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
    copies of the Software, and to permit persons to whom the Software is
    furnished to do so, subject to the following conditions:
- 
+
    The above copyright notice and this permission notice shall be included in all
    copies or substantial portions of the Software.
-  
+
    THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
    IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
    FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
@@ -25,18 +25,169 @@
    SOFTWARE.
    ============================================================================= *)
 
-(** Sequence of consecutive assembly instructions that represents a semantic unit.
-    
-    Examples:
-    - switch statement constructed by 
-      - table branch instructions (TBB/TBH), or
-      - load from table into pc
-      - indirect jump from table
-      
-    - question expression constructed by Thumb-2 if-then instruction
-    
-    In translation to CHIF, semantics are obtained from the anchor, all other
-    instructions belonging to the aggregate are ignored.
+
+(** {1 Instruction aggregates: Overview} *)
+
+(** {2 Description}
+
+    An instruction aggregate is a (usually, but not always, contiguous)
+    sequence of two or more instructions that is treated as a single
+    semantic unit. The semantics for the entire sequence is assigned to
+    one of the instructions (often the last one in the sequence) and all
+    other instructions are considere no-ops by all subsequent analyses.
+
+    Instruction aggregates cover a variety of constructs ranging from
+    predicate and ternary assignments to jump tables.
+
+    {2 Motivation}
+
+    The rationale behind combining a sequence of instructions into an
+    aggregate is that the collective action of the individual instructions
+    combined is not easily apparent from considering their semantics in
+    isolation. The instructions usually collaborate in a very specific
+    way to achieve a particular result, with operands from different instructions
+    playing playing a specific role. This is especially true of the jump
+    table aggregates. For some of the other aggregate kinds the semantics
+    of the individual instructions combined would be similar, but analysis
+    of the aggregate is more efficient and precise. For example, this is
+    the case with the predicate assignment:
+    {[
+    <test>
+    MOVcc   Rx, #1
+    MOVcc'  Rx, #0   where cc' is (not cc)
+    ]}
+    The two MOV instructions can be combined into one assignment of the
+    boolean <test-cc>:
+    {[
+    Rx := <test-cc>
+    ]}
+    Translating and analyzing the two instructions in isolation produces
+    two joins, and potentially three reaching definitions for a subsequent
+    use of Rx. In contrast, the two instructions combined into one
+    predicate assignment produces zero joins, and only a single reaching
+    definition for a subsequent use of Rx, a considerable improvement.
+
+    {2 Identification}
+
+    Instruction aggregates are identified during disassembly by pattern
+    matching. Identification is entirely syntactic, so only the information
+    present in the instructions themselves, such as opcode and operands,
+    are used; not the possible values that those operands may have, unless
+    they are immediates.
+
+    {2 Representation}
+
+    The aggregate is represented by objects of the class type
+    [arm_instruction_aggregate_int]. These objects contain the kind of
+    aggregate, a list of the contributing instructions, and information
+    about its entry, exit, and anchor address. The anchor is the
+    instruction to which the full semantics of the aggregate is assigned.
+
+    Cross references to instances are recorded in the [arm_assembly_instruction_int]
+    instances of the instructions that make up the aggregate to enable
+    triggering proper translation and analysis. The collection of all
+    aggregates themselves is maintained in the singleton object of type
+    [arm_assembly_instructions_int].
+
+    Most aggregates are contained within a single basic block and do not
+    affect control flow. The exceptions are jump tables, whose components
+    are directly incorporated into the CFG during disassembly and require
+    no further semantic handling.
+
+    {2 Translation into CHIF}
+
+    The semantics of the aggregate is explicated in the translation into
+    CHIF. In general, instructions are individually translated into CHIF
+    (in the function [translate_arm_instruction]). In the case of aggregates
+    CHIF is generated for the full semantics at the anchor instruction,
+    while all other other instructions in the aggregate are treated as
+    no-ops. In the case of jump tables the full semantics is already
+    incorporated in the CFG during disassembly and all instructions in
+    the aggregate are treated as no-ops.
+
+    {2 Transfer to front end}
+
+    The kind and structure of aggregates and analysis results involving
+    their components are communicated to the (python) front end in the
+    instruction results data contained in the function opcode dictionary
+    (see bCHFnARMDictionary). The format varies with the kind of aggregate,
+    as each kind has different types of values that characterize its
+    operation. In the (python) front end these values are made accessible
+    to the various instructions in the [InstrXData] objects created for
+    each instruction. The documentation of each aggregate kind below and
+    elsewhere presents more details on the actual format for each of these.
+
+    {2 Tests}
+
+    Currenly only two of the kinds of aggregates have associated unit tests:
+    - bCHARMJumpTableTest
+    - bCHThumbITSequenceTest
+    These tests contain instances of code fragments encountered in actual
+    binaries and give some insight in their use.
+
+
+    {1 Predicate Assignments}
+
+    {2 Description}
+
+    A predicate assignment aggregate consists of two assignment instructions
+    that combine into a single assignment of a boolean predicate. The pattern
+    for the aggregate is two adjacent MOV instructions of the form:
+    {[
+    <test>
+    MOVcc  Rx, #1
+    MOVcc' Rx, #0  where cc' is (not cc)
+    ]}
+    or
+    {[
+    <test>
+    MOVcc' Rx, #0
+    MOVcc  Rx, #1  where cc is not (cc')
+    ]}
+    In all executions exactly one of these two MOV instructions is executed.
+    If the joint condition <test-cc> is true Rx is assigned 1, if it is false
+    Rx is assigned 0, and thus the postcondition of these two instructions
+    is essentially the assignment of the boolean <test-cc>.
+
+    {3 Example}
+
+    {[
+    <CMP R0, #5>
+    MOVNE  R1, #0
+    MOVEQ  R1, #1
+    ]}
+    is translated into
+    {[ R1 := (R0 == 5)  ]}
+
+    {2 Representation}
+
+    The [arm_instruction_aggregate] instance of the predicate assignment
+    records the address of the second instruction as the anchor, the
+    destination operand, and whether the <test-cc> predicate is to be
+    inverted, where cc is the condition code for the anchor instruction.
+    The predicate is to be inverted if the anchor instruction assigns 0.
+
+    {2 Translation to CHIF}
+
+    The first MOV instruction is translated into a no-op. The second
+    MOV instruction is translated into the assignment
+    {[ Rx := [not] predicate ]}
+    with the single defined variable Rx, and with variables used all
+    variables referenced in the predicate.
+
+    If a predicate cannot be constructed or derived, the destination
+    variable Rx is abstracted.
+
+    {2 Transfer to front end}
+
+    The first instruction is tagged as 'subsumed' by the second
+    instruction, and thus to be treated as a no-op. The second
+    instruction is tagged with 'agg:predassign' with a list of
+    dependents (the first instruction in this case). It lists as
+    a variable the destination operand, along with its (high)
+    uses. If a predicate was construction, it lists
+    (the possibly inverse of) the predicate in its original and
+    rewritten form, along with its reaching definitions.
  *)
 
 (* bchlib *)
diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMTypes.mli b/CodeHawk/CHB/bchlibarm32/bCHARMTypes.mli
index b1c09332..6a0d4330 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHARMTypes.mli
+++ b/CodeHawk/CHB/bchlibarm32/bCHARMTypes.mli
@@ -4,7 +4,7 @@
    ------------------------------------------------------------------------------
    The MIT License (MIT)
 
-   Copyright (c) 2021-2024 Aarno Labs, LLC
+   Copyright (c) 2021-2025 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
@@ -1449,6 +1449,20 @@ class type arm_assembly_instruction_int =
   end
 
 
+(** {1 Instruction aggregates} *)
+
+(** An instruction aggregate is a (usually, but not always, contiguous)
+    sequence of two or more instructions that is treate as a single
+    semantic unit. The semantics for the entire sequence is assigned to
+    one of the instructions (often the last one in the sequence) and all
+    other instructions are considere no-ops by all subsequent analyses.
+
+    Instruction aggregates cover a variety of constructs ranging from
+    predicate and ternary assignments to jump tables.
+
+    A more detailed description is provided in [bCHARMInstructionAggregate].
+ *)
+
 type arm_assembly_instruction_result = arm_assembly_instruction_int traceresult
 
 
@@ -1534,6 +1548,7 @@ type arm_aggregate_kind_t =
       * arm_assembly_instruction_int
       * arm_assembly_instruction_int
   | ARMPredicateAssignment of bool * arm_operand_int
+  | ARMTernaryAssignment of arm_operand_int * numerical_t * numerical_t
   | BXCall of arm_assembly_instruction_int * arm_assembly_instruction_int
 
 
@@ -1560,6 +1575,7 @@ class type arm_instruction_aggregate_int =
     method is_pseudo_ldrsh: bool
     method is_pseudo_ldrsb: bool
     method is_predicate_assign: bool
+    method is_ternary_assign: bool
 
     (* i/o *)
     method write_xml: xml_element_int -> unit
diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml
index d9b9afa4..209d76f7 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml
@@ -234,6 +234,23 @@ object (self)
           xpr in
       simplify_xpr xpr in
 
+    let rewrite_in_cc_context
+          (floc: floc_int) (cc: arm_opcode_cc_t) (x: xpr_t): xpr_t =
+      let xx = rewrite_expr x in
+      match cc with
+      | ACCAlways -> xx
+      | _ when instr#is_condition_covered -> xx
+      | _ when is_cond_conditional cc && floc#has_test_expr ->
+         let txpr = floc#get_test_expr in
+         let tcond = rewrite_expr txpr in
+         (match tcond with
+          | XOp (XEq, [XVar vr; XConst (IntConst n)]) ->
+             let subst v =
+               if v#equal vr then XConst (IntConst n) else XVar vr in
+             simplify_xpr (substitute_expr subst xx)
+          | _ -> xx)
+      | _ -> xx in
+
     let flagrdefs: int list =
       let flags_used = get_arm_flags_used instr#get_opcode in
       List.concat
@@ -536,8 +553,10 @@ object (self)
          let csetter = floc#f#get_associated_cc_setter floc#cia in
          let txpr = floc#get_test_expr in
          let fxpr = simplify_xpr (XOp (XLNot, [txpr])) in
-         let tcond = rewrite_test_expr csetter txpr in
-         let fcond = rewrite_test_expr csetter fxpr in
+         (* we can rewrite with invariants at this address, since the expression
+            should have been made position independent for local variables.*)
+         let tcond = rewrite_expr txpr in
+         let fcond = rewrite_expr fxpr in
          let ctcond_r = floc#convert_xpr_to_c_expr ~size:(Some 4) tcond in
          let cfcond_r = floc#convert_xpr_to_c_expr ~size:(Some 4) fcond in
          let rdefs = (get_all_rdefs txpr) @ (get_all_rdefs tcond) in
@@ -554,7 +573,8 @@ object (self)
          let icrtag = "icr:" ^ (string_of_int (argslen + 1)) in
          let icctag = "icc:" ^ (string_of_int (argslen + 2)) in
          let iccrtag = "iccr:" ^ (string_of_int (argslen + 3)) in
-         let tags = xtag :: [ictag; icrtag; icctag; iccrtag] in
+         let icsetter = "icsetter:" ^ csetter in
+         let tags = xtag :: [ictag; icrtag; icctag; iccrtag; icsetter] in
          let args = args @ newargs in
          (tags, args)
       | _ -> (tagstring :: ["uc"], args) in
@@ -966,6 +986,14 @@ object (self)
          let (tags, args) = add_optional_instr_condition tagstring args c in
          (tags, args)
 
+      | BitwiseNot _ when (Option.is_some instr#is_in_aggregate) ->
+         (* TODO: add output for the case where BitwiseNot is the anchor *)
+         (match instr#is_in_aggregate with
+          | Some va ->
+             let ctxtva = (make_i_location floc#l va)#ci in
+             ("a:" :: ["subsumed"; ctxtva], [])
+          | _ -> (["a:"], []))
+
       | BitwiseNot (_, c, rd, rm, _) ->
          let vrd_r = rd#to_variable floc in
          let xrm_r = rm#to_expr floc in
@@ -2009,6 +2037,8 @@ object (self)
          let result_r =
            TR.tmap2 (fun xrn xrm -> XOp (XLsl, [xrn; xrm])) xrn_r xrm_r in
          let rresult_r = TR.tmap rewrite_expr result_r in
+         let cresult_r =
+           TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) rresult_r in
          let rdefs =
            [get_rdef_r xrn_r; get_rdef_r xrm_r] @ (get_all_rdefs_r rresult_r) in
          let uses = [get_def_use_r vrd_r] in
@@ -2017,6 +2047,7 @@ object (self)
            mk_instrx_data_r
              ~vars_r:[vrd_r]
              ~xprs_r:[xrn_r; xrm_r; result_r; rresult_r]
+             ~cxprs_r:[cresult_r]
              ~rdefs
              ~uses
              ~useshigh
@@ -2032,6 +2063,8 @@ object (self)
          let result_r =
            TR.tmap2 (fun xrn xrm -> XOp (XLsr, [xrn; xrm])) xrn_r xrm_r in
          let rresult_r = TR.tmap rewrite_expr result_r in
+         let cresult_r =
+           TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) rresult_r in
          let rdefs =
            [get_rdef_r xrn_r; get_rdef_r xrm_r] @ (get_all_rdefs_r rresult_r) in
          let uses = [get_def_use_r vrd_r] in
@@ -2040,6 +2073,7 @@ object (self)
            mk_instrx_data_r
              ~vars_r:[vrd_r]
              ~xprs_r:[xrn_r; xrm_r; result_r; rresult_r]
+             ~cxprs_r:[cresult_r]
              ~rdefs
              ~uses
              ~useshigh
@@ -2050,52 +2084,99 @@ object (self)
       | Move _ when instr#is_aggregate_anchor ->
          let finfo = floc#f in
          let ctxtiaddr = floc#l#ci in
-         if finfo#has_associated_cc_setter ctxtiaddr then
-           let testiaddr = finfo#get_associated_cc_setter ctxtiaddr in
-           let testloc = ctxt_string_to_location faddr testiaddr in
-           let testaddr = testloc#i in
-           let testinstr =
-             fail_tvalue
-               (trerror_record
-                  (LBLOCK [
-                       STR "FnDictionary: predicate assignment"; floc#ia#toPretty]))
-               (get_arm_assembly_instruction testaddr) in
-           let agg = get_aggregate floc#ia in
+         let agg = get_aggregate floc#ia in
+         let (tags, args) =
            (match agg#kind with
-            | ARMPredicateAssignment (inverse, dstop) ->
-               let (_, optpredicate, _) =
-                 arm_conditional_expr
-                   ~condopc:instr#get_opcode
-                   ~testopc:testinstr#get_opcode
-                   ~condloc:floc#l
-                   ~testloc:testloc in
-               let (tags, args) =
-                 (match optpredicate with
-                  | Some p ->
-                     let p = if inverse then XOp (XLNot, [p]) else p in
-                     let lhs_r = dstop#to_variable floc in
-                     let rdefs = get_all_rdefs p in
-                     let xp = rewrite_expr p in
-                     let (tagstring, args) =
-                       mk_instrx_data_r
-                         ~vars_r:[lhs_r]
-                         ~xprs_r:[Ok p; Ok xp]
-                         ~rdefs
-                         ~uses:[get_def_use_r lhs_r]
-                         ~useshigh:[get_def_use_high_r lhs_r]
-                         () in
-                     ([tagstring], args)
-                  | _ ->
-                     ([], [])) in
-               let dependents =
-                 List.map (fun d ->
-                     (make_i_location floc#l d#get_address)#ci) agg#instrs in
-               let tags = tags @ ["subsumes"] @ dependents in
-               (tags, args)
+            | ARMPredicateAssignment (_, dstop)
+              | ARMTernaryAssignment (dstop, _, _) ->
+               let lhs_r = dstop#to_variable floc in
+               let uses = [get_def_use_r lhs_r] in
+               let useshigh = [get_def_use_high_r lhs_r] in
+               (match get_associated_test_instr finfo ctxtiaddr with
+                | Some (testloc, testinstr) ->
+                   let (_, optpredicate, _) =
+                     arm_conditional_expr
+                       ~condopc:instr#get_opcode
+                       ~testopc:testinstr#get_opcode
+                       ~condloc:floc#l
+                       ~testloc in
+                   (match agg#kind with
+                    | ARMPredicateAssignment (inverse, _) ->
+                       (match optpredicate with
+                        | Some p ->
+                           let p = if inverse then XOp (XLNot, [p]) else p in
+                           let rdefs = get_all_rdefs p in
+                           let xp = rewrite_expr p in
+                           let cxp_r = floc#convert_xpr_to_c_expr ~size:(Some 4) xp in
+                           let (tagstring, args) =
+                             mk_instrx_data_r
+                               ~vars_r:[lhs_r]
+                               ~xprs_r:[Ok p; Ok xp]
+                               ~cxprs_r:[cxp_r]
+                               ~rdefs
+                               ~uses
+                               ~useshigh
+                               () in
+                           ([tagstring; "agg:predassign"], args)
+                        | _ ->
+                           let (tagstring, args) =
+                             mk_instrx_data_r ~vars_r:[lhs_r] ~uses ~useshigh () in
+                           ([tagstring; "agg:predassign:nd"], args))
+                    | ARMTernaryAssignment (_, n1, n2) ->
+                       let xp1 = num_constant_expr n1 in
+                       let xp2 = num_constant_expr n2 in
+                       (match optpredicate with
+                        | Some p ->
+                           let xp = rewrite_expr p in
+                           let cxp_r = floc#convert_xpr_to_c_expr ~size:(Some 4) xp in
+                           let rdefs = get_all_rdefs p in
+                           let (tagstring, args) =
+                             mk_instrx_data_r
+                               ~vars_r:[lhs_r]
+                               ~xprs_r:[Ok p; Ok xp; Ok xp1; Ok xp2]
+                               ~cxprs_r: [cxp_r]
+                               ~rdefs
+                               ~uses
+                               ~useshigh
+                               () in
+                           ([tagstring; "agg:ternassign"], args)
+                        | _ ->
+                           let (tagstring, args) =
+                             mk_instrx_data_r
+                               ~vars_r:[lhs_r]
+                               ~xprs_r:[Ok xp1; Ok xp2]
+                               ~uses
+                               ~useshigh
+                               () in
+                           ([tagstring; "agg:ternassign:nd"], args))
+                    | _ ->
+                       raise
+                         (BCH_failure
+                            (LBLOCK [
+                                 STR __FILE__; STR ":"; INT __LINE__; STR ": ";
+                                 floc#l#toPretty;
+                                 STR ": unknown MOV aggregate"])))
+                | _ ->
+                   (* no associated test instr found *)
+                   let (tagstring, args) =
+                     mk_instrx_data_r ~vars_r:[lhs_r] ~uses ~useshigh () in
+                   let tags = match agg#kind with
+                     | ARMPredicateAssignment _ -> [tagstring; "agg:predassign:nd"]
+                     | ARMTernaryAssignment _ -> [tagstring; "agg:ternassign:nd"]
+                     | _ -> [tagstring] in
+                   (tags, args))
             | _ ->
-               ([], []))
-         else
-           ([], [])
+               raise
+                 (BCH_failure
+                    (LBLOCK [
+                         STR __FILE__; STR ":"; INT __LINE__; STR ": ";
+                         floc#l#toPretty;
+                         STR ": unknown MOV aggregate"]))) in
+         let dependents =
+           List.map (fun d ->
+               (make_i_location floc#l d#get_address)#ci) agg#instrs in
+         let tags = tags @ ["subsumes"] @ dependents in
+         (tags, args)
 
       | Move _ when (Option.is_some instr#is_in_aggregate) ->
          (match instr#is_in_aggregate with
@@ -3067,7 +3148,7 @@ object (self)
          let xrm_r = rm#to_expr floc in
          let result_r =
            TR.tmap2 (fun xrn xrm -> XOp (XMinus, [xrn; xrm])) xrn_r xrm_r in
-         let rresult_r = TR.tmap rewrite_expr result_r in
+         let rresult_r = TR.tmap (rewrite_in_cc_context floc c) result_r in
          let cresult_r =
            TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) rresult_r in
          let rdefs =
diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml
index 23e1af8a..dfabde71 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml
@@ -1300,7 +1300,20 @@ object (self)
              begin
                log_subtype_constraint __LINE__ "SUB-rdef-1" rntypeterm lhstypeterm;
                store#add_subtype_constraint rntypeterm lhstypeterm
-             end) rndefs
+             end) rndefs;
+
+         (* propagate function return type *)
+         (if rd#get_register = AR0 && (has_exit_use_r (rd#to_variable floc)) then
+            let regvar = mk_reglhs_typevar rdreg faddr iaddr in
+            let fvar = mk_function_typevar faddr in
+            let fvar = add_return_capability fvar in
+            let regterm = mk_vty_term regvar in
+            let fterm = mk_vty_term fvar in
+            begin
+              log_subtype_constraint __LINE__ "SUB-freturn" regterm fterm;
+              store#add_subtype_constraint regterm fterm
+            end);
+
        end
 
     | UnsignedBitFieldExtract (_, _, rn) ->
diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml
index 159d9278..43eafc82 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml
@@ -117,6 +117,14 @@ let package_transaction
   TRANSACTION (label, LF.mkCode (cnstAssigns @ cmds), None)
 
 
+(* Returns the predicate instruction and associated info for a conditional,
+   in particular, it returns a tuple consisting of:
+   - a list of temporary variables created to preserve the (frozen) values
+     at the test location (testloc) for the location of the conditional (condloc)
+   - the predicate that expresses the joint condition of test and condition
+     code (cc, e.g., EQ), and
+   - a list of the operands used in the creation of the predicate
+ *)
 let make_conditional_predicate
       ~(condinstr: arm_assembly_instruction_int)
       ~(testinstr: arm_assembly_instruction_int)
@@ -141,54 +149,29 @@ let make_instr_local_tests
   let env = testfloc#f#env in
   let reqN () = env#mk_num_temp in
   let reqC i = env#request_num_constant i in
-  let (frozenVars, optboolxpr, _) =
-    if is_opcode_conditional testinstr#get_opcode then
-      let finfo = testfloc#f in
-      let faddr = testfloc#fa in
-      if finfo#has_associated_cc_setter testloc#ci then
-        let testtestiaddr = finfo#get_associated_cc_setter testloc#ci in
-        let testtestloc = ctxt_string_to_location faddr testtestiaddr in
-        let testtestaddr = testtestloc#i in
-        let testtestinstr =
-          fail_tvalue
-            (trerror_record
-               (LBLOCK [STR "Internal error in make_instr_local_tests"]))
-            (get_arm_assembly_instruction testtestaddr) in
-        let _ =
-          if collect_diagnostics () then
-            ch_diagnostics_log#add
-              "conditional conditional test"
-              (LBLOCK [
-                   testfloc#l#toPretty;
-                   STR ": ";
-                   STR (arm_opcode_to_string testinstr#get_opcode);
-                   STR " with setter ";
-                   STR (arm_opcode_to_string testtestinstr#get_opcode)]) in
-        arm_conditional_conditional_expr
-          ~condopc:condinstr#get_opcode
-          ~testopc: testinstr#get_opcode
-          ~testtestopc: testtestinstr#get_opcode
-          ~condloc
-          ~testloc
-          ~testtestloc
-      else
-        arm_conditional_expr
-          ~condopc:condinstr#get_opcode
-          ~testopc:testinstr#get_opcode
-          ~condloc
-          ~testloc
-    else
-      arm_conditional_expr
-        ~condopc:condinstr#get_opcode
-        ~testopc:testinstr#get_opcode
-        ~condloc
-        ~testloc in
-(*  let (frozenVars, optboolxpr) =
+  let get_default_conditional_expr () =
     arm_conditional_expr
       ~condopc:condinstr#get_opcode
       ~testopc:testinstr#get_opcode
       ~condloc
-      ~testloc in *)
+      ~testloc in
+  let (frozenVars, optboolxpr, _) =
+    if is_opcode_conditional testinstr#get_opcode then
+      let finfo = testfloc#f in
+      match get_associated_test_instr finfo testloc#ci with
+      | Some (testtestloc, testtestinstr) ->
+         arm_conditional_conditional_expr
+           ~condopc:condinstr#get_opcode
+           ~testopc: testinstr#get_opcode
+           ~testtestopc: testtestinstr#get_opcode
+           ~condloc
+           ~testloc
+           ~testtestloc
+      | _ ->
+         get_default_conditional_expr ()
+    else
+      get_default_conditional_expr () in
+
   let convert_to_chif expr =
     let (cmds,bxpr) = xpr_to_boolexpr reqN reqC expr in
     cmds @ [ASSERT bxpr] in
@@ -255,29 +238,17 @@ let make_tests
   let env = testfloc#f#env in
   let reqN () = env#mk_num_temp in
   let reqC i = env#request_num_constant i in
+  let get_default_conditional_expr () =
+    arm_conditional_expr
+      ~condopc:condinstr#get_opcode
+      ~testopc:testinstr#get_opcode
+      ~condloc
+      ~testloc in
   let (frozenVars, optboolxpr, _) =
     if is_opcode_conditional testinstr#get_opcode then
       let finfo = testfloc#f in
-      let faddr = testfloc#fa in
-      if finfo#has_associated_cc_setter testloc#ci then
-        let testtestiaddr = finfo#get_associated_cc_setter testloc#ci in
-        let testtestloc = ctxt_string_to_location faddr testtestiaddr in
-        let testtestaddr = testtestloc#i in
-        let testtestinstr =
-          fail_tvalue
-            (trerror_record
-               (LBLOCK [STR "Internal error in make_instr_local_tests"]))
-            (get_arm_assembly_instruction testtestaddr) in
-        let _ =
-          if collect_diagnostics () then
-            ch_diagnostics_log#add
-              "conditional conditional test"
-              (LBLOCK [
-                   testfloc#l#toPretty;
-                   STR ": ";
-                   STR (arm_opcode_to_string testinstr#get_opcode);
-                   STR " with setter ";
-                   STR (arm_opcode_to_string testtestinstr#get_opcode)]) in
+      match get_associated_test_instr finfo testloc#ci with
+      | Some (testtestloc, testtestinstr) ->
         arm_conditional_conditional_expr
           ~condopc:condinstr#get_opcode
           ~testopc: testinstr#get_opcode
@@ -285,18 +256,10 @@ let make_tests
           ~condloc
           ~testloc
           ~testtestloc
-      else
-        arm_conditional_expr
-          ~condopc:condinstr#get_opcode
-          ~testopc:testinstr#get_opcode
-          ~condloc
-          ~testloc
+      | _ ->
+         get_default_conditional_expr ()
     else
-      arm_conditional_expr
-        ~condopc:condinstr#get_opcode
-        ~testopc:testinstr#get_opcode
-        ~condloc
-        ~testloc in
+      get_default_conditional_expr () in
 
   let _ =
     if testsupport#requested_arm_conditional_expr then
@@ -381,6 +344,18 @@ let make_tests
   | _ -> (frozenVars, None)
 
 
+(* Returns the CHIF code for a conditional branch instruction that
+   incorporates the full condition as part of the instruction (i.e. no
+   dependency on a separate test instruction), such as CBZ or CBNZ.
+
+   The CHIF code consists of a tuple of two sequences of CHIF commands.
+   The first sequence is the CHIF for the then test, the second sequence
+   is the CHIF for the else test.
+
+   If the condition cannot be converted to CHIF SKIP commands are
+   returned, that is, the conditional branch is effectively turned into
+   a nondeterminstic branch.
+ *)
 let make_local_tests
       (condinstr: arm_assembly_instruction_int)
       (condloc: location_int): (cmd_t list * cmd_t list) =
@@ -427,6 +402,17 @@ let make_local_tests
     boolxpr_r
 
 
+(* Returns the control-flow graph nodes and edges of a conditional branch
+   instruction that incorporates the full condition as part of the instruction
+   (i.e., no dependency on a separate test instruction), such as CBZ
+   (CompareBranchZero) or CBNZ)
+
+   Two cfg nodes are created: a 'then' node with the then-test and an 'else'
+   node with the else-test. Four cfg edges are created: (1) from block label
+   to thennode, (2) from block label to elsenode, (3) from thennode to the
+   cfg target jump address, and (4) from elsenode to the cfg fall-through
+   address.
+ *)
 let make_local_condition
       (condinstr: arm_assembly_instruction_int)
       (condloc: location_int)
@@ -452,6 +438,29 @@ let make_local_condition
   ([(thentestlabel, thennode); (elsetestlabel, elsenode)], thenedges @ elseedges)
 
 
+(* Returns the control-flow graph nodes and edges of a conditional branch or an
+   IfThen instruction that is handled with full control flow rather than with an
+   aggregate. It applies to conditional branches in which the test is performed
+   by a separate instruction (the test instruction) and the branch condition
+   is determined by the combination of the test instruction and the condition
+   code that is part of the branch instruction (or IfThen).
+
+   If a conditional predicate for the branch can be synthesized and converted into
+   CHIF, a 'then node' with the then-test and an 'else node' with the else-test
+   are created. In both nodes the temporary variables that were created to carry
+   the frozen values are abstracted to avoid unnecessary propagation of variables
+   that will never be used again. Four edges are created: (1) from block-label
+   to thenblock, (2) from thenblock to the cfg target jump address, (3) from
+   block-label to elseblock, and (4) from elseblock to the cfg fall-through
+   instruction.
+
+   If a conditional predicate for the branch cannot be constructed the control flow
+   components created represent a non-deterministic branch. One node is
+   constructed, to abstract the temporary variables created by the attempt to
+   create a condition. Three edges are created: (1) from block-label to the new
+   node, (2) from the new node to the cfg target jump address, and (3) from the new
+   node to the cfg fall-through instruction.
+*)
 let make_condition
       ?(thencode: cmd_t list = [])
       ?(elsecode: cmd_t list = [])
@@ -560,43 +569,41 @@ let translate_arm_instruction
   let pcassign = floc#get_assign_commands pcv (XConst (IntConst iaddr8)) in
   let default newcmds =
     ([], [], cmds @ frozenAsserts @ (invop :: newcmds) @ [bwdinvop] @ pcassign) in
+
   let make_conditional_commands (_c: arm_opcode_cc_t) (cmds: cmd_t list) =
     if instr#is_condition_covered then
       default cmds
-    else if finfo#has_associated_cc_setter ctxtiaddr then
-      let testiaddr = finfo#get_associated_cc_setter ctxtiaddr in
-      let testloc = ctxt_string_to_location faddr testiaddr in
-      let testaddr = (ctxt_string_to_location faddr testiaddr)#i in
-      let testinstr =
-        fail_tvalue
-          (trerror_record
-             (LBLOCK [STR "Internal error in make_instr_local_tests"]))
-          (get_arm_assembly_instruction testaddr) in
-
-      let (_, tests) =
-        make_instr_local_tests ~condloc:loc ~testloc ~condinstr:instr ~testinstr in
-      match tests with
-      | Some (thentest, elsetest) ->
-         if has_false_condition_context ctxtiaddr then
-           default elsetest
-         else if has_true_condition_context ctxtiaddr then
-           default (thentest @ cmds)
-         else
-           default [BRANCH [LF.mkCode (thentest @ cmds); LF.mkCode elsetest]]
+    else
+      match get_associated_test_instr finfo ctxtiaddr with
+      | Some (testloc, testinstr) ->
+         let (_, tests) =
+           make_instr_local_tests
+             ~condloc:loc ~testloc ~condinstr:instr ~testinstr in
+         (match tests with
+          | Some (thentest, elsetest) ->
+             if has_false_condition_context ctxtiaddr then
+               default elsetest
+             else if has_true_condition_context ctxtiaddr then
+               default (thentest @ cmds)
+             else
+               default [BRANCH [LF.mkCode (thentest @ cmds); LF.mkCode elsetest]]
+          | _ ->
+             (* make non-deterministic branch, unless covered by True/False
+                context*)
+             if has_false_condition_context ctxtiaddr then
+               default []
+             else if has_true_condition_context ctxtiaddr then
+               default cmds
+             else
+               default [BRANCH [LF.mkCode cmds; LF.mkCode [SKIP]]])
       | _ ->
          if has_false_condition_context ctxtiaddr then
            default []
          else if has_true_condition_context ctxtiaddr then
            default cmds
          else
-           default [BRANCH [LF.mkCode cmds; LF.mkCode [SKIP]]]
-    else
-      if has_false_condition_context ctxtiaddr then
-        default []
-      else if has_true_condition_context ctxtiaddr then
-        default cmds
-      else
-        default [BRANCH [LF.mkCode cmds; LF.mkCode [SKIP]]] in
+           default [BRANCH [LF.mkCode cmds; LF.mkCode [SKIP]]] in
+
   let get_register_vars (ops: arm_operand_int list) =
     List.fold_left (fun acc op ->
         if op#is_register || op#is_extension_register then
@@ -678,6 +685,7 @@ let translate_arm_instruction
     match instr#is_in_aggregate with
     | Some dw -> (get_aggregate dw)#is_jumptable
     | _ -> false in
+
   let is_part_of_pseudo_instr () =
     match instr#is_in_aggregate with
     | Some dw ->
@@ -764,15 +772,8 @@ let translate_arm_instruction
        else
          "?" in
      let defcmds =
-       if finfo#has_associated_cc_setter ctxtiaddr then
-         let testiaddr = finfo#get_associated_cc_setter ctxtiaddr in
-         let testloc = ctxt_string_to_location faddr testiaddr in
-         let testaddr = (ctxt_string_to_location faddr testiaddr)#i in
-         let testinstr =
-           fail_tvalue
-             (trerror_record
-                (LBLOCK [STR "Internal error in make_instr_local_tests"]))
-             (get_arm_assembly_instruction testaddr) in
+       match get_associated_test_instr finfo ctxtiaddr with
+       | Some (testloc, testinstr) ->
          let (_, optxpr, opsused) =
            make_conditional_predicate
              ~condinstr:instr
@@ -784,7 +785,7 @@ let translate_arm_instruction
            | Some xpr -> get_use_high_vars [xpr]
            | _ -> [] in
          floc#get_vardef_commands ~use ~usehigh ctxtiaddr
-       else
+       | _ ->
          [] in
      let elseaddr = codepc#get_false_branch_successor in
      let cmds = cmds @ [invop] @ defcmds @ [bwdinvop] in
@@ -1096,6 +1097,11 @@ let translate_arm_instruction
    *     APSR.Z = IsZeroBit(result);
    *     APSR.C = carry;
    * ------------------------------------------------------------------------ *)
+  | BitwiseNot _ when Option.is_some instr#is_in_aggregate ->
+     (* may be part of a ternary assignment.
+        TODO: add code for the case where MVN is the anchor instruction.*)
+     default []
+
   | BitwiseNot (_, c, rd, rm, _) when rm#is_immediate ->
      let vrd = floc#env#mk_register_variable rd#to_register in
      let lhs_r = TR.tmap fst (rd#to_lhs floc) in
@@ -1325,90 +1331,76 @@ let translate_arm_instruction
      default []
 
   | IfThen _ when instr#is_aggregate_anchor ->
-     if finfo#has_associated_cc_setter ctxtiaddr then
-       let testiaddr = finfo#get_associated_cc_setter ctxtiaddr in
-       let testloc = ctxt_string_to_location faddr testiaddr in
-       let testaddr = testloc#i in
-       let testinstr =
-         fail_tvalue
-           (trerror_record
-              (LBLOCK [STR "Translate IfThenin: "; STR ctxtiaddr]))
-           (get_arm_assembly_instruction testaddr) in
-       let itagg = get_aggregate loc#i in
-       let its = itagg#it_sequence in
-       (match its#kind with
-        | ITPredicateAssignment (inverse, dstop) ->
-           let (_, optpredicate, _opsused) =
-             make_conditional_predicate
-               ~condinstr:instr
-               ~testinstr:testinstr
-               ~condloc:loc
-               ~testloc:testloc in
-           let cmds =
-             match optpredicate with
-             | Some p ->
-                let p = if inverse then XOp (XLNot, [p]) else p in
-                let vrd = floc#env#mk_register_variable dstop#to_register in
-                let lhs_r = TR.tmap fst (dstop#to_lhs floc) in
-                let usevars = vars_in_expr_list [p] in
-                let usehigh = get_use_high_vars [p] in
-                let cmds = floc#get_assign_commands_r lhs_r (Ok p) in
-                let defcmds =
-                  floc#get_vardef_commands
-                    ~defs:[vrd]
-                    ~use:usevars
-                    ~usehigh:usehigh
-                    ~flagdefs:flagdefs
-                    ctxtiaddr in
-                defcmds @ cmds
-             | _ ->
-                begin
-                  log_error_result
-                    ~tag:"IfThen"
-                    __FILE__ __LINE__
-                    ["Predicate assignment without predicate"];
-                  []
-                end in
-           default cmds)
-     else
-       begin
-         log_error_result
-           ~tag:"IfThen"
-           __FILE__ __LINE__
-           ["Aggregate IfThen without associated cc setter"];
-         default []
-       end
+     (match get_associated_test_instr finfo ctxtiaddr with
+      | Some (testloc, testinstr) ->
+         let itagg = get_aggregate loc#i in
+         let its = itagg#it_sequence in
+         (match its#kind with
+          | ITPredicateAssignment (inverse, dstop) ->
+             let (_, optpredicate, _opsused) =
+               make_conditional_predicate
+                 ~condinstr:instr
+                 ~testinstr:testinstr
+                 ~condloc:loc
+                 ~testloc:testloc in
+             let cmds =
+               match optpredicate with
+               | Some p ->
+                  let p = if inverse then XOp (XLNot, [p]) else p in
+                  let vrd = floc#env#mk_register_variable dstop#to_register in
+                  let lhs_r = TR.tmap fst (dstop#to_lhs floc) in
+                  let usevars = vars_in_expr_list [p] in
+                  let usehigh = get_use_high_vars [p] in
+                  let cmds = floc#get_assign_commands_r lhs_r (Ok p) in
+                  let defcmds =
+                    floc#get_vardef_commands
+                      ~defs:[vrd]
+                      ~use:usevars
+                      ~usehigh:usehigh
+                      ~flagdefs:flagdefs
+                      ctxtiaddr in
+                  defcmds @ cmds
+               | _ ->
+                  begin
+                    log_error_result
+                      ~tag:"IfThen"
+                      __FILE__ __LINE__
+                      ["Predicate assignment without predicate"];
+                    []
+                  end in
+             default cmds)
+      | _ ->
+         begin
+           log_error_result
+             ~tag:"IfThen"
+             __FILE__ __LINE__
+             ["Aggregate IfThen without associated cc setter"];
+           default []
+         end)
 
   | IfThen _ when instr#is_block_condition ->
      let thenaddr = codepc#get_true_branch_successor in
      let elseaddr = codepc#get_false_branch_successor in
      let cmds = cmds @ [invop] in
      let transaction = package_transaction finfo blocklabel cmds in
-     if finfo#has_associated_cc_setter ctxtiaddr then
-       let testiaddr = finfo#get_associated_cc_setter ctxtiaddr in
-       let testloc = ctxt_string_to_location faddr testiaddr in
-       let testaddr = (ctxt_string_to_location faddr testiaddr)#i in
-       let testinstr =
-         fail_tvalue
-           (trerror_record
-              (LBLOCK [STR "Internal error in make_instr_local_tests"]))
-           (get_arm_assembly_instruction testaddr) in
-       let (nodes, edges) =
-         make_condition
-           ~condinstr:instr
-           ~testinstr:testinstr
-           ~condloc:loc
-           ~testloc
-           ~blocklabel
-           ~thenaddr
-           ~elseaddr () in
-       ((blocklabel, [transaction]) :: nodes, edges, [])
-     else
-       let thenlabel = make_code_label thenaddr in
-       let elselabel = make_code_label elseaddr in
-       let nodes = [(blocklabel, [transaction])] in
-       let edges = [(blocklabel, thenlabel); (blocklabel, elselabel)] in
-       (nodes, edges, [])
+     (match get_associated_test_instr finfo ctxtiaddr with
+      | Some (testloc, testinstr) ->
+         let (nodes, edges) =
+           make_condition
+             ~condinstr:instr
+             ~testinstr:testinstr
+             ~condloc:loc
+             ~testloc
+             ~blocklabel
+             ~thenaddr
+             ~elseaddr () in
+         ((blocklabel, [transaction]) :: nodes, edges, [])
+      | _ ->
+         let thenlabel = make_code_label thenaddr in
+         let elselabel = make_code_label elseaddr in
+         let nodes = [(blocklabel, [transaction])] in
+         let edges = [(blocklabel, thenlabel); (blocklabel, elselabel)] in
+         (nodes, edges, []))
 
   (* ---------------------------------------- LoadMultipleDecrementAfter --
    * Loads multiple registers from consecutive memory locations using an
@@ -1551,7 +1543,7 @@ let translate_arm_instruction
            let memrhs_r = memop#to_expr floc in
            let memuse = TR.tfold_default (fun memvar -> [memvar]) [] memvar_r in
            let memusehigh = get_use_high_vars_r [memrhs_r] in
-           let cmds1 = floc#get_assign_commands_r memvar_r memrhs_r in
+           let cmds1 = floc#get_assign_commands_r (Ok regvar) memrhs_r in
            let defcmds1 =
              floc#get_vardef_commands
                ~defs:[regvar]
@@ -2040,52 +2032,96 @@ let translate_arm_instruction
    *    APSR.Z = IsZeroBit(result);
    * ------------------------------------------------------------------------ *)
   | Move _ when instr#is_aggregate_anchor ->
-     let floc = get_floc loc in
-     if finfo#has_associated_cc_setter ctxtiaddr then
-       let testiaddr = finfo#get_associated_cc_setter ctxtiaddr in
-       let testloc = ctxt_string_to_location faddr testiaddr in
-       let testaddr = testloc#i in
-       let testinstr =
-         fail_tvalue
-           (trerror_record
-              (LBLOCK [STR "Translate MOV predicate assignment"; STR ctxtiaddr]))
-           (get_arm_assembly_instruction testaddr) in
-       let movagg = get_aggregate loc#i in
-       (match movagg#kind with
-        | ARMPredicateAssignment (inverse, dstop) ->
-           let (_, optpredicate, _) =
-             make_conditional_predicate
-               ~condinstr:instr
-               ~testinstr:testinstr
-               ~condloc:loc
-               ~testloc:testloc in
-           let cmds =
-             match optpredicate with
-             | Some p ->
-                let p = if inverse then XOp (XLNot, [p]) else p in
-                let lhs_r = TR.tmap fst (dstop#to_lhs floc) in
-                let cmds = floc#get_assign_commands_r lhs_r (Ok p) in
-                let vrd = floc#env#mk_register_variable dstop#to_register in
-                let usevars = vars_in_expr_list [p] in
-                let usehigh = get_use_high_vars [p] in
-                let defcmds =
-                  floc#get_vardef_commands
-                    ~defs:[vrd]
-                    ~use:usevars
-                    ~usehigh
-                    ~flagdefs
-                    ctxtiaddr in
-                defcmds @ cmds
-             | _ ->
-                [] in
-           default cmds
-        | _ -> default [])
-     else
-       let _ =
-         chlog#add
-           "predicate assignment aggregate without predicate"
-           (LBLOCK [loc#toPretty; STR ": "; instr#toPretty]) in
-       default []
+     (match get_associated_test_instr finfo ctxtiaddr with
+      | Some (testloc, testinstr) ->
+         let movagg = get_aggregate loc#i in
+         (match movagg#kind with
+          | ARMPredicateAssignment (inverse, dstop) ->
+             let (_, optpredicate, _) =
+               make_conditional_predicate
+                 ~condinstr:instr ~testinstr ~condloc:loc ~testloc in
+             let cmds =
+               let lhs_r = TR.tmap fst (dstop#to_lhs floc) in
+               let vrd = floc#env#mk_register_variable dstop#to_register in
+               match optpredicate with
+               | Some p ->
+                  let p = if inverse then XOp (XLNot, [p]) else p in
+                  let cmds = floc#get_assign_commands_r lhs_r (Ok p) in
+                  let usevars = vars_in_expr_list [p] in
+                  let usehigh = get_use_high_vars [p] in
+                  let defcmds =
+                    floc#get_vardef_commands
+                      ~defs:[vrd]
+                      ~use:usevars
+                      ~usehigh
+                      ~flagdefs
+                      ctxtiaddr in
+                  defcmds @ cmds
+               | _ ->
+                  let _ =
+                    chlog#add
+                      "predicate assignment:no predicate"
+                      (LBLOCK [floc#l#toPretty]) in
+                  let cmds = floc#get_abstract_commands_r lhs_r in
+                  let defcmds =
+                    floc#get_vardef_commands ~defs:[vrd] ~flagdefs ctxtiaddr in
+                  defcmds @ cmds in
+             default cmds
+          | ARMTernaryAssignment (dstop, n1, n2) ->
+             let (_, optpredicate, _) =
+               make_conditional_predicate
+                 ~condinstr:instr ~testinstr ~condloc:loc ~testloc in
+             let (_, tests) =
+               make_instr_local_tests
+                 ~condloc:loc ~testloc ~condinstr:instr ~testinstr in
+             let cmds =
+               let lhs_r = TR.tmap fst (dstop#to_lhs floc) in
+               let vrd = floc#env#mk_register_variable dstop#to_register in
+               match optpredicate with
+               | Some p ->
+                  let x1 = XConst (IntConst n1) in
+                  let x2 = XConst (IntConst n2) in
+                  let cmd1 = floc#get_assign_commands_r lhs_r (Ok x1) in
+                  let cmd2 = floc#get_assign_commands_r lhs_r (Ok x2) in
+                  let usevars = vars_in_expr_list [p] in
+                  let usehigh = get_use_high_vars [p] in
+                  let defcmds =
+                    floc#get_vardef_commands
+                      ~defs:[vrd]
+                      ~use:usevars
+                      ~usehigh
+                      ~flagdefs
+                      ctxtiaddr in
+                  let brcmd =
+                    match tests with
+                    | Some (thentest, elsetest) ->
+                       BRANCH [LF.mkCode (thentest @ cmd1);
+                               LF.mkCode (elsetest @ cmd2)]
+                    | _ ->
+                       BRANCH [LF.mkCode cmd1; LF.mkCode cmd2] in
+                  defcmds @ [brcmd]
+               | _ ->
+                  let _ =
+                    chlog#add
+                      "ternary assignment:no predicate"
+                      (LBLOCK [floc#l#toPretty]) in
+                  let cmds = floc#get_abstract_commands_r lhs_r in
+                  let defcmds =
+                    floc#get_vardef_commands ~defs:[vrd] ~flagdefs ctxtiaddr in
+                  defcmds @ cmds in
+             default cmds
+
+          | _ ->
+             (* should not be reachable *)
+             raise
+               (BCH_failure
+                  (LBLOCK [floc#l#toPretty; STR ": Unknown MOV aggregate kind"])))
+      | _ ->
+         let _ =
+           chlog#add
+             "predicate assignment aggregate without predicate"
+             (LBLOCK [loc#toPretty; STR ": "; instr#toPretty]) in
+         default [])
 
   | Move _ when Option.is_some instr#is_in_aggregate ->
      default []
@@ -2376,25 +2412,21 @@ let translate_arm_instruction
 
      let ccdefcmds (): cmd_t list =
        if is_cond_conditional c && finfo#has_associated_cc_setter ctxtiaddr then
-         let testiaddr = finfo#get_associated_cc_setter ctxtiaddr in
-         let testloc = ctxt_string_to_location faddr testiaddr in
-         let testaddr = (ctxt_string_to_location faddr testiaddr)#i in
-         let testinstr =
-           fail_tvalue
-             (trerror_record
-                (LBLOCK [STR "Internal error in make tests"]))
-             (get_arm_assembly_instruction testaddr) in
-         let (_, optxpr, opsused) =
-           make_conditional_predicate
-             ~condinstr: instr
-             ~testinstr: testinstr
-             ~condloc:loc
-             ~testloc in
-         let use = get_register_vars opsused in
-         let usehigh = match optxpr with
-           | Some xpr -> get_use_high_vars [xpr]
-           | _ -> [] in
-         floc#get_vardef_commands ~use ~usehigh ctxtiaddr
+         match get_associated_test_instr finfo ctxtiaddr with
+         | Some (testloc, testinstr) ->
+            let (_, optxpr, opsused) =
+              make_conditional_predicate
+                ~condinstr: instr
+                ~testinstr: testinstr
+                ~condloc:loc
+                ~testloc in
+            let use = get_register_vars opsused in
+            let usehigh = match optxpr with
+              | Some xpr -> get_use_high_vars [xpr]
+              | _ -> [] in
+            floc#get_vardef_commands ~use ~usehigh ctxtiaddr
+         | _ ->
+            []
        else
          [] in
 
@@ -2425,39 +2457,32 @@ let translate_arm_instruction
        let transaction = package_transaction finfo blocklabel cmds in
 
        (* create the branches according to the condition *)
-       if finfo#has_associated_cc_setter ctxtiaddr then
-         let testiaddr = finfo#get_associated_cc_setter ctxtiaddr in
-         let testloc = ctxt_string_to_location faddr testiaddr in
-         let testaddr = (ctxt_string_to_location faddr testiaddr)#i in
-         let testinstr =
-           fail_tvalue
-             (trerror_record
-                (LBLOCK [STR "Internal error in conditional Pop"]))
-             (get_arm_assembly_instruction testaddr) in
-         let (nodes, edges) =
-           make_condition
-             ~thencode:(popcmds ())
-             ~condinstr:instr
-             ~testinstr:testinstr
-             ~condloc:loc
-             ~testloc
-             ~blocklabel
-             ~thenaddr
-             ~elseaddr () in
-         ((blocklabel, [transaction]) :: nodes, edges, [])
-       else
-         let (poplabel, popnode) =
-           let label = make_code_label ~modifier:"pop" thenaddr in
-           let transaction = TRANSACTION (label, LF.mkCode (popcmds ()), None) in
-           (label, [transaction]) in
-         let thenlabel = make_code_label thenaddr in
-         let elselabel = make_code_label elseaddr in
-         let nodes = [(blocklabel, [transaction]); (poplabel, popnode)] in
-         let edges = [
-             (blocklabel, poplabel);
-             (poplabel, thenlabel);
-             (blocklabel, elselabel)] in
-         (nodes, edges, [])
+       (match get_associated_test_instr finfo ctxtiaddr with
+        | Some (testloc, testinstr) ->
+           let (nodes, edges) =
+             make_condition
+               ~thencode:(popcmds ())
+               ~condinstr:instr
+               ~testinstr:testinstr
+               ~condloc:loc
+               ~testloc
+               ~blocklabel
+               ~thenaddr
+               ~elseaddr () in
+           ((blocklabel, [transaction]) :: nodes, edges, [])
+        | _ ->
+           let (poplabel, popnode) =
+             let label = make_code_label ~modifier:"pop" thenaddr in
+             let transaction = TRANSACTION (label, LF.mkCode (popcmds ()), None) in
+             (label, [transaction]) in
+           let thenlabel = make_code_label thenaddr in
+           let elselabel = make_code_label elseaddr in
+           let nodes = [(blocklabel, [transaction]); (poplabel, popnode)] in
+           let edges = [
+               (blocklabel, poplabel);
+               (poplabel, thenlabel);
+               (blocklabel, elselabel)] in
+           (nodes, edges, []))
 
      else
        (* regular, unconditional Pop, or conditional pop without pc *)
diff --git a/CodeHawk/CHT/tchlib/tCHTest.mli b/CodeHawk/CHT/tchlib/tCHTest.mli
index 0ef0c5d3..564a6468 100644
--- a/CodeHawk/CHT/tchlib/tCHTest.mli
+++ b/CodeHawk/CHT/tchlib/tCHTest.mli
@@ -51,7 +51,7 @@ open TCHTestApi
 val return: 'a -> (unit -> 'a)
 
 
-(** {6 Assertion-based tests} *)
+(** {1 Assertion-based tests} *)
 
 
 (** [make_assert_test ~title:t set_up f tear_down] constructs a test running the
@@ -70,7 +70,7 @@ val make_assert_test:
 val make_simple_test: ?title:string -> (unit -> unit) -> testcase_t
   
   
-(** {6 Generator-based tests} *)
+(** {1 Generator-based tests} *)
 
 (** [make_random_test ~title:t ~nb_runs:nb ~nb_tries:nt ~classifier:c ~reducer:red
     ~random_src:rnd gen f spec] constructs a random test. [f] is the function to

From bff8143d9f52540f582e3ca7ecbf434421adc014 Mon Sep 17 00:00:00 2001
From: Henny Sipma <hennysipma@mac.com>
Date: Tue, 8 Jul 2025 09:10:40 -0700
Subject: [PATCH 16/16] CHT: fix unit test output

---
 .../txbchlibarm32/bCHDisassembleThumbInstructionTest.ml       | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHDisassembleThumbInstructionTest.ml b/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHDisassembleThumbInstructionTest.ml
index bd0910f4..edcd2d62 100644
--- a/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHDisassembleThumbInstructionTest.ml
+++ b/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHDisassembleThumbInstructionTest.ml
@@ -5,7 +5,7 @@
    ------------------------------------------------------------------------------
    The MIT License (MIT)
 
-   Copyright (c) 2022-2024  Aarno Labs LLC
+   Copyright (c) 2022-2025  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
@@ -70,7 +70,7 @@ let thumb_2_basic () =
       ("ADDS-I-T2",  "0132", "ADDS           R2, R2, #1");
       ("ADDS-R-T2",  "7c44", "ADDS           R4, R4, PC");
       ("ADD-SPI-T2", "0ab0", "ADD            SP, SP, #0x28");
-      ("AND-R-T1",   "1e40", "AND            R6, R6, R3");
+      ("AND-R-T1",   "1e40", "ANDS           R6, R6, R3");
       ("ASRS-I-T1",  "4910", "ASRS           R1, R1, #1");
       ("BKPT",       "fbbe", "BKPT           #0xfb");
       ("BLX-R-T1",   "9847", "BLX            R3");