compile musketeer

Author: Daniel Kroening

src/musketeer/cycles_visitor.cpp

@@ -30,7 +30,7 @@ class instrumentert;
 \*******************************************************************/
 
 /* po^+ /\ U{C_1, ..., C_n} \/ delays */
-void cycles_visitort::po_edges(std::set<unsigned>& edges)
+void cycles_visitort::po_edges(std::set<event_idt>& edges)
 {
   instrumentert& instrumenter=fence_inserter.instrumenter;
 
@@ -176,7 +176,7 @@ void cycles_visitort::po_edges(std::set<unsigned>& edges)
       /* computes the largest pos+ in C_j */
       std::map<unsigned,event_grapht::critical_cyclet::const_iterator> m_begin;
       std::map<unsigned,event_grapht::critical_cyclet::const_iterator> m_end;
-      std::set<unsigned> m_threads;
+      std::set<event_idt> m_threads;
 
       unsigned previous_thread=0;
       for(event_grapht::critical_cyclet::const_iterator C_j_it=C_j->begin();
@@ -199,7 +199,7 @@ void cycles_visitort::po_edges(std::set<unsigned>& edges)
       /* computes the largest pos+ in C_k */
       std::map<unsigned,event_grapht::critical_cyclet::const_iterator> k_begin;
       std::map<unsigned,event_grapht::critical_cyclet::const_iterator> k_end;
-      std::set<unsigned> k_threads;
+      std::set<event_idt> k_threads;
 
       previous_thread=0;
       for(event_grapht::critical_cyclet::const_iterator C_k_it=C_k->begin();
@@ -220,7 +220,7 @@ void cycles_visitort::po_edges(std::set<unsigned>& edges)
       }
 
       /* if there are some commun threads, take the intersection if relevant */
-      for(std::set<unsigned>::const_iterator it=m_threads.begin();
+      for(std::set<event_idt>::const_iterator it=m_threads.begin();
         it!=m_threads.end(); ++it)
         if(k_threads.find(*it)!=k_threads.end())
         {
@@ -264,7 +264,7 @@ void cycles_visitort::po_edges(std::set<unsigned>& edges)
 /* C_j /\ po^+ /\ poWR */
 void cycles_visitort::powr_constraint(
   const event_grapht::critical_cyclet& C_j,
-  std::set<unsigned>& edges)
+  std::set<event_idt>& edges)
 {
   event_grapht& graph=fence_inserter.instrumenter.egraph;
 
@@ -295,7 +295,7 @@ void cycles_visitort::powr_constraint(
 /* C_j /\ po^+ /\ poWW */
 void cycles_visitort::poww_constraint(
   const event_grapht::critical_cyclet& C_j,
-  std::set<unsigned>& edges)
+  std::set<event_idt>& edges)
 {
   event_grapht& graph=fence_inserter.instrumenter.egraph;
 
@@ -326,7 +326,7 @@ void cycles_visitort::poww_constraint(
 /* C_j /\ po^+ /\ poRW */
 void cycles_visitort::porw_constraint(
   const event_grapht::critical_cyclet& C_j,
-  std::set<unsigned>& edges)
+  std::set<event_idt>& edges)
 {
   event_grapht& graph=fence_inserter.instrumenter.egraph;
 
@@ -357,7 +357,7 @@ void cycles_visitort::porw_constraint(
 /* C_j /\ po^+ /\ poRR */
 void cycles_visitort::porr_constraint(
   const event_grapht::critical_cyclet& C_j,
-  std::set<unsigned>& edges)
+  std::set<event_idt>& edges)
 {
   event_grapht& graph=fence_inserter.instrumenter.egraph;
 
@@ -388,7 +388,7 @@ void cycles_visitort::porr_constraint(
 /* C_j /\ comWR */
 void cycles_visitort::com_constraint(
   const event_grapht::critical_cyclet& C_j,
-  std::set<unsigned>& edges)
+  std::set<event_idt>& edges)
 {
   event_grapht& egraph=fence_inserter.instrumenter.egraph;
 

src/musketeer/cycles_visitor.h

@@ -28,20 +28,20 @@ class cycles_visitort
   {}
 
   /* computes po^+ edges in U{C_1, ..., C_j} */
-  void po_edges(std::set<unsigned>& edges);
+  void po_edges(std::set<event_idt>& edges);
 
   /* computes pairs that will be protected for the
      TSO/PSO/RMO/Power/ARM by the constraints */
   void powr_constraint(const event_grapht::critical_cyclet& C_j,
-    std::set<unsigned>& edges);
+    std::set<event_idt>& edges);
   void poww_constraint(const event_grapht::critical_cyclet& C_j,
-    std::set<unsigned>& edges);
+    std::set<event_idt>& edges);
   void porw_constraint(const event_grapht::critical_cyclet& C_j,
-    std::set<unsigned>& edges);
+    std::set<event_idt>& edges);
   void porr_constraint(const event_grapht::critical_cyclet& C_j,
-    std::set<unsigned>& edges);
+    std::set<event_idt>& edges);
   void com_constraint(const event_grapht::critical_cyclet& C_j,
-    std::set<unsigned>& edges);
+    std::set<event_idt>& edges);
 };
 
 #endif // CPROVER_MUSKETEER_CYCLES_VISITOR_H