From 83d1f312e3db42e6958c702de15bf9bc68ca1081 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 18 Oct 2018 14:37:20 +0000
Subject: [PATCH] Remove unused includes from regression tests

This cleanup avoids giving the false impression we would be testing any
functions declared in those header files, which in turn simplifies moving tests
that exercise the internal modelling library to a separate folder.
---
 regression/cbmc/Endianness6/main.c          | 2 +-
 regression/cbmc/Function_Pointer13/main.c   | 6 ++----
 regression/cbmc/Variadic1/main.c            | 1 -
 regression/cbmc/byte_update1/main.c         | 1 -
 regression/cbmc/byte_update3/main.c         | 1 -
 regression/cbmc/byte_update4/main.c         | 1 -
 regression/cbmc/byte_update5/main.c         | 1 -
 regression/cbmc/complex1/main.c             | 1 -
 regression/cbmc/dynamic_sizeof1/main.c      | 1 -
 regression/cbmc/pointer-extra-checks/main.c | 3 ---
 regression/cbmc/va_list3/main.c             | 1 -
 11 files changed, 3 insertions(+), 16 deletions(-)

diff --git a/regression/cbmc/Endianness6/main.c b/regression/cbmc/Endianness6/main.c
index 1f1085cb3f..2fd577308d 100644
--- a/regression/cbmc/Endianness6/main.c
+++ b/regression/cbmc/Endianness6/main.c
@@ -1,4 +1,4 @@
-#include <stdio.h>
+#include <assert.h>
 
 int main()
 {
diff --git a/regression/cbmc/Function_Pointer13/main.c b/regression/cbmc/Function_Pointer13/main.c
index a3bac9430b..504abee377 100644
--- a/regression/cbmc/Function_Pointer13/main.c
+++ b/regression/cbmc/Function_Pointer13/main.c
@@ -1,5 +1,3 @@
-#include <stdlib.h>
-#include <stdio.h>
 #include <assert.h>
 
 typedef unsigned int u32;
@@ -17,11 +15,11 @@ u32 myfunc_2(u32 value2){
 }
 
 int main(void){
-myfuncptr fptr=NULL;
+  myfuncptr fptr = 0;
 u32 value;
 
 
-assert(fptr == NULL);
+  assert(fptr == 0);
 
 fptr=myfunc_1;
 value=2;
diff --git a/regression/cbmc/Variadic1/main.c b/regression/cbmc/Variadic1/main.c
index d634c6e90f..481ccc5942 100644
--- a/regression/cbmc/Variadic1/main.c
+++ b/regression/cbmc/Variadic1/main.c
@@ -1,5 +1,4 @@
 #include <stdarg.h>
-#include <stdio.h>
 #include <assert.h>
 
 // how to do it:
diff --git a/regression/cbmc/byte_update1/main.c b/regression/cbmc/byte_update1/main.c
index 9171d79328..87e25b2aaa 100644
--- a/regression/cbmc/byte_update1/main.c
+++ b/regression/cbmc/byte_update1/main.c
@@ -1,4 +1,3 @@
-#include <stdio.h>
 #include <assert.h>
 
 struct A {
diff --git a/regression/cbmc/byte_update3/main.c b/regression/cbmc/byte_update3/main.c
index e20eb6588c..9cce10a13e 100644
--- a/regression/cbmc/byte_update3/main.c
+++ b/regression/cbmc/byte_update3/main.c
@@ -1,4 +1,3 @@
-#include <stdio.h>
 #include <assert.h>
 
 int main(int argc, char** argv) {
diff --git a/regression/cbmc/byte_update4/main.c b/regression/cbmc/byte_update4/main.c
index 2866b20a0f..4b72a7db00 100644
--- a/regression/cbmc/byte_update4/main.c
+++ b/regression/cbmc/byte_update4/main.c
@@ -1,4 +1,3 @@
-#include <stdio.h>
 #include <assert.h>
 
 int main(int argc, char** argv) {
diff --git a/regression/cbmc/byte_update5/main.c b/regression/cbmc/byte_update5/main.c
index fc698a2014..7a1ccaa6fb 100644
--- a/regression/cbmc/byte_update5/main.c
+++ b/regression/cbmc/byte_update5/main.c
@@ -1,4 +1,3 @@
-#include <stdio.h>
 #include <assert.h>
 
 int main(int argc, char** argv) {
diff --git a/regression/cbmc/complex1/main.c b/regression/cbmc/complex1/main.c
index 72695b5edf..e2a7eec670 100644
--- a/regression/cbmc/complex1/main.c
+++ b/regression/cbmc/complex1/main.c
@@ -1,5 +1,4 @@
 #include <assert.h>
-#include <stdio.h>
 
 int main()
 {
diff --git a/regression/cbmc/dynamic_sizeof1/main.c b/regression/cbmc/dynamic_sizeof1/main.c
index 14082f936c..dee1908ada 100644
--- a/regression/cbmc/dynamic_sizeof1/main.c
+++ b/regression/cbmc/dynamic_sizeof1/main.c
@@ -1,4 +1,3 @@
-#include <stdlib.h>
 #include <assert.h>
 
 int main()
diff --git a/regression/cbmc/pointer-extra-checks/main.c b/regression/cbmc/pointer-extra-checks/main.c
index 5a920dec4f..a8cfdc94ff 100644
--- a/regression/cbmc/pointer-extra-checks/main.c
+++ b/regression/cbmc/pointer-extra-checks/main.c
@@ -1,6 +1,3 @@
-#include <assert.h>
-#include <stdlib.h>
-
 int main()
 {
   {
diff --git a/regression/cbmc/va_list3/main.c b/regression/cbmc/va_list3/main.c
index 672dff0ba5..2a0c4e9773 100644
--- a/regression/cbmc/va_list3/main.c
+++ b/regression/cbmc/va_list3/main.c
@@ -1,4 +1,3 @@
-#include <stdio.h> 
 #include <stdarg.h> 
 #include <assert.h>