Merge pull request #7825 from diffblue/abs-preconditions

preconditions for abs, labs, llabs, imaxabs

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

@@ -1,3 +1,4 @@
+#include <limits.h>
 #include <math.h>
 #include <stdlib.h>
 
@@ -17,7 +18,8 @@ int main()
   assert(fabs(-1.0) == 1);
 
   iabs = (my_i < 0) ? -my_i : my_i;
-  assert(abs(my_i) == iabs);
+  if(my_i != INT_MIN)
+    assert(abs(my_i) == iabs);
 
   __CPROVER_assume(!isnan(my_d));
 

src/ansi-c/library/stdlib.c

@@ -1,27 +1,53 @@
 /* FUNCTION: abs */
 
+#ifndef __CPROVER_LIMITS_H_INCLUDED
+#  include <limits.h>
+#  define __CPROVER_LIMITS_H_INCLUDED
+#endif
+
 #undef abs
 
 int abs(int i)
 {
+  // C99 Section 7.20.6.1:
+  // "If the result cannot be represented, the behavior is undefined."
+  __CPROVER_precondition(i != INT_MIN, "argument to abs must not be INT_MIN");
   return __CPROVER_abs(i);
 }
 
 /* FUNCTION: labs */
 
+#ifndef __CPROVER_LIMITS_H_INCLUDED
+#  include <limits.h>
+#  define __CPROVER_LIMITS_H_INCLUDED
+#endif
+
 #undef labs
 
 long int labs(long int i)
 {
+  // C99 Section 7.20.6.1:
+  // "If the result cannot be represented, the behavior is undefined."
+  __CPROVER_precondition(
+    i != LONG_MIN, "argument to labs must not be LONG_MIN");
   return __CPROVER_labs(i);
 }
 
 /* FUNCTION: llabs */
 
+#ifndef __CPROVER_LIMITS_H_INCLUDED
+#  include <limits.h>
+#  define __CPROVER_LIMITS_H_INCLUDED
+#endif
+
 #undef llabs
 
 long long int llabs(long long int i)
 {
+  // C99 Section 7.20.6.1:
+  // "If the result cannot be represented, the behavior is undefined."
+  __CPROVER_precondition(
+    i != LLONG_MIN, "argument to llabs must not be LLONG_MIN");
   return __CPROVER_llabs(i);
 }
 
@@ -32,12 +58,19 @@ long long int llabs(long long int i)
 #  define __CPROVER_INTTYPES_H_INCLUDED
 #endif
 
+#ifndef __CPROVER_LIMITS_H_INCLUDED
+#  include <limits.h>
+#  define __CPROVER_LIMITS_H_INCLUDED
+#endif
+
 #undef imaxabs
 
 intmax_t __CPROVER_imaxabs(intmax_t);
 
 intmax_t imaxabs(intmax_t i)
 {
+  __CPROVER_precondition(
+    i != INTMAX_MIN, "argument to imaxabs must not be INTMAX_MIN");
   return __CPROVER_imaxabs(i);
 }