CBMC library regression tests: ensure GNUC-only declarations are present

MSVC won't have the built-in declarations available, and will thus fail
type checking.

Author: tautschnig

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

@@ -1,5 +1,9 @@
 #include <assert.h>
 
+#ifndef __GNUC__
+_Bool __atomic_always_lock_free(__CPROVER_size_t, void *);
+#endif
+
 int main()
 {
   assert(__atomic_always_lock_free(sizeof(int), 0));

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

@@ -1,5 +1,9 @@
 #include <assert.h>
 
+#ifndef __GNUC__
+void __atomic_clear(_Bool *, int);
+#endif
+
 int main()
 {
   _Bool n;

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

@@ -1,5 +1,9 @@
 #include <assert.h>
 
+#ifndef __GNUC__
+_Bool __atomic_is_lock_free(__CPROVER_size_t, void *);
+#endif
+
 int main()
 {
   assert(__atomic_is_lock_free(sizeof(int), 0));

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

@@ -1,5 +1,9 @@
 #include <assert.h>
 
+#ifndef __GNUC__
+void __atomic_signal_fence(int);
+#endif
+
 int main()
 {
   __atomic_signal_fence(0);

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

@@ -1,5 +1,9 @@
 #include <assert.h>
 
+#ifndef __GNUC__
+_Bool __atomic_test_and_set(void *, int);
+#endif
+
 int main()
 {
   char c = 0;

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

@@ -1,5 +1,9 @@
 #include <assert.h>
 
+#ifndef __GNUC__
+void __atomic_thread_fence(int);
+#endif
+
 int main()
 {
   __atomic_thread_fence(0);

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

@@ -1,5 +1,9 @@
 #include <setjmp.h>
 
+#ifndef __GNUC__
+#  define _longjmp(a, b) longjmp(a, b)
+#endif
+
 static jmp_buf env;
 
 int main()

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

@@ -1,8 +1,8 @@
 CORE
 main.c
 --pointer-check --bounds-check
-^\[_longjmp.assertion.1\] line 12 _longjmp requires instrumentation: FAILURE$
-^\[main.assertion.1\] line 8 unreachable: SUCCESS$
+^\[_?longjmp.assertion.1\] line 12 _?longjmp requires instrumentation: FAILURE$
+^\[main.assertion.1\] line 12 unreachable: SUCCESS$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$