Fixed formatting since we updated clang-format

Author: zvonimir

include/smack/BoogieAst.h

@@ -680,6 +680,6 @@ std::ostream &operator<<(std::ostream &os, const Expr *e);
 
 std::ostream &operator<<(std::ostream &os, Decl &e);
 std::ostream &operator<<(std::ostream &os, Decl *e);
-}
+} // namespace smack
 
 #endif // BOOGIEAST_H

include/smack/BplFilePrinter.h

@@ -23,6 +23,6 @@ class BplFilePrinter : public llvm::ModulePass {
 
   virtual void getAnalysisUsage(llvm::AnalysisUsage &AU) const;
 };
-}
+} // namespace smack
 
 #endif // BPLPRINTER_H

include/smack/BplPrinter.h

@@ -17,6 +17,6 @@ class BplPrinter : public llvm::ModulePass {
   virtual bool runOnModule(llvm::Module &m);
   virtual void getAnalysisUsage(llvm::AnalysisUsage &AU) const;
 };
-}
+} // namespace smack
 
 #endif // BPLPRINTER_H

include/smack/CodifyStaticInits.h

@@ -20,4 +20,4 @@ class CodifyStaticInits : public llvm::ModulePass {
   virtual bool runOnModule(llvm::Module &M);
   virtual void getAnalysisUsage(llvm::AnalysisUsage &AU) const;
 };
-}
+} // namespace smack

include/smack/Contracts.h

@@ -33,4 +33,4 @@ class ContractsExtractor : public InstVisitor<ContractsExtractor> {
     return ConstantInt::get(Type::getInt32Ty(ctx), slices.size());
   }
 };
-}
+} // namespace smack

include/smack/DSAWrapper.h

@@ -17,7 +17,7 @@ class DSGraph;
 class TDDataStructures;
 class BUDataStructures;
 class DSNodeEquivs;
-}
+} // namespace llvm
 
 namespace dsa {
 template <class dsa> struct TypeSafety;
@@ -74,6 +74,6 @@ class DSAWrapper : public llvm::ModulePass {
   const llvm::DSNode *getNode(const llvm::Value *v);
   void printDSAGraphs(const char *Filename);
 };
-}
+} // namespace smack
 
 #endif // DSAWRAPPER_H

include/smack/ExtractContracts.h

@@ -16,4 +16,4 @@ class ExtractContracts : public ModulePass {
   virtual bool runOnModule(Module &M);
   virtual void getAnalysisUsage(AnalysisUsage &AU) const;
 };
-}
+} // namespace smack

include/smack/IntegerOverflowChecker.h

@@ -32,6 +32,6 @@ class IntegerOverflowChecker : public llvm::ModulePass {
   void addBlockingAssume(llvm::Function *va, llvm::Value *flag,
                          llvm::Instruction *i);
 };
-}
+} // namespace smack
 
 #endif // INTEGEROVERFLOWCHECKER_H

include/smack/MemorySafetyChecker.h

@@ -35,6 +35,6 @@ class MemorySafetyChecker : public llvm::FunctionPass,
   void visitMemSetInst(llvm::MemSetInst &I);
   void visitMemTransferInst(llvm::MemTransferInst &I);
 };
-}
+} // namespace smack
 
 #endif // MEMORYSAFETYCHECKER_H

include/smack/Naming.h

@@ -116,6 +116,6 @@ class Naming {
   static bool isSmackGeneratedName(std::string s);
   static std::string escape(std::string s);
 };
-}
+} // namespace smack
 
 #endif

include/smack/NormalizeLoops.h

@@ -19,6 +19,6 @@ class NormalizeLoops : public llvm::ModulePass {
   virtual bool runOnModule(llvm::Module &m) override;
   virtual void getAnalysisUsage(llvm::AnalysisUsage &) const override;
 };
-}
+} // namespace smack
 
 #endif // NORMALIZELOOPS_H

include/smack/Prelude.h

@@ -215,6 +215,6 @@ class Prelude {
   FuncDecl *unsafeStore(Binding elemBinding, const Expr *body,
                         bool bytes = true);
 };
-}
+} // namespace smack
 
 #endif // PRELUDE_H

include/smack/Regions.h

@@ -92,6 +92,6 @@ class Regions : public ModulePass, public InstVisitor<Regions> {
   void visitMemIntrinsic(MemIntrinsic &);
   void visitCallInst(CallInst &);
 };
-}
+} // namespace smack
 
 #endif // REGIONS_H

include/smack/RemoveDeadDefs.h

@@ -18,4 +18,4 @@ class RemoveDeadDefs : public llvm::ModulePass {
   RemoveDeadDefs() : llvm::ModulePass(ID) {}
   virtual bool runOnModule(llvm::Module &M);
 };
-}
+} // namespace smack

include/smack/SimplifyLibCalls.h

@@ -25,4 +25,4 @@ class SimplifyLibCalls : public ModulePass,
   virtual bool runOnModule(Module &M);
   void visitCallInst(CallInst &);
 };
-}
+} // namespace smack

include/smack/Slicing.h

@@ -40,6 +40,6 @@ class Slice {
   const Decl *getBoogieDecl(Naming *naming, SmackRep *rep);
   const Expr *getBoogieExpression(Naming *naming, SmackRep *rep);
 };
-}
+} // namespace smack
 
 #endif

include/smack/SmackInstGenerator.h

@@ -98,6 +98,6 @@ class SmackInstGenerator : public llvm::InstVisitor<SmackInstGenerator> {
   void visitMemSetInst(llvm::MemSetInst &i);
   void visitIntrinsicInst(llvm::IntrinsicInst &i);
 };
-}
+} // namespace smack
 
 #endif // SMACKINSTVISITOR_H

include/smack/SmackModuleGenerator.h

@@ -23,6 +23,6 @@ class SmackModuleGenerator : public llvm::ModulePass {
   void generateProgram(llvm::Module &m);
   Program *getProgram() { return program; }
 };
-}
+} // namespace smack
 
 #endif // SMACKMODULEGENERATOR_H

include/smack/SmackOptions.h

@@ -32,6 +32,6 @@ class SmackOptions {
 
   static bool isEntryPoint(std::string);
 };
-}
+} // namespace smack
 
 #endif // SMACKREP_H

include/smack/SmackRep.h

@@ -197,6 +197,6 @@ class SmackRep {
   std::string opName(const std::string &operation,
                      std::list<const llvm::Type *> types);
 };
-}
+} // namespace smack
 
 #endif // SMACKREP_H

include/smack/SmackWarnings.h

@@ -50,6 +50,6 @@ class SmackWarnings {
   static bool isSufficientWarningLevel(WarningLevel level);
   static std::string getFlagStr(UnsetFlagsT flags);
 };
-}
+} // namespace smack
 
 #endif // SMACKWARNINGS_H

include/smack/SplitAggregateValue.h

@@ -36,4 +36,4 @@ class SplitAggregateValue : public llvm::BasicBlockPass {
                                    std::vector<InfoT> &info, llvm::Value *V);
   bool isConstantAggregate(llvm::Value *V);
 };
-}
+} // namespace smack

include/smack/VectorOperations.h

@@ -41,6 +41,6 @@ class VectorOperations {
   FuncDecl *load(const Value *V);
   FuncDecl *store(const Value *V);
 };
-}
+} // namespace smack
 
 #endif // VECTOROPERATIONS_H

include/smack/VerifierCodeMetadata.h

@@ -26,4 +26,4 @@ class VerifierCodeMetadata : public ModulePass,
   void visitInstruction(Instruction &);
   static bool isMarked(const Instruction &I);
 };
-}
+} // namespace smack

lib/smack/BoogieAst.cpp

@@ -685,4 +685,4 @@ void Program::print(std::ostream &os) const {
   print_seq<Decl *>(os, decls, "\n");
   os << "\n";
 }
-}
+} // namespace smack

lib/smack/BplFilePrinter.cpp

@@ -28,4 +28,4 @@ bool BplFilePrinter::runOnModule(llvm::Module &m) {
   // DEBUG_WITH_TYPE("bpl", errs() << "" << s.str());
   return false;
 }
-}
+} // namespace smack

lib/smack/BplPrinter.cpp

@@ -28,4 +28,4 @@ bool BplPrinter::runOnModule(llvm::Module &m) {
   DEBUG_WITH_TYPE("bpl", errs() << "" << s.str());
   return false;
 }
-}
+} // namespace smack

lib/smack/CodifyStaticInits.cpp

@@ -28,8 +28,8 @@ bool CodifyStaticInits::runOnModule(Module &M) {
   LLVMContext &C = M.getContext();
   DSAWrapper *DSA = &getAnalysis<DSAWrapper>();
 
-  Function *F = dyn_cast<Function>(M.getOrInsertFunction(
-      Naming::STATIC_INIT_PROC, Type::getVoidTy(C)));
+  Function *F = dyn_cast<Function>(
+      M.getOrInsertFunction(Naming::STATIC_INIT_PROC, Type::getVoidTy(C)));
 
   BasicBlock *B = BasicBlock::Create(C, "entry", F);
   IRBuilder<> IRB(B);
@@ -101,4 +101,4 @@ char CodifyStaticInits::ID = 0;
 // Register the pass
 static RegisterPass<CodifyStaticInits> X("codify-static-inits",
                                          "Codify Static Initializers");
-}
+} // namespace smack

lib/smack/Contracts.cpp

@@ -93,4 +93,4 @@ void ContractsExtractor::visitCallInst(CallInst &ci) {
     head->getInstList().insert(I, &ci);
   }
 }
-}
+} // namespace smack

lib/smack/Debug.cpp

@@ -36,7 +36,7 @@ void setCurrentDebugTypes(const char **Types, unsigned Count) {
   for (size_t T = 0; T < Count; ++T)
     CurrentDebugType->push_back(Types[T]);
 }
-}
+} // namespace smack
 
 #ifndef NDEBUG
 
@@ -57,13 +57,14 @@ struct DebugOnlyOpt {
       CurrentDebugType->push_back(dbgType);
   }
 };
-}
+} // namespace
 
 static DebugOnlyOpt DebugOnlyOptLoc;
 
 static ::llvm::cl::opt<DebugOnlyOpt, true, cl::parser<std::string>>
-    DebugOnly("debug-only", cl::desc("Enable a specific type of debug output "
-                                     "(comma separated list of types)"),
+    DebugOnly("debug-only",
+              cl::desc("Enable a specific type of debug output "
+                       "(comma separated list of types)"),
               cl::Hidden, cl::ZeroOrMore, cl::value_desc("debug string"),
               cl::location(DebugOnlyOptLoc), cl::ValueRequired);
 
@@ -80,6 +81,6 @@ raw_ostream &smack::dbgs() {
 #else
 namespace smack {
 raw_ostream &dbgs() { return llvm::errs(); }
-}
+} // namespace smack
 
 #endif

lib/smack/ExtractContracts.cpp

@@ -204,7 +204,7 @@ std::vector<std::tuple<Function *, Function *>> getContractExprs(Function &F) {
   }
   return Fs;
 }
-}
+} // namespace
 
 bool ExtractContracts::runOnModule(Module &M) {
   bool modified = false;
@@ -303,4 +303,4 @@ char ExtractContracts::ID = 0;
 // Register the pass
 static RegisterPass<ExtractContracts> X("extract-contracts",
                                         "Extract Contracts");
-}
+} // namespace smack

lib/smack/IntegerOverflowChecker.cpp

@@ -222,4 +222,4 @@ char IntegerOverflowChecker::ID = 0;
 StringRef IntegerOverflowChecker::getPassName() const {
   return "Checked integer arithmetic intrinsics";
 }
-}
+} // namespace smack

lib/smack/MemorySafetyChecker.cpp

@@ -92,7 +92,7 @@ Value *accessSizeAsPointer(StoreInst &I) {
   auto &M = *I.getParent()->getParent()->getParent();
   return accessSizeAsPointer(M, I.getPointerOperand());
 }
-}
+} // namespace
 
 void MemorySafetyChecker::visitLoadInst(LoadInst &I) {
   insertMemoryAccessCheck(I.getPointerOperand(), accessSizeAsPointer(I), &I);
@@ -113,4 +113,4 @@ void MemorySafetyChecker::visitMemTransferInst(MemTransferInst &I) {
 
 // Pass ID variable
 char MemorySafetyChecker::ID = 0;
-}
+} // namespace smack

lib/smack/Naming.cpp

@@ -267,4 +267,4 @@ std::string Naming::freshVarName(const Value &V) {
   s << varNum++;
   return s.str();
 }
-}
+} // namespace smack

lib/smack/NormalizeLoops.cpp

@@ -158,4 +158,4 @@ bool NormalizeLoops::runOnModule(Module &m) {
 char NormalizeLoops::ID = 0;
 
 StringRef NormalizeLoops::getPassName() const { return "NormalizeLoops"; }
-}
+} // namespace smack

lib/smack/Prelude.cpp

@@ -367,14 +367,17 @@ void IntOpGen::generateArithOps(std::stringstream &s) const {
   const auto intBuiltinOp = new BuiltinOp<IntOp::attrT>(IntOp::intAttrFunc);
   const auto uninterpretedOp = new UninterpretedOp();
   const std::vector<IntOpGen::IntArithOp> intArithOpTable{
-      {"add", 2, new InlinedOp<IntOp::exprT>(
-                     IntOpGen::IntArithOp::intArithExpr<BinExpr::Plus>),
+      {"add", 2,
+       new InlinedOp<IntOp::exprT>(
+           IntOpGen::IntArithOp::intArithExpr<BinExpr::Plus>),
        bvBuiltinOp, true},
-      {"sub", 2, new InlinedOp<IntOp::exprT>(
-                     IntOpGen::IntArithOp::intArithExpr<BinExpr::Minus>),
+      {"sub", 2,
+       new InlinedOp<IntOp::exprT>(
+           IntOpGen::IntArithOp::intArithExpr<BinExpr::Minus>),
        bvBuiltinOp, true},
-      {"mul", 2, new InlinedOp<IntOp::exprT>(
-                     IntOpGen::IntArithOp::intArithExpr<BinExpr::Times>),
+      {"mul", 2,
+       new InlinedOp<IntOp::exprT>(
+           IntOpGen::IntArithOp::intArithExpr<BinExpr::Times>),
        bvBuiltinOp, true},
       {"sdiv", 2, intBuiltinOp, bvBuiltinOp, false},
       {"smod", 2, intBuiltinOp, bvBuiltinOp, false},
@@ -874,9 +877,9 @@ void MemDeclGen::generateGlobalAllocations(std::stringstream &s) const {
 
     std::list<const Stmt *> stmts;
     for (auto E : prelude.rep.globalAllocations)
-      stmts.push_back(Stmt::call(
-          "$galloc",
-          {prelude.rep.expr(E.first), prelude.rep.pointerLit(E.second)}));
+      stmts.push_back(
+          Stmt::call("$galloc", {prelude.rep.expr(E.first),
+                                 prelude.rep.pointerLit(E.second)}));
     s << Decl::procedure("$global_allocations", {}, {}, {},
                          {Block::block("", stmts)})
       << "\n";
@@ -924,9 +927,8 @@ void PtrOpGen::generatePreds(std::stringstream &s) const {
              indexedName(pred, {Naming::PTR_TYPE}),
              {{"p1", Naming::PTR_TYPE}, {"p2", Naming::PTR_TYPE}},
              prelude.rep.intType(1),
-             Expr::cond(Expr::fn(indexedName(pred,
-                                             {prelude.rep.pointerType(),
-                                              Naming::BOOL_TYPE}),
+             Expr::cond(Expr::fn(indexedName(pred, {prelude.rep.pointerType(),
+                                                    Naming::BOOL_TYPE}),
                                  {Expr::id("p1"), Expr::id("p2")}),
                         prelude.rep.integerLit(1LL, 1),
                         prelude.rep.integerLit(0LL, 1)),
@@ -1449,9 +1451,10 @@ void FpOpGen::generateMemOps(std::stringstream &s) const {
         // e.g., function {:inline} $load.unsafe.bvhalf(M: [ref] i8, p: ref)
         // returns (bvhalf) { $bitcast.i16.bvhalf($load.i16(M, p)) }
         s << prelude.unsafeLoad(
-                 type, Expr::fn(indexedName("$bitcast", {intType, type}),
-                                Expr::fn(indexedName("$load", {intType}),
-                                         makeMapVarExpr(0), makePtrVarExpr(0))),
+                 type,
+                 Expr::fn(indexedName("$bitcast", {intType, type}),
+                          Expr::fn(indexedName("$load", {intType}),
+                                   makeMapVarExpr(0), makePtrVarExpr(0))),
                  false)
           << "\n";
         // e.g., function {:inline} $store.unsafe.bvfloat(M: [ref] i8, p: ref,
@@ -1488,10 +1491,9 @@ void FpOpGen::generateMemOps(std::stringstream &s) const {
       // function {:inline} $store.bytes.float(M: [ref] bv8, p: ref, f: float)
       // returns ([ref] bv8) { M[p := $bitcast.float.bv8(f)] }
       s << prelude.unsafeStore(
-               binding,
-               prelude.mapUpdExpr(
-                   0, Expr::fn(indexedName("$bitcast", {type, bvType}),
-                               makeFpVarExpr(0))))
+               binding, prelude.mapUpdExpr(
+                            0, Expr::fn(indexedName("$bitcast", {type, bvType}),
+                                        makeFpVarExpr(0))))
         << "\n";
     } else {
       std::string intType = getIntTypeName(8);