STP: Remove stray semi-colons.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@100391 91177308-0d34-0410-b5e6-96231b3b80d8

21 files changed, 28 insertions, 28 deletions

diff --git a/stp/AST/AST.cpp b/stp/AST/AST.cpp
index 87541877..e75620ec 100644
--- a/stp/AST/AST.cpp
+++ b/stp/AST/AST.cpp
@@ -1575,5 +1575,5 @@ namespace BEEV {
   BeevMgr::~BeevMgr() {
     ClearAllTables();
   }
-}; // end namespace
+} // end namespace
 
diff --git a/stp/AST/AST.h b/stp/AST/AST.h
index 202f6598..4277029e 100644
--- a/stp/AST/AST.h
+++ b/stp/AST/AST.h
@@ -1011,7 +1011,7 @@ namespace BEEV {
     if (_int_node_ptr) {
       _int_node_ptr->DecRef();
     }
-  };
+  }
 #else
   // No refcounting
   inline void ASTInternal::DecRef()
@@ -1802,5 +1802,5 @@ namespace BEEV {
     }
   };
 
-}; // end namespace BEEV
+} // end namespace BEEV
 #endif
diff --git a/stp/AST/ASTKind.h b/stp/AST/ASTKind.h
index d069fdcf..2480b6e6 100644
--- a/stp/AST/ASTKind.h
+++ b/stp/AST/ASTKind.h
@@ -58,7 +58,7 @@ namespace BEEV {
     WRITE,
     ARRAY,
     BITVECTOR,
-    BOOLEAN,
+    BOOLEAN
 } Kind;
 
 extern unsigned char _kind_categories[];
@@ -73,7 +73,7 @@ extern const char *_kind_names[];
 inline ostream& operator<<(ostream &os, const Kind &kind) { os << _kind_names[kind]; return os; }
 
 
-};  // end namespace
+}  // end namespace
 
 
 #endif
diff --git a/stp/AST/ASTUtil.cpp b/stp/AST/ASTUtil.cpp
index bc36812c..ecb54a4a 100644
--- a/stp/AST/ASTUtil.cpp
+++ b/stp/AST/ASTUtil.cpp
@@ -42,4 +42,4 @@ namespace BEEV {
     }
     s[functionname] += 1;
   }
-};// end of namespace
+} // end of namespace
diff --git a/stp/AST/ASTUtil.h b/stp/AST/ASTUtil.h
index 0ed6bfa2..c90ee0ce 100644
--- a/stp/AST/ASTUtil.h
+++ b/stp/AST/ASTUtil.h
@@ -103,5 +103,5 @@ namespace BEEV {
   //corresponding ASTNode and prints a char* of that ASTNode
   void Convert_MINISATVar_To_ASTNode_Print(int minisat_var, 
 					   int decision, int polarity=0);
-}; // end namespace.
+} // end namespace.
 #endif
diff --git a/stp/AST/ToSAT.cpp b/stp/AST/ToSAT.cpp
index 7a164c9c..29635ec5 100644
--- a/stp/AST/ToSAT.cpp
+++ b/stp/AST/ToSAT.cpp
@@ -1382,4 +1382,4 @@ namespace BEEV {
       }
     }
   }
-}; //end of namespace BEEV
+} //end of namespace BEEV
diff --git a/stp/AST/genkinds.pl b/stp/AST/genkinds.pl
index 7944832b..672481ad 100755
--- a/stp/AST/genkinds.pl
+++ b/stp/AST/genkinds.pl
@@ -83,7 +83,7 @@ sub gen_h_file {
 	"/** Prints symbolic name of kind */\n",
 	"inline ostream& operator<<(ostream &os, const Kind &kind) { os << _kind_names[kind]; return os; }\n",
 	"\n\n",
-	"};  // end namespace\n",
+	"}  // end namespace\n",
 	"\n\n#endif\n";
 
     close(HFILE);
@@ -112,7 +112,7 @@ sub gen_cpp_file {
     }
     print CPPFILE 
 	"};\n",
-	"\n};  // end namespace\n";
+	"\n}  // end namespace\n";
 
     close(CPPFILE);
 }
diff --git a/stp/bitvec/consteval.cpp b/stp/bitvec/consteval.cpp
index 7cb8dfcb..8fa652cf 100644
--- a/stp/bitvec/consteval.cpp
+++ b/stp/bitvec/consteval.cpp
@@ -1041,4 +1041,4 @@ namespace BEEV {
     return iii;
   }
 */
-}; //end of namespace BEEV
+} //end of namespace BEEV
diff --git a/stp/constantbv/constantbv.cpp b/stp/constantbv/constantbv.cpp
index 65698981..e01fa0ac 100644
--- a/stp/constantbv/constantbv.cpp
+++ b/stp/constantbv/constantbv.cpp
@@ -3568,4 +3568,4 @@ void Matrix_Transpose(unsigned int *  X, unsigned int rowsX, unsigned int colsX,
     }
   }
 }
-}; //end of namespace CONSTANTBV
+} //end of namespace CONSTANTBV
diff --git a/stp/constantbv/constantbv.h b/stp/constantbv/constantbv.h
index 47e0c56f..bd64132d 100644
--- a/stp/constantbv/constantbv.h
+++ b/stp/constantbv/constantbv.h
@@ -309,8 +309,8 @@ namespace CONSTANTBV {
       0x05, 0x06, 0x06, 0x07,  0x06, 0x07, 0x07, 0x08  /* 0xF0 */
     };
 #ifdef __cplusplus
-  };
+  }
 #endif
-}; //end of namespace CONSTANTBV
+} //end of namespace CONSTANTBV
 #endif
 
diff --git a/stp/sat/Global.h b/stp/sat/Global.h
index a428975c..deaf8c24 100644
--- a/stp/sat/Global.h
+++ b/stp/sat/Global.h
@@ -194,7 +194,7 @@ template<class V, class T>
 void remove(V& ts, const T& t)
 {
     int j = 0;
-    for (; j < ts.size() && ts[j] != t; j++);
+    for (; j < ts.size() && ts[j] != t; j++) ;
     assert(j < ts.size());
     for (; j < ts.size()-1; j++) ts[j] = ts[j+1];
     ts.pop();
@@ -205,7 +205,7 @@ template<class V, class T>
 bool find(V& ts, const T& t)
 {
     int j = 0;
-    for (; j < ts.size() && ts[j] != t; j++);
+    for (; j < ts.size() && ts[j] != t; j++) ;
     return j < ts.size();
 }
 
@@ -251,5 +251,5 @@ template <class T> static inline bool operator >= (const T& x, const T& y) { ret
 
 
 //=================================================================================================
-};
+}
 #endif
diff --git a/stp/sat/Heap.h b/stp/sat/Heap.h
index acfa1c1e..e3a82dd0 100644
--- a/stp/sat/Heap.h
+++ b/stp/sat/Heap.h
@@ -147,5 +147,5 @@ class Heap {
 };
 
 //=================================================================================================
-};
+}
 #endif
diff --git a/stp/sat/Simplifier.cpp b/stp/sat/Simplifier.cpp
index 1c192e20..2e709066 100644
--- a/stp/sat/Simplifier.cpp
+++ b/stp/sat/Simplifier.cpp
@@ -539,4 +539,4 @@ bool Solver::eliminate()
 
     return true;
 }
-};
+}
diff --git a/stp/sat/Solver.cpp b/stp/sat/Solver.cpp
index 0fcb6149..13a9ae08 100644
--- a/stp/sat/Solver.cpp
+++ b/stp/sat/Solver.cpp
@@ -316,7 +316,7 @@ void Solver::analyze(Clause* confl, vec<Lit>& out_learnt, int& out_btlevel)
         }
 
         // Select next clause to look at:
-        while (!seen[var(trail[index--])]);
+        while (!seen[var(trail[index--])]) ;
         p     = trail[index+1];
         confl = reason[var(p)];
         seen[var(p)] = 0;
@@ -808,4 +808,4 @@ bool Solver::solve(const vec<Lit>& assumps)
     cancelUntil(0);
     return status == l_True;
 }
-};//end of MINISAT namespace
+} //end of MINISAT namespace
diff --git a/stp/sat/Solver.h b/stp/sat/Solver.h
index 829194cc..8826fac7 100644
--- a/stp/sat/Solver.h
+++ b/stp/sat/Solver.h
@@ -355,5 +355,5 @@ static inline int64 memUsed(void) {
 #endif
 
 //=================================================================================================
-};
+}
 #endif
diff --git a/stp/sat/SolverTypes.h b/stp/sat/SolverTypes.h
index 90e7a9bd..29c3b95d 100644
--- a/stp/sat/SolverTypes.h
+++ b/stp/sat/SolverTypes.h
@@ -124,5 +124,5 @@ class TrailPos {
     bool operator <   (TrailPos other) const { return tp <  other.tp; }
 };
 
-};
+}
 #endif
diff --git a/stp/sat/Sort.h b/stp/sat/Sort.h
index a7011edb..9def2990 100644
--- a/stp/sat/Sort.h
+++ b/stp/sat/Sort.h
@@ -129,5 +129,5 @@ template <class T> void sortUnique(vec<T>& v) {
 
 
 //=================================================================================================
-};
+}
 #endif
diff --git a/stp/sat/VarOrder.h b/stp/sat/VarOrder.h
index 6ad1bfb1..6d2a40f0 100644
--- a/stp/sat/VarOrder.h
+++ b/stp/sat/VarOrder.h
@@ -142,5 +142,5 @@ namespace MINISAT {
   
   
   //=================================================================================================
-};
+}
 #endif
diff --git a/stp/simplifier/bvsolver.cpp b/stp/simplifier/bvsolver.cpp
index 1c08f30b..369251db 100644
--- a/stp/simplifier/bvsolver.cpp
+++ b/stp/simplifier/bvsolver.cpp
@@ -711,4 +711,4 @@ namespace BEEV {
     UpdateAlreadySolvedMap(input,output);
     return output;
   } //end of BVSolve_Even()
-};//end of namespace BEEV
+} //end of namespace BEEV
diff --git a/stp/simplifier/bvsolver.h b/stp/simplifier/bvsolver.h
index a8981b12..8df32042 100644
--- a/stp/simplifier/bvsolver.h
+++ b/stp/simplifier/bvsolver.h
@@ -131,4 +131,4 @@ namespace BEEV {
     //equation to be solved, solves them,
     ASTNode TopLevelBVSolve(const ASTNode& a);
   }; //end of class bvsolver
-};//end of namespace BEEV
+} //end of namespace BEEV
diff --git a/stp/simplifier/simplifier.cpp b/stp/simplifier/simplifier.cpp
index 2a627398..c0519e83 100644
--- a/stp/simplifier/simplifier.cpp
+++ b/stp/simplifier/simplifier.cpp
@@ -2492,4 +2492,4 @@ namespace BEEV {
     TermsAlreadySeenMap[term] = var;
     return false;
   }
-};//end of namespace
+} //end of namespace