Assume C compiler's default standard is `-std=gnu17`

Newer compilers use `-std=gnu17` as the default when compiling C code.
Fix all the test cases that violate this behaviour or explicitly request
older standards `-std=c89` where necessary.

19 files changed, 24 insertions, 10 deletions

diff --git a/test/regression/2007-07-25-invalid-stp-array-binding-to-objectstate.c b/test/regression/2007-07-25-invalid-stp-array-binding-to-objectstate.c
index 1897266a..ac32063c 100644
--- a/test/regression/2007-07-25-invalid-stp-array-binding-to-objectstate.c
+++ b/test/regression/2007-07-25-invalid-stp-array-binding-to-objectstate.c
@@ -2,6 +2,7 @@
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out %t1.bc
 
+#include "klee/klee.h"
 #include <assert.h>
 
 int main(void) {
diff --git a/test/regression/2007-07-30-unflushed-byte.c b/test/regression/2007-07-30-unflushed-byte.c
index bb480b9a..2d2f1e8c 100644
--- a/test/regression/2007-07-30-unflushed-byte.c
+++ b/test/regression/2007-07-30-unflushed-byte.c
@@ -1,7 +1,7 @@
 // RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out %t1.bc
-
+#include "klee/klee.h"
 #include <assert.h>
 
 int main() {
diff --git a/test/regression/2007-08-01-cache-unclear-on-overwrite-flushed.c b/test/regression/2007-08-01-cache-unclear-on-overwrite-flushed.c
index 96115557..73ceec91 100644
--- a/test/regression/2007-08-01-cache-unclear-on-overwrite-flushed.c
+++ b/test/regression/2007-08-01-cache-unclear-on-overwrite-flushed.c
@@ -2,6 +2,7 @@
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out %t1.bc
 
+#include "klee/klee.h"
 #include <assert.h>
 #include <stdio.h>
 
diff --git a/test/regression/2007-08-06-64bit-shift.c b/test/regression/2007-08-06-64bit-shift.c
index f072e453..675211fd 100644
--- a/test/regression/2007-08-06-64bit-shift.c
+++ b/test/regression/2007-08-06-64bit-shift.c
@@ -2,6 +2,7 @@
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out %t1.bc
 
+#include "klee/klee.h"
 #include <assert.h>
 
 int main() {
diff --git a/test/regression/2007-08-06-access-after-free.c b/test/regression/2007-08-06-access-after-free.c
index 7d1f81db..ef47c868 100644
--- a/test/regression/2007-08-06-access-after-free.c
+++ b/test/regression/2007-08-06-access-after-free.c
@@ -2,7 +2,9 @@
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out %t1.bc
 
+#include "klee/klee.h"
 #include <assert.h>
+#include <stdlib.h>
 
 int main() {
   int a;
diff --git a/test/regression/2007-08-16-invalid-constant-value.c b/test/regression/2007-08-16-invalid-constant-value.c
index c49357f8..f5474f7a 100644
--- a/test/regression/2007-08-16-invalid-constant-value.c
+++ b/test/regression/2007-08-16-invalid-constant-value.c
@@ -1,5 +1,5 @@
 // RUN: rm -f %t4.out %t4.err %t4.log
-// RUN: %clang %s -emit-llvm -O2 -c -o %t1.bc
+// RUN: %clang %s -std=c89 -emit-llvm -O2 -c -o %t1.bc
 // RUN: %llvmas -f %p/../Feature/_utils._ll -o %t2.bc
 // RUN: %llvmlink %t1.bc %t2.bc -o %t3.bc
 // RUN: rm -rf %t.klee-out
@@ -7,8 +7,6 @@
 
 #include <assert.h>
 
-#include "../Feature/utils.h"
-
 int main() {
   unsigned char a;
 
diff --git a/test/regression/2007-08-16-valid-write-to-freed-object.c b/test/regression/2007-08-16-valid-write-to-freed-object.c
index 6b6efecb..2a43a240 100644
--- a/test/regression/2007-08-16-valid-write-to-freed-object.c
+++ b/test/regression/2007-08-16-valid-write-to-freed-object.c
@@ -2,6 +2,8 @@
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out %t1.bc
 
+#include "klee/klee.h"
+#include <stdio.h>
 unsigned sym() {
   unsigned x;
   klee_make_symbolic(&x, sizeof x, "x");
diff --git a/test/regression/2007-10-11-free-of-alloca.c b/test/regression/2007-10-11-free-of-alloca.c
index 6aa6cdb3..cecdeef2 100644
--- a/test/regression/2007-10-11-free-of-alloca.c
+++ b/test/regression/2007-10-11-free-of-alloca.c
@@ -2,7 +2,7 @@
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck %s
 // RUN: test -f %t.klee-out/test000001.free.err
-
+#include <stdlib.h>
 int main() {
   int buf[4];
   // CHECK: 2007-10-11-free-of-alloca.c:9: free of alloca
diff --git a/test/regression/2007-10-12-failed-make-symbolic-after-copy.c b/test/regression/2007-10-12-failed-make-symbolic-after-copy.c
index 64cae9f4..77f9b9f6 100644
--- a/test/regression/2007-10-12-failed-make-symbolic-after-copy.c
+++ b/test/regression/2007-10-12-failed-make-symbolic-after-copy.c
@@ -2,7 +2,7 @@
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out %t1.bc
 // RUN: test -f %t.klee-out/test000001.ktest
-
+#include "klee/klee.h"
 int main() {
   unsigned x, y[4];
 
diff --git a/test/regression/2008-03-04-free-of-global.c b/test/regression/2008-03-04-free-of-global.c
index 995e7173..fb4a2df8 100644
--- a/test/regression/2008-03-04-free-of-global.c
+++ b/test/regression/2008-03-04-free-of-global.c
@@ -3,10 +3,11 @@
 // RUN: %klee --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck %s
 // RUN: test -f %t.klee-out/test000001.free.err
 
+#include <stdlib.h>
 int buf[4];
 
 int main() {
-  // CHECK: 2008-03-04-free-of-global.c:10: free of global
+  // CHECK: 2008-03-04-free-of-global.c:[[@LINE+1]]: free of global
   free(buf); // this should give runtime error, not crash
   return 0;
 }
diff --git a/test/regression/2008-03-11-free-of-malloc-zero.c b/test/regression/2008-03-11-free-of-malloc-zero.c
index e90baa2c..cdd2ef35 100644
--- a/test/regression/2008-03-11-free-of-malloc-zero.c
+++ b/test/regression/2008-03-11-free-of-malloc-zero.c
@@ -1,7 +1,7 @@
 // RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc
-
+#include "klee/klee.h"
 #include <stdlib.h>
 
 int main() {
diff --git a/test/regression/2008-04-10-bad-alloca-free.c b/test/regression/2008-04-10-bad-alloca-free.c
index 5049f47c..d20d07d2 100644
--- a/test/regression/2008-04-10-bad-alloca-free.c
+++ b/test/regression/2008-04-10-bad-alloca-free.c
@@ -2,6 +2,7 @@
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc
 
+#include "klee/klee.h"
 void f(int *addr) {
   klee_make_symbolic(addr, sizeof *addr, "moo");
 }
diff --git a/test/regression/2014-07-04-unflushed-error-report.c b/test/regression/2014-07-04-unflushed-error-report.c
index c929328d..058aef7e 100644
--- a/test/regression/2014-07-04-unflushed-error-report.c
+++ b/test/regression/2014-07-04-unflushed-error-report.c
@@ -6,6 +6,7 @@
 /* This test checks that the error file isn't empty and contains the
  * right content.
  */
+#include "klee/klee.h"
 int main() {
   unsigned int x = 15;
   unsigned int y;
diff --git a/test/regression/2015-08-05-invalid-fork.c b/test/regression/2015-08-05-invalid-fork.c
index a165cab2..5c09cbfc 100644
--- a/test/regression/2015-08-05-invalid-fork.c
+++ b/test/regression/2015-08-05-invalid-fork.c
@@ -3,6 +3,7 @@
    is printed a single time. 
 */
 #include "klee/klee.h"
+#include <stdio.h>
 
 // RUN: %clang %s -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
diff --git a/test/regression/2015-08-30-empty-constraints.c b/test/regression/2015-08-30-empty-constraints.c
index f92b6978..8598b6ae 100644
--- a/test/regression/2015-08-30-empty-constraints.c
+++ b/test/regression/2015-08-30-empty-constraints.c
@@ -10,6 +10,7 @@
  * are generated.
  * Make sure we are able to generate an input.
  */
+#include "klee/klee.h"
 int main() {
   int d;
 
diff --git a/test/regression/2015-08-30-sdiv-1.c b/test/regression/2015-08-30-sdiv-1.c
index 7356e74c..2b819aea 100644
--- a/test/regression/2015-08-30-sdiv-1.c
+++ b/test/regression/2015-08-30-sdiv-1.c
@@ -7,6 +7,7 @@
 /* Division by constant can be optimized.using mul/shift
  * For signed division, div by 1 or -1 cannot be optimized like that.
  */
+#include "klee/klee.h"
 #include <stdint.h>
 int main() {
   int32_t dividend;
diff --git a/test/regression/2017-02-21-pathOS-id.c b/test/regression/2017-02-21-pathOS-id.c
index b6ee269a..112875de 100644
--- a/test/regression/2017-02-21-pathOS-id.c
+++ b/test/regression/2017-02-21-pathOS-id.c
@@ -5,6 +5,9 @@
 // RUN: cat %t.klee-out/test000002.path | wc -l | grep -q 1
 // RUN: cat %t.klee-out/test000003.path | wc -l | grep -q 1
 // RUN: cat %t.klee-out/test000004.path | wc -l | grep -q 1
+
+#include "klee/klee.h"
+#include "stdlib.h"
 int main(){
 	int a, b;
 	klee_make_symbolic (&a, sizeof(int), "a");
diff --git a/test/regression/2017-11-01-test-with-empty-varname.c b/test/regression/2017-11-01-test-with-empty-varname.c
index 89108d9d..578043ad 100644
--- a/test/regression/2017-11-01-test-with-empty-varname.c
+++ b/test/regression/2017-11-01-test-with-empty-varname.c
@@ -2,7 +2,7 @@
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out %t1.bc
 // RUN: FileCheck %s --input-file=%t.klee-out/warnings.txt
-
+#include "klee/klee.h"
 int main() {
   unsigned a;
 
diff --git a/test/regression/2020-04-27-stp-array-names.c b/test/regression/2020-04-27-stp-array-names.c
index f06e1b1a..a256441c 100644
--- a/test/regression/2020-04-27-stp-array-names.c
+++ b/test/regression/2020-04-27-stp-array-names.c
@@ -1,4 +1,4 @@
-// RUN: %clang %s -emit-llvm %O0opt -g -c -o %t.bc
+// RUN: %clang -std=c89 %s -emit-llvm %O0opt -g -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee -output-dir=%t.klee-out --search=bfs --max-instructions=1000 %t.bc
 b;