From 05e958a21d536b8066615457decc771d3e7cc723 Mon Sep 17 00:00:00 2001
From: Henny Sipma <hennysipma@mac.com>
Date: Tue, 16 Jun 2026 22:47:00 -0700
Subject: [PATCH] CHC: update PO generation for Div and Mod

---
 .../CHC/cchanalyze/cCHPOCheckIntOverflow.ml   |  8 +++++++
 .../CHC/cchpre/cCHPrimaryProofObligations.ml  | 23 ++++++++++---------
 2 files changed, 20 insertions(+), 11 deletions(-)

diff --git a/CodeHawk/CHC/cchanalyze/cCHPOCheckIntOverflow.ml b/CodeHawk/CHC/cchanalyze/cCHPOCheckIntOverflow.ml
index d58c87d5..de1d2fa6 100644
--- a/CodeHawk/CHC/cchanalyze/cCHPOCheckIntOverflow.ml
+++ b/CodeHawk/CHC/cchanalyze/cCHPOCheckIntOverflow.ml
@@ -1214,6 +1214,14 @@ object
 end
 
 
+  (* C99 $6.5.5:
+     When integers are divided, the result of the / operator is the algebraic
+     quotient with any fractional part discarded.105) If the quotient a/b is
+     representable, the expression (a/b)*b + a%b shall equal a;
+
+     C11 $6.5.5 adds the following:
+     otherwise, the behavior of both a/b and a%b is undefined.*)
+
 let check_int_overflow
       ?(unsigned=false)
       (poq:po_query_int)
diff --git a/CodeHawk/CHC/cchpre/cCHPrimaryProofObligations.ml b/CodeHawk/CHC/cchpre/cCHPrimaryProofObligations.ml
index ae2b213d..f06b9b03 100644
--- a/CodeHawk/CHC/cchpre/cCHPrimaryProofObligations.ml
+++ b/CodeHawk/CHC/cchpre/cCHPrimaryProofObligations.ml
@@ -315,22 +315,25 @@ and create_po_binop
             ^ " " ^ (p2s (current_loc_to_pretty loc))]
     end
 
-  | Div ->
+  (* C99 $6.5.5:
+     When integers are divided, the result of the / operator is the algebraic
+     quotient with any fractional part discarded.105) If the quotient a/b is
+     representable, the expression (a/b)*b + a%b shall equal a;
+
+     C11 $6.5.5 adds the following:
+     otherwise, the behavior of both a/b and a%b is undefined.*)
+  | Div | Mod ->
      begin
        match fenv#get_type_unrolled t with
        | TInt (ik, _) when is_signed_type ik ->
 	  begin
-	    add (PIntUnderflow (binop, e1, e2, ik));
 	    add (PIntOverflow (binop, e1, e2, ik));
 	    addxop (PNotZero e2) 2
 	  end
-       | TInt (ik,_) ->
-	  begin
-	    add (PUIntUnderflow (binop, e1, e2, ik));
-	    add (PUIntOverflow (binop, e1, e2, ik));
-	    addxop (PNotZero e2) 2
-	  end
-       | TFloat _ -> add (PNotZero e2)
+       | TInt _ ->
+          addxop (PNotZero e2) 2
+       | TFloat _ ->
+          add (PNotZero e2)
        | _ ->
          log_error_result
            ~tag:"create_po_binop"
@@ -344,8 +347,6 @@ and create_po_binop
             ^ " " ^ (p2s (current_loc_to_pretty loc))]
      end
 
-  | Mod -> addxop (PNotZero e2) 2
-
   | PlusPI | IndexPI | MinusPI ->
      let tgttyp =
        match fenv#get_type_unrolled t with