clang format

smackers · Oct 19, 2024 · f18245d · f18245d
1 parent e04fceb
commit f18245d
Show file tree

Hide file tree

Showing 5 changed files with 189 additions and 131 deletions.
diff --git a/examples/equivalence/trunc.c b/examples/equivalence/trunc.c
@@ -1,8 +1,10 @@
 #include "smack.h"
 
-double c_trunc(double x)
-{
-  union {double f; unsigned long i;} u = {x};
+double c_trunc(double x) {
+  union {
+    double f;
+    unsigned long i;
+  } u = {x};
   __VERIFIER_equiv_store_unsigned_long(u.i, 0);
   int e = (int)(u.i >> 52 & 0x7ff) - 0x3ff + 12;
   unsigned long m;

diff --git a/lib/smack/Naming.cpp b/lib/smack/Naming.cpp
@@ -43,7 +43,6 @@ const std::string Naming::LOOP_EXIT = "__SMACK_loop_exit";
 const std::string Naming::EQUIV_STORE_COUNTER = "__SMACK_equiv_store_counter";
 const std::string Naming::EQUIV_LOAD_COUNTER = "__SMACK_equiv_load_counter";
 
-
 const std::string Naming::MEMORY = "$M";
 const std::string Naming::ALLOC = "$alloc";
 const std::string Naming::FREE = "$free";

diff --git a/lib/smack/SmackModuleGenerator.cpp b/lib/smack/SmackModuleGenerator.cpp
@@ -38,10 +38,12 @@ void SmackModuleGenerator::generateProgram(llvm::Module &M) {
   SmackRep rep(&M.getDataLayout(), &naming, program, &getAnalysis<Regions>());
   std::list<Decl *> &decls = program->getDeclarations();
 
-  decls.insert(decls.end(), {Decl::variable(Naming::EQUIV_STORE_COUNTER, "int"),
-                             Decl::variable(Naming::EQUIV_LOAD_COUNTER, "int")});
+  decls.insert(decls.end(),
+               {Decl::variable(Naming::EQUIV_STORE_COUNTER, "int"),
+                Decl::variable(Naming::EQUIV_LOAD_COUNTER, "int")});
 
-  decls.insert(decls.end(), {Decl::function("__SMACK_equiv_id", {{"id", "int"}}, "int")});
+  decls.insert(decls.end(),
+               {Decl::function("__SMACK_equiv_id", {{"id", "int"}}, "int")});
 
   SDEBUG(errs() << "Analyzing globals...\n");
 

diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp
@@ -1244,10 +1244,10 @@ Decl *SmackRep::getInitFuncs() {
     b->addStmt(
         Stmt::assign(Expr::id(Naming::RMODE_VAR), Expr::lit(RModeKind::RNE)));
   }
-  b->addStmt(
-      Stmt::assign(Expr::id(Naming::EQUIV_STORE_COUNTER), Expr::lit((unsigned int) 0)));
-        b->addStmt(
-      Stmt::assign(Expr::id(Naming::EQUIV_LOAD_COUNTER), Expr::lit((unsigned int) 0)));
+  b->addStmt(Stmt::assign(Expr::id(Naming::EQUIV_STORE_COUNTER),
+                          Expr::lit((unsigned int)0)));
+  b->addStmt(Stmt::assign(Expr::id(Naming::EQUIV_LOAD_COUNTER),
+                          Expr::lit((unsigned int)0)));
   b->addStmt(Stmt::return_());
   proc->getBlocks().push_back(b);
   return proc;