Merge pull request #323 from rjmunro/normalize-whitespace

Normalize whitespace

Author: Daniel Kroening

doc/html-manual/boop-example/driver.c

@@ -18,7 +18,7 @@ int dummy_open (struct inode *inode, struct file *filp)
   if (locked)
     return -1;
   locked = TRUE;
- 
+
   return 0; /* success */
 }
 
@@ -30,7 +30,7 @@ unsigned int dummy_read (struct file *filp, char *buf, int max)
       n = nondet_int ();
       __CPROVER_assume ((n >= 0) && (n <= max));
       /* writing to the buffer is not modeled here */
-      
+
       return n;
     }
   return -1;
@@ -46,4 +46,3 @@ int dummy_release (struct inode *inode, struct file *filp)
     }
   return -1;
 }
-

doc/html-manual/boop-example/spec.c

@@ -31,7 +31,7 @@ int main ()
   unsigned int   count;
   unsigned char  random;
 
-  int lock_held = 0; 
+  int lock_held = 0;
 
   dummy_major = register_chrdev (0, "dummy");
   inode.i_rdev = dummy_major << MINORBITS;
@@ -49,14 +49,14 @@ int main ()
 
       switch (random)
 	{
-	case 1: 
+	case 1:
 	  rval = dummy_open (&inode, &my_file);
 	  if (rval == 0)
 	    lock_held = TRUE;
 	  break;
 	case 2:
 	  __CPROVER_assume (lock_held);
-	  count = dummy_read (&my_file, buffer, BUF_SIZE); 
+	  count = dummy_read (&my_file, buffer, BUF_SIZE);
 	  break;
 	case 3:
 	  dummy_release (&inode, &my_file);

doc/html-manual/gcc-wrap.c

@@ -16,7 +16,7 @@ void run(const char *what, char *const argv[])
 
   /* now create new process */
   childpid = fork();
-    
+
   if(childpid>=0) /* fork succeeded */
   {
     if(childpid==0) /* fork() returns 0 to the child process */
@@ -40,24 +40,24 @@ void run(const char *what, char *const argv[])
     exit(1);
   }
 }
- 
+
 int main(int argc, char * argv[])
 {
   // First do original call.
-  
+
   // on some systems, gcc gets confused if it is not argument 0
   // (which normally contains the path to the executable being called).
   argv[0]=strdup(gcc);
 
   run(gcc, argv);
-  
+
   // now do preprocessing call
   char **new_argv=malloc(sizeof(char *)*(argc+1));
-  
+
   _Bool compile=0;
   _Bool assemble=0;
   _Bool next_is_o=0;
-  
+
   unsigned i;
 
   for(i=0; i<argc; i++)
@@ -72,7 +72,7 @@ int main(int argc, char * argv[])
 
       if(strcmp(tmp+l-2, ".o")==0)
         tmp[l-2]=0; // cut off .o
-      
+
       strcat(tmp, ".i"); // append .i
       arg=tmp;
       next_is_o=0;
@@ -100,13 +100,13 @@ int main(int argc, char * argv[])
 
     new_argv[i]=arg;
   }
-  
+
   new_argv[argc]=NULL;
-  
+
   if(compile && !assemble)
   {
     run(gcc, new_argv);
   }
-    
+
   return 0;
 }

doc/html-manual/header.inc

@@ -21,4 +21,3 @@
 <li><a href="/hardware/">Hardware Verification</a></li>
 </ul>
 </div>
-

doc/html-manual/pid.c

@@ -30,7 +30,7 @@ float desired_pitch;
 float climb_sum_err=0;
 
 /** Computes desired_gaz and desired_pitch */
-void climb_pid_run() 
+void climb_pid_run()
 {
 
   float err=estimator_z_dot-desired_climb;
@@ -39,7 +39,7 @@ void climb_pid_run()
 
   float pprz=fgaz*MAX_PPRZ;
   desired_gaz=((pprz>=0 && pprz<=MAX_PPRZ) ? pprz : (pprz>MAX_PPRZ ? MAX_PPRZ : 0));
-  
+
   /** pitch offset for climb */
   float pitch_of_vz=(desired_climb>0) ? desired_climb*pitch_of_vz_pgain : 0;
   desired_pitch=nav_pitch+pitch_of_vz;
@@ -55,18 +55,18 @@ int main()
 
   while(1)
   {
-    /** Non-deterministic input values */ 
+    /** Non-deterministic input values */
     desired_climb=nondet_float();
     estimator_z_dot=nondet_float();
 
-    /** Range of input values */ 
+    /** Range of input values */
     __CPROVER_assume(desired_climb>=-MAX_CLIMB && desired_climb<=MAX_CLIMB);
     __CPROVER_assume(estimator_z_dot>=-MAX_CLIMB && estimator_z_dot<=MAX_CLIMB);
 
     __CPROVER_input("desired_climb", desired_climb);
     __CPROVER_input("estimator_z_dot", estimator_z_dot);
 
-    climb_pid_run(); 
+    climb_pid_run();
 
     __CPROVER_output("desired_gaz", desired_gaz);
     __CPROVER_output("desired_pitch", desired_pitch);
@@ -75,4 +75,3 @@ int main()
 
   return 0;
 }
-

doc/html-manual/ring_buffer1.c

@@ -15,14 +15,14 @@ unsigned int ring_buffer[SIZE];
 int main()
 {
   unsigned index=0;
-  
+
   while(1)
   {
     unsigned output;
     output=ring_buffer[index];
     printf("%u\n", output);
     assert(output<=MAX);
-    
+
     ring_buffer[index]=sample();
 
     index=(index+1)%SIZE;

doc/html-manual/ring_buffer2.c

@@ -15,14 +15,14 @@ unsigned int ring_buffer[SIZE];
 int main()
 {
   unsigned index=0, previous_index=SIZE-1;
-  
+
   while(1)
   {
     unsigned output;
     output=(ring_buffer[index]+ring_buffer[previous_index])/2;
     assert(ring_buffer[index]<=MAX);
     assert(output<=MAX);
-    
+
     ring_buffer[index]=sample();
 
     previous_index=index;

regression/ansi-c/Array_Declarator1/main.c

@@ -22,7 +22,7 @@ keyword static also appears within the [ and ] of the array type
 derivation, then for each call to the function, the value of the
 corresponding actual argument shall provide access to the first element
 of an array with at least as many elements as specified by the size
-expression. 
+expression.
 
 6.7.5.3(21):
 The following are all compatible function prototype declarators.
@@ -39,10 +39,10 @@ as are:
 corresponding to a in any call to f must be a non-null pointer to the
 first of at least three arrays of 5 doubles, which the others do not.)
 
-The comments in the rule for array_abstract_declarator in 
+The comments in the rule for array_abstract_declarator in
 src/ansi-c/parser.y indicate awareness of the standard regarding this
 issue, however, it seems that the case where both TOK_STATIC and
-attribute_type_qualifier_list (in either order) occur is not covered, 
+attribute_type_qualifier_list (in either order) occur is not covered,
 even though the standard allows this combination.
 
 Further investigation into this issue also revealed that the rules

regression/ansi-c/Array_Declarator3/main.c

@@ -7,4 +7,3 @@ int main(void)
   int bar0[restrict] = {0};
   return 0;
 }
-

regression/ansi-c/Atomic1/main.c

@@ -1,9 +1,9 @@
 // _Atomic is a C11 keyword. It can be used as a type qualifier
 // and as a type specifier, which introduces ambiguity into the grammar.
-               
+
 // 6.7.2.4 - 4: If the _Atomic keyword is immediately followed by a left
 // parenthesis, it is interpreted as a type specifier (with a type name),
-// not as a type qualifier. 
+// not as a type qualifier.
 
 // Visual Studio doesn't have it, will likely never have it.
 

regression/ansi-c/Header_files1/main.c

@@ -28,4 +28,3 @@ int main()
 {
   return 0;
 }
-

regression/ansi-c/Header_files1/test.desc

@@ -8,4 +8,3 @@ main.c
 ^CONVERSION ERROR$
 is not declared$
 --
-

regression/ansi-c/Initializer_cast1/main.c

@@ -21,18 +21,18 @@ int main()
   struct S s;
   union U u;
 
-  // scalar  
+  // scalar
   l=(long){0x1};
-  
+
   // struct
   s=(struct S){ 1, 2, 3, 4, 5, 6 };
-  
+
   // union
   u=(union U)s;
-  
+
   // union
   u=(union U){ 1 };
-  
+
   // array
   const int *a=(array_type){ 1, 2, 3, 4 };
 }

regression/ansi-c/KnR1/main.c

@@ -37,4 +37,3 @@ int main()
 {
   return d(-1)!=0;
 }
-

regression/ansi-c/KnR2/main.c

@@ -12,4 +12,3 @@ register int x;
 int main()
 {
 }
-

regression/ansi-c/KnR3/main.c

@@ -29,4 +29,3 @@ int main()
 {
   return whois_func_head(0)==0;
 }
-

regression/ansi-c/Lvalue1/main.c

@@ -14,4 +14,3 @@ int main()
   const char *f=&(__FUNCTION__[2]);
   char *p=&(char){':'};
 }
-

regression/ansi-c/MMX1/main.c

@@ -5,13 +5,13 @@
 int main()
 {
   // This is a gcc extension
-  #ifdef __GNUC__  
+  #ifdef __GNUC__
   #ifdef __MMX__
   __m64 x;
-  
+
   long long unsigned di;
-  
-  x=(__m64)di;  
+
+  x=(__m64)di;
   #endif
   #endif
 

regression/ansi-c/Qualifiers1/main.c

@@ -16,11 +16,11 @@ int main()
   volatile int * const p=(int * const)&a;
   *((int * const)&a) = 1;
   *p=2;
-  
+
   f(&a);
   g(&a);
 
-  // now with typedef  
+  // now with typedef
   ptr_constant pp1;
   const_ptr_constant pp2=pp1;
 }

regression/ansi-c/Recursive_Structure2/main.c

@@ -12,4 +12,3 @@ int main()
 
   return 0;
 }
-

regression/ansi-c/Struct_Bitfields1/main.c

@@ -44,7 +44,7 @@ int main()
   s1.my_bit++;
   ++s1.my_bit;
   (unsigned)s1.my_bit;
-  
+
   int *p;
   p=p+s1.my_bit;
   p=p-s1.my_bit;

regression/ansi-c/Struct_Enum_Padding1/main.c

@@ -27,4 +27,3 @@ STATIC_ASSERT(sizeof(struct ofpact) == 4);
 int main()
 {
 }
-

regression/ansi-c/Struct_Padding2/main.c

@@ -157,4 +157,3 @@ STATIC_ASSERT(
 int main()
 {
 }
-

regression/ansi-c/Struct_Padding3/main.c

@@ -19,7 +19,7 @@ STATIC_ASSERT(__builtin_offsetof(struct my_struct1a, ch2)==5);
 struct my_struct1b {
   char ch1;
   // this would normally be padded, but it won't!
-  int i __attribute__((packed)); 
+  int i __attribute__((packed));
   char ch2;
 };
 
@@ -31,7 +31,7 @@ struct my_struct1c {
   // this would normally be padded, but it won't!
   struct
   {
-    int i; 
+    int i;
   } sub __attribute__((packed));
   char ch2;
 };
@@ -115,4 +115,3 @@ STATIC_ASSERT(__builtin_offsetof(struct my_struct3, i3)==28);
 int main()
 {
 }
-

regression/ansi-c/Transparent_union1/main.c

@@ -35,11 +35,11 @@ int main()
 {
   struct S1 s1;
   struct S2 s2;
-  
+
   f1(&s1);
   f1(&s2);
   f1(0);
-  
+
   f2(0);
   f2(1>2); // these are int
 }

regression/ansi-c/Typecast_to_array_ptr1/main.c

@@ -6,4 +6,3 @@ int main()
 
   return 0;
 }
-

regression/ansi-c/Typecast_to_union1/main.c

@@ -10,7 +10,7 @@ union U
 int main()
 {
   union U u;
-  
+
   u=(union U)(1>2); // the relational operators return "int"
   u=(union U)(1 && 1);
   u=(union U)1.0; // the literal is double, not float