C library: add imaxabs

This is another variant of absolute-value functions.

Author: tautschnig

regression/cbmc-library/imaxabs-01/main.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <inttypes.h>
+#include <stdlib.h>
+
+int main()
+{
+  assert(imaxabs(INTMAX_MIN + 1) == INTMAX_MAX);
+  return 0;
+}

regression/cbmc-library/imaxabs-01/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check --signed-overflow-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/ansi-c/c_typecheck_expr.cpp

@@ -2872,12 +2872,13 @@ exprt c_typecheck_baset::do_special_functions(
 
     return std::move(infl_expr);
   }
-  else if(identifier==CPROVER_PREFIX "abs" ||
-          identifier==CPROVER_PREFIX "labs" ||
-          identifier==CPROVER_PREFIX "llabs" ||
-          identifier==CPROVER_PREFIX "fabs" ||
-          identifier==CPROVER_PREFIX "fabsf" ||
-          identifier==CPROVER_PREFIX "fabsl")
+  else if(
+    identifier == CPROVER_PREFIX "abs" || identifier == CPROVER_PREFIX "labs" ||
+    identifier == CPROVER_PREFIX "llabs" ||
+    identifier == CPROVER_PREFIX "imaxabs" ||
+    identifier == CPROVER_PREFIX "fabs" ||
+    identifier == CPROVER_PREFIX "fabsf" ||
+    identifier == CPROVER_PREFIX "fabsl")
   {
     if(expr.arguments().size()!=1)
     {

src/ansi-c/library/stdlib.c

@@ -25,6 +25,22 @@ long long int llabs(long long int i)
   return __CPROVER_llabs(i);
 }
 
+/* FUNCTION: imaxabs */
+
+#ifndef __CPROVER_INTTYPES_H_INCLUDED
+#  include <inttypes.h>
+#  define __CPROVER_INTTYPES_H_INCLUDED
+#endif
+
+#undef imaxabs
+
+intmax_t __CPROVER_imaxabs(intmax_t);
+
+intmax_t imaxabs(intmax_t i)
+{
+  return __CPROVER_imaxabs(i);
+}
+
 /* FUNCTION: __builtin_abs */
 
 int __builtin_abs(int i)