__CPROVER_llabs returns a long long

Fixes the declaration in builtin_headers.h. Type checking actually
ignored this declaration and would always generate the expression of the
correct type.

Author: tautschnig

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

@@ -1,9 +1,13 @@
 #include <assert.h>
-#include <stdlib.h>
+
+#include <limits.h>
+
+#ifndef __GNUC__
+long long __builtin_llabs(long long);
+#endif
 
 int main()
 {
-  __builtin_llabs();
-  assert(0);
+  assert(__builtin_llabs(LLONG_MIN + 1) == LLONG_MAX);
   return 0;
 }

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

@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+--pointer-check --bounds-check --signed-overflow-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

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

@@ -1,9 +1,10 @@
 #include <assert.h>
 #include <stdlib.h>
 
+#include <limits.h>
+
 int main()
 {
-  llabs();
-  assert(0);
+  assert(llabs(LLONG_MIN + 1) == LLONG_MAX);
   return 0;
 }

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

@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+--pointer-check --bounds-check --signed-overflow-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

src/ansi-c/cprover_builtin_headers.h

@@ -84,7 +84,7 @@ int __CPROVER_isunorderedd(double f, double g);
 // absolute value
 int __CPROVER_abs(int x);
 long int __CPROVER_labs(long int x);
-long int __CPROVER_llabs(long long int x);
+long long int __CPROVER_llabs(long long int x);
 double __CPROVER_fabs(double x);
 long double __CPROVER_fabsl(long double x);
 float __CPROVER_fabsf(float x);