Clang-format

Author: peterschrammel

src/goto-checker/property_checker.cpp

@@ -15,42 +15,44 @@ std::string property_checkert::as_string(resultt result)
 {
   switch(result)
   {
-  case property_checkert::resultt::PASS: return "OK";
-  case property_checkert::resultt::FAIL: return "FAILURE";
-  case property_checkert::resultt::ERROR: return "ERROR";
-  case property_checkert::resultt::UNKNOWN: return "UNKNOWN";
+  case property_checkert::resultt::PASS:
+    return "OK";
+  case property_checkert::resultt::FAIL:
+    return "FAILURE";
+  case property_checkert::resultt::ERROR:
+    return "ERROR";
+  case property_checkert::resultt::UNKNOWN:
+    return "UNKNOWN";
   }
 
   return "";
 }
 
-property_checkert::property_checkert(
-  message_handlert &_message_handler):
-  messaget(_message_handler)
+property_checkert::property_checkert(message_handlert &_message_handler)
+  : messaget(_message_handler)
 {
 }
 
 void property_checkert::initialize_property_map(
   const goto_functionst &goto_functions)
 {
   forall_goto_functions(it, goto_functions)
-    if(!it->second.is_inlined() ||
-       it->first==goto_functions.entry_point())
+    if(!it->second.is_inlined() || it->first == goto_functions.entry_point())
     {
-      const goto_programt &goto_program=it->second.body;
+      const goto_programt &goto_program = it->second.body;
 
       forall_goto_program_instructions(i_it, goto_program)
       {
         if(!i_it->is_assert())
           continue;
 
-        const source_locationt &source_location=i_it->source_location;
+        const source_locationt &source_location = i_it->source_location;
 
-        irep_idt property_id=source_location.get_property_id();
+        irep_idt property_id = source_location.get_property_id();
 
-        property_statust &property_status=property_map[property_id];
-        property_status.result=resultt::UNKNOWN;
-        property_status.location=i_it;
+        property_statust &property_status = property_map[property_id];
+        property_status.result = resultt::UNKNOWN;
+        property_status.location = i_it;
       }
     }
 }

src/goto-checker/property_checker.h

@@ -19,22 +19,27 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/goto_model.h>
 #include <goto-programs/goto_trace.h>
 
-class property_checkert:public messaget
+class property_checkert : public messaget
 {
 public:
   property_checkert()
   {
   }
 
-  explicit property_checkert(
-    message_handlert &_message_handler);
+  explicit property_checkert(message_handlert &_message_handler);
 
-  enum class resultt { PASS, FAIL, ERROR, UNKNOWN };
+  enum class resultt
+  {
+    PASS,
+    FAIL,
+    ERROR,
+    UNKNOWN
+  };
 
   static std::string as_string(resultt);
 
   // Check whether all properties in goto_functions hold.
-  virtual resultt operator()(const goto_modelt &)=0;
+  virtual resultt operator()(const goto_modelt &) = 0;
 
   struct property_statust
   {

src/goto-checker/safety_checker.cpp

@@ -11,15 +11,13 @@ Author: Daniel Kroening, [email protected]
 
 #include "safety_checker.h"
 
-safety_checkert::safety_checkert(const namespacet &_ns):
-  ns(_ns)
+safety_checkert::safety_checkert(const namespacet &_ns) : ns(_ns)
 {
 }
 
 safety_checkert::safety_checkert(
   const namespacet &_ns,
-  message_handlert &_message_handler):
-  messaget(_message_handler),
-  ns(_ns)
+  message_handlert &_message_handler)
+  : messaget(_message_handler), ns(_ns)
 {
 }

src/goto-checker/safety_checker.h

@@ -20,11 +20,10 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/goto_model.h>
 #include <goto-programs/goto_trace.h>
 
-class safety_checkert:public messaget
+class safety_checkert : public messaget
 {
 public:
-  explicit safety_checkert(
-    const namespacet &_ns);
+  explicit safety_checkert(const namespacet &_ns);
 
   explicit safety_checkert(
     const namespacet &_ns,
@@ -51,8 +50,7 @@ class safety_checkert:public messaget
   // check whether all assertions in goto_functions are safe
   // if UNSAFE, then a trace is returned
 
-  virtual resultt operator()(
-    const goto_functionst &goto_functions)=0;
+  virtual resultt operator()(const goto_functionst &goto_functions) = 0;
 
   // this is the counterexample
   goto_tracet error_trace;