Merge pull request #1201 from sosy-lab/line-endings

Normalize line endings in relevant parts of the repository

Author: dbeyer

.gitattributes

@@ -0,0 +1,24 @@
+# This file is part of the SV-Benchmarks collection of verification tasks:
+# https://github.com/sosy-lab/sv-benchmarks
+#
+# SPDX-FileCopyrightText: 2011-2020 The SV-Benchmarks Community
+#
+# SPDX-License-Identifier: Apache-2.0
+
+# Enable git's auto-detection of text files and enable normalization of line endings
+* text=auto
+# Force certain file types to be always considered as text with normalized line endings
+*.c text
+*.h text
+*.i text
+*.java text
+*.md text
+*.py text
+*.set text
+*.txt text
+*.yml text
+Makefile text
+Makefile.* text
+# Prevent changes to certain large directories where it is not relevant now
+clauses/** !text
+c/Juliet_Test/Juliet_Test_Suite_v1.3_for_C_Cpp/** !text

c/array-industry-pattern/ReadMe.txt

@@ -1,2 +1,2 @@
-Programs handling arrays. 
+Programs handling arrays. 
 These programs are based on patterns observed in industry applications.

c/array-lopstr16/break-2.c

@@ -1,32 +1,32 @@
 extern void abort(void);
 #include <assert.h>
 void reach_error() { assert(0); }
-void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: {reach_error();abort();} } }
-#define SIZE 1000000
-struct S
-{
-	int n;
-};
-
-struct S s[SIZE];
-
-int main()
-{
-	int i;
-
-	for(i = 0; i < SIZE; i++)
-	{
-		if(i > SIZE / 2)
-			break;
-
-		s[i].n = 10;
-	}
-
-	for(i = 0; i < SIZE; i++)
-	{
-		if(i <= SIZE /2 )
-			__VERIFIER_assert(s[i].n == 10);
-	}
-
-	return 0;
-}
+void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: {reach_error();abort();} } }
+#define SIZE 1000000
+struct S
+{
+	int n;
+};
+
+struct S s[SIZE];
+
+int main()
+{
+	int i;
+
+	for(i = 0; i < SIZE; i++)
+	{
+		if(i > SIZE / 2)
+			break;
+
+		s[i].n = 10;
+	}
+
+	for(i = 0; i < SIZE; i++)
+	{
+		if(i <= SIZE /2 )
+			__VERIFIER_assert(s[i].n == 10);
+	}
+
+	return 0;
+}

c/array-lopstr16/motivex.c

@@ -1,40 +1,40 @@
 extern void abort(void);
 #include <assert.h>
 void reach_error() { assert(0); }
-void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: {reach_error();abort();} } }
-extern short __VERIFIER_nondet_short(void);
-#define SIZE 1000000
-struct S {
-	unsigned short p;		  
-	unsigned short q;		 		  
-} a[10000];
-
-int main()
-{
-	unsigned char k;
-	
-	int i;
-	for (i  = 0; i < SIZE ; i++)
-	{
-		a[i].p = i; 
-		a[i].q = i ;
-	}
-
-	for (i = 0; i < SIZE; i++)
-	{
-		if (__VERIFIER_nondet_short() )
-		{
-			k = __VERIFIER_nondet_short();
-			a[i].p = k;
-			a[i].q = k * k ;
-		}
-	}
-
-	for (i = 0; i < SIZE; i++)
-	{
-		__VERIFIER_assert(a[i].p == a[i].q || a[i].q == a[i].p * a[i].p);
-	}
-
-	return 0;
-}
-
+void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: {reach_error();abort();} } }
+extern short __VERIFIER_nondet_short(void);
+#define SIZE 1000000
+struct S {
+	unsigned short p;		  
+	unsigned short q;		 		  
+} a[10000];
+
+int main()
+{
+	unsigned char k;
+	
+	int i;
+	for (i  = 0; i < SIZE ; i++)
+	{
+		a[i].p = i; 
+		a[i].q = i ;
+	}
+
+	for (i = 0; i < SIZE; i++)
+	{
+		if (__VERIFIER_nondet_short() )
+		{
+			k = __VERIFIER_nondet_short();
+			a[i].p = k;
+			a[i].q = k * k ;
+		}
+	}
+
+	for (i = 0; i < SIZE; i++)
+	{
+		__VERIFIER_assert(a[i].p == a[i].q || a[i].q == a[i].p * a[i].p);
+	}
+
+	return 0;
+}
+

c/array-lopstr16/scalar_loopdep.c

@@ -1,36 +1,36 @@
 extern void abort(void);
 #include <assert.h>
 void reach_error() { assert(0); }
-void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: {reach_error();abort();} } }
-
-#define SIZE 100000
-struct _S
-{
-	int n;
-};
-typedef struct _S S;
-
-S a[SIZE];
-
-int main()
-{
-	int i,x;
-	int y = 100;
-	for(i = 0; i < SIZE; i++)
-	{
-		x = y;
-		a[i].n = y;
-		y++;
-	}
-
-
-	for(i = 0; i < SIZE; i++)
-	{
-		__VERIFIER_assert(a[i].n >= 100);
-		
-	}
-
-	return 0;
-}
-
-
+void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: {reach_error();abort();} } }
+
+#define SIZE 100000
+struct _S
+{
+	int n;
+};
+typedef struct _S S;
+
+S a[SIZE];
+
+int main()
+{
+	int i,x;
+	int y = 100;
+	for(i = 0; i < SIZE; i++)
+	{
+		x = y;
+		a[i].n = y;
+		y++;
+	}
+
+
+	for(i = 0; i < SIZE; i++)
+	{
+		__VERIFIER_assert(a[i].n >= 100);
+		
+	}
+
+	return 0;
+}
+
+

c/array-lopstr16/sum_multi_array.c

@@ -1,43 +1,43 @@
 extern void abort(void);
 #include <assert.h>
 void reach_error() { assert(0); }
-void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: {reach_error();abort();} } }
-extern int __VERIFIER_nondet_int();
-#define SIZE 1000000
-struct _S
-{
-	int n;
-};
-typedef struct _S S;
-
-S a[SIZE];
-S b[SIZE];
-S c[SIZE];
-
-int main()
-{
-	
-	int i;
-
-	for(i = 0; i < SIZE; i++)
-	{
-		int v;
-	        v = __VERIFIER_nondet_int();
-		a[i].n= v;
-		v = __VERIFIER_nondet_int();
-		b[i].n = v;
-	}
-	
-	for(i = 0; i < SIZE; i++)
-	{
-		c[i].n = a[i].n + b[i].n;
-	}
-
-	for(i = 0; i < SIZE; i++)
-	{
-		__VERIFIER_assert(c[i].n == a[i].n + b[i].n);
-	}
-
-	return 0;
-}
-
+void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: {reach_error();abort();} } }
+extern int __VERIFIER_nondet_int();
+#define SIZE 1000000
+struct _S
+{
+	int n;
+};
+typedef struct _S S;
+
+S a[SIZE];
+S b[SIZE];
+S c[SIZE];
+
+int main()
+{
+	
+	int i;
+
+	for(i = 0; i < SIZE; i++)
+	{
+		int v;
+	        v = __VERIFIER_nondet_int();
+		a[i].n= v;
+		v = __VERIFIER_nondet_int();
+		b[i].n = v;
+	}
+	
+	for(i = 0; i < SIZE; i++)
+	{
+		c[i].n = a[i].n + b[i].n;
+	}
+
+	for(i = 0; i < SIZE; i++)
+	{
+		__VERIFIER_assert(c[i].n == a[i].n + b[i].n);
+	}
+
+	return 0;
+}
+

c/array-memsafety/README.txt

@@ -1,19 +1,19 @@
-C programs for termination analysis, that were used by AProVE:
-
-http://aprove.informatik.rwth-aachen.de/
-
-The benchmarks were contributed by:
-Frank Emrich
-Stephan Falke
-Matthias Heizmann
-Jera Hensel
-Janine Repke
-Thomas Ströder
-
-You may use and redistribute them according to the (2-clause) BSD license that is shipped with these examples.
-
-[comment by Ondrej Lengal (11 Oct 2015):
-
-  Array examples were moved from memory-alloca/ here in commit f3f1cdf .
-]
-
+C programs for termination analysis, that were used by AProVE:
+
+http://aprove.informatik.rwth-aachen.de/
+
+The benchmarks were contributed by:
+Frank Emrich
+Stephan Falke
+Matthias Heizmann
+Jera Hensel
+Janine Repke
+Thomas Ströder
+
+You may use and redistribute them according to the (2-clause) BSD license that is shipped with these examples.
+
+[comment by Ondrej Lengal (11 Oct 2015):
+
+  Array examples were moved from memory-alloca/ here in commit f3f1cdf .
+]
+

c/array-multidimensional/ReadMe.txt

@@ -1 +1 @@
-Benchmarks used in the paper "Extending VIAP to Handle Array Program" which was published at VSTTE 2018 and written by Pritom Rajkhowa and Fangzhen Lin
+Benchmarks used in the paper "Extending VIAP to Handle Array Program" which was published at VSTTE 2018 and written by Pritom Rajkhowa and Fangzhen Lin