Undo changes to math.c

Author: hannes-steffenhagen-diffblue

src/ansi-c/library/math.c

@@ -2303,28 +2303,32 @@ long double copysignl(long double x, long double y)
 
 _Bool __builtin_sadd_overflow(int a, int b, int *res)
 {
-  return __builtin_add_overflow(a, b, res);
+  *res = a + b;
+  return __CPROVER_overflow_plus(a, b);
 }
 
 /* FUNCTION: __builtin_saddl_overflow */
 
 _Bool __builtin_saddl_overflow(long a, long b, long *res)
 {
-  return __builtin_add_overflow(a, b, res);
+  *res = a + b;
+  return __CPROVER_overflow_plus(a, b);
 }
 
 /* FUNCTION: __builtin_saddll_overflow */
 
 _Bool __builtin_saddll_overflow(long long a, long long b, long long *res)
 {
-  return __builtin_add_overflow(a, b, res);
+  *res = a + b;
+  return __CPROVER_overflow_plus(a, b);
 }
 
 /* FUNCTION: __builtin_uadd_overflow */
 
 _Bool __builtin_uadd_overflow(unsigned a, unsigned b, unsigned *res)
 {
-  return __builtin_add_overflow(a, b, res);
+  *res = a + b;
+  return __CPROVER_overflow_plus(a, b);
 }
 
 /* FUNCTION: __builtin_uaddl_overflow */
@@ -2334,7 +2338,8 @@ _Bool __builtin_uaddl_overflow(
   unsigned long b,
   unsigned long *res)
 {
-  return __builtin_add_overflow(a, b, res);
+  *res = a + b;
+  return __CPROVER_overflow_plus(a, b);
 }
 
 /* FUNCTION: __builtin_uaddll_overflow */
@@ -2344,35 +2349,40 @@ _Bool __builtin_uaddll_overflow(
   unsigned long long b,
   unsigned long long *res)
 {
-  return __builtin_add_overflow(a, b, res);
+  *res = a + b;
+  return __CPROVER_overflow_plus(a, b);
 }
 
 /* FUNCTION: __builtin_ssub_overflow */
 
 _Bool __builtin_ssub_overflow(int a, int b, int *res)
 {
-  return __builtin_sub_overflow(a, b, res);
+  *res = a - b;
+  return __CPROVER_overflow_minus(a, b);
 }
 
 /* FUNCTION: __builtin_ssubl_overflow */
 
 _Bool __builtin_ssubl_overflow(long a, long b, long *res)
 {
-  return __builtin_sub_overflow(a, b, res);
+  *res = a - b;
+  return __CPROVER_overflow_minus(a, b);
 }
 
 /* FUNCTION: __builtin_ssubll_overflow */
 
 _Bool __builtin_ssubll_overflow(long long a, long long b, long long *res)
 {
-  return __builtin_sub_overflow(a, b, res);
+  *res = a - b;
+  return __CPROVER_overflow_minus(a, b);
 }
 
 /* FUNCTION: __builtin_usub_overflow */
 
 _Bool __builtin_usub_overflow(unsigned a, unsigned b, unsigned *res)
 {
-  return __builtin_sub_overflow(a, b, res);
+  *res = a - b;
+  return __CPROVER_overflow_minus(a, b);
 }
 
 /* FUNCTION: __builtin_usubl_overflow */
@@ -2382,7 +2392,8 @@ _Bool __builtin_usubl_overflow(
   unsigned long b,
   unsigned long *res)
 {
-  return __builtin_sub_overflow(a, b, res);
+  *res = a - b;
+  return __CPROVER_overflow_minus(a, b);
 }
 
 /* FUNCTION: __builtin_usubll_overflow */
@@ -2392,35 +2403,40 @@ _Bool __builtin_usubll_overflow(
   unsigned long long b,
   unsigned long long *res)
 {
-  return __builtin_sub_overflow(a, b, res);
+  *res = a - b;
+  return __CPROVER_overflow_minus(a, b);
 }
 
 /* FUNCTION: __builtin_smul_overflow */
 
 _Bool __builtin_smul_overflow(int a, int b, int *res)
 {
-  return __builtin_mul_overflow(a, b, res);
+  *res = a * b;
+  return __CPROVER_overflow_mult(a, b);
 }
 
 /* FUNCTION: __builtin_smull_overflow */
 
 _Bool __builtin_smull_overflow(long a, long b, long *res)
 {
-  return __builtin_mul_overflow(a, b, res);
+  *res = a * b;
+  return __CPROVER_overflow_mult(a, b);
 }
 
 /* FUNCTION: __builtin_smulll_overflow */
 
 _Bool __builtin_smulll_overflow(long long a, long long b, long long *res)
 {
-  return __builtin_mul_overflow(a, b, res);
+  *res = a * b;
+  return __CPROVER_overflow_mult(a, b);
 }
 
 /* FUNCTION: __builtin_umul_overflow */
 
 _Bool __builtin_umul_overflow(unsigned a, unsigned b, unsigned *res)
 {
-  return __builtin_mul_overflow(a, b, res);
+  *res = a * b;
+  return __CPROVER_overflow_mult(a, b);
 }
 
 /* FUNCTION: __builtin_umull_overflow */
@@ -2430,7 +2446,8 @@ _Bool __builtin_umull_overflow(
   unsigned long b,
   unsigned long *res)
 {
-  return __builtin_mul_overflow(a, b, res);
+  *res = a * b;
+  return __CPROVER_overflow_mult(a, b);
 }
 
 /* FUNCTION: __builtin_umulll_overflow */
@@ -2440,5 +2457,6 @@ _Bool __builtin_umulll_overflow(
   unsigned long long b,
   unsigned long long *res)
 {
-  return __builtin_mul_overflow(a, b, res);
+  *res = a * b;
+  return __CPROVER_overflow_mult(a, b);
 }