Exclude nonsense kernel1 test

goblint · Jul 26, 2024 · ac3a40a · ac3a40a
1 parent f441f54
commit ac3a40a
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/test/small2/kernel1.c b/test/small2/kernel1.c
@@ -1,4 +1,4 @@
-
+// This test is nonsense: DECLARE_WAIT_QUEUE_HEAD is a macro in Linux kernel
 DECLARE_WAIT_QUEUE_HEAD(log_wait);
 
 

diff --git a/test/testcil.pl b/test/testcil.pl
@@ -658,7 +658,7 @@ sub addToGroup {
 addBadComment("scott/globalprob", "Notbug. Not a bug if fails on a non-Linux machine ;-)");
 addTest("scott/bisonerror $gcc");
 addTest("scott/cmpzero");
-addTest("scott/kernel1 $gcc");
+# addTest("scott/kernel1 $gcc");
 addTest("scott/kernel2 $gcc");
 addTest("scott/xcheckers $gcc");
 addTest("scott/memberofptr $gcc");
Original file line number	Diff line number	Diff line change
		@@ -1,4 +1,4 @@

		// This test is nonsense: DECLARE_WAIT_QUEUE_HEAD is a macro in Linux kernel
		DECLARE_WAIT_QUEUE_HEAD(log_wait);


Expand Down