Fix/no warnings compilation

src/ebmc/bdd_engine.cpp

@@ -534,7 +534,7 @@ bdd_enginet::BDD bdd_enginet::property2BDD(const exprt &expr)
           expr.id()==ID_sva_overlapped_implication)
   {
     assert(expr.operands().size()==2);
-    return !property2BDD(expr.op0()) | property2BDD(expr.op1());
+    return (!property2BDD(expr.op0())) | property2BDD(expr.op1());
   }
   else if(expr.id()==ID_and)
   {
@@ -556,7 +556,7 @@ bdd_enginet::BDD bdd_enginet::property2BDD(const exprt &expr)
 
     // use sva_nexttime for this
     unary_predicate_exprt tmp(ID_sva_nexttime, expr.op1());
-    return !property2BDD(expr.op0()) | property2BDD(tmp);
+    return (!property2BDD(expr.op0())) | property2BDD(tmp);
   }
   else if(expr.id()==ID_sva_nexttime)
   {

src/ebmc/diameter.cpp

@@ -255,7 +255,7 @@ Function: compare
 
 \*******************************************************************/
 
-#define bool unsigned
+//#define bool unsigned
 #define ASCENDING 1   // sorting direction
 #define DESCENDING 0
 

src/ebmc/ebmc_base.cpp

@@ -480,7 +480,7 @@ int ebmc_baset::do_bmc(prop_convt &solver, bool convert_only)
 {
   solver.set_message_handler(get_message_handler());
 
-  int result;
+  int result=0;
 
   try
   {

src/ic3/Makefile

@@ -1,4 +1,6 @@
-CXXFLAGS = -Wno-literal-suffix -Wno-write-strings -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS -O3 $(INC_DIR)
+
+CXXFLAGS = -std=c++0x -Wno-write-strings -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS -O3 $(INC_DIR)
+
 CXFLAGS = $(INC_DIR)
 CFLAGS =   -O3  $(INC_DIR) 
 CXX = g++

src/ic3/aux_types.hh

@@ -8,6 +8,14 @@ Author: Eugene Goldberg, [email protected]
 
 #include <string>
 
+#ifndef UNUSED
+#ifdef _MSC_VER
+#define UNUSED
+#else
+#define UNUSED __attribute__((unused))
+#endif
+#endif
+
 typedef std::pair<CUBE,int> StatePair;
 typedef std::pair<int,int> LenInd;
 typedef std::pair<float,int> ActInd;
@@ -61,7 +69,7 @@ public:
   void hsh_init(int nelems);
   void clean();
   void add_elem(void);
-  int size();
+  size_t size();
   void started_using(void);
   void done_using(void);
 }; 
@@ -117,7 +125,7 @@ typedef std::priority_queue<PqElem,std::vector <PqElem>, pq_compare> PrQueue;
 
 struct ClauseInfo 
 {  
-  int  span;    // specifies the span of cube. If span = j, F_j is the latest
+  size_t  span;    // specifies the span of cube. If span = j, F_j is the latest
                 // formula where  the clause at hand is present
   unsigned active : 1; // is set to 0 if clause C=F[curr_ind] is strictly 
                        //subsumed by a clause obtained after pushing clause C 

src/ic3/build_prob/assign_indexes.cc

@@ -52,7 +52,7 @@ void CompInfo::form_property_gates(CUBE &Gates)
     Gates.push_back(gt_ind);
 
 
-    for (int i=0; i < G.Fanin_list.size();i++)  {
+    for (size_t i=0; i < G.Fanin_list.size();i++)  {
       int fanin_ind = G.Fanin_list[i];
       Buffer.push_back(fanin_ind);
     }
@@ -73,7 +73,7 @@ void find_latch(Circuit *N,Gate &G,int &latch_ind)
 {
 
 
-  for (int i=0; i < G.Fanout_list.size();i++) {
+  for (size_t i=0; i < G.Fanout_list.size();i++) {
     int gate_ind = G.Fanout_list[i];
     Gate &G1 = N->get_gate(gate_ind);
     if (G1.gate_type == LATCH) {
@@ -96,8 +96,7 @@ void CompInfo::assign_var_indexes()
 
   Gate_to_var.assign(N->Gate_list.size(),-1);
   int curr_index = 1;
-  for (int i=0; i < N->Gate_list.size();i++) {
-    Gate &G = N->get_gate(i);
+  for (size_t i=0; i < N->Gate_list.size();i++) {
     Gate_to_var[i]=curr_index++;
   }
 

src/ic3/build_prob/build_arrays.cc

@@ -25,7 +25,7 @@ Author: Eugene Goldberg, [email protected]
 ===========================================*/
 void CompInfo::form_inp_vars()
 {
-  for (int i=0; i < N->Inputs.size();i++) {
+  for (size_t i=0; i < N->Inputs.size();i++) {
     int gate_ind = N->Inputs[i];
     int var = Gate_to_var[gate_ind];      
     Inp_vars.push_back(var);
@@ -41,7 +41,7 @@ void CompInfo::form_inp_vars()
 ===============================================*/
 void CompInfo::form_pres_state_vars()
 {
-  for (int i=0; i < N->Gate_list.size();i++) {
+  for (size_t i=0; i < N->Gate_list.size();i++) {
     Gate &G = N->get_gate(i);
     if (G.gate_type != LATCH) continue;
     int var = Gate_to_var[i];      
@@ -59,7 +59,7 @@ void CompInfo::form_pres_state_vars()
 void CompInfo::form_next_state_vars()
 {
 
-  for (int i=0; i < N->Gate_list.size();i++) {
+  for (size_t i=0; i < N->Gate_list.size();i++) {
      Gate &G = N->get_gate(i);
       if (G.flags.feeds_latch == 0) continue;
       int var = Gate_to_var[i];      
@@ -79,7 +79,7 @@ void CompInfo::form_next_to_pres_conv()
 
   CUBE Pairs;
 
-  for (int i=0; i < N->Gate_list.size();i++) {
+  for (size_t i=0; i < N->Gate_list.size();i++) {
     Gate &G = N->get_gate(i);
     if (G.flags.feeds_latch == 0) continue;
     int next_var = Gate_to_var[i]; 
@@ -104,7 +104,7 @@ void CompInfo::form_pres_to_next_conv()
 
   CUBE Pairs;
 
-  for (int i=0; i < N->Gate_list.size();i++) {
+  for (size_t i=0; i < N->Gate_list.size();i++) {
     Gate &G = N->get_gate(i);
     if (G.flags.feeds_latch == 0) continue;
     int next_var = Gate_to_var[i]; 

src/ic3/build_prob/g0en_cnf.cc

@@ -24,14 +24,9 @@ int debug_flag=0;
   G E N _ C N F S
 
   =====================*/
-void  CompInfo::gen_cnfs(char *fname,bool print_flag)
+void  CompInfo::gen_cnfs(const char *fname,bool print_flag)
 {  
-  int total_ngates = N->Gate_list.size();  
-  int shift = total_ngates - N->nlatches; // we subtract latches
-
   assign_var_indexes();
-
-
 
   char fname1[MAX_NAME];
 
@@ -62,7 +57,7 @@ void  CompInfo::add_last_cube(DNF &F)
 {
   // find the output gate
   int gate_ind=-1;
-  for (int i=0; i < N->Gate_list.size(); i++) {
+  for (size_t i=0; i < N->Gate_list.size(); i++) {
     Gate &G =  N->Gate_list[i];
     if (G.flags.output == 1) {
       gate_ind = i;
@@ -85,9 +80,7 @@ void  CompInfo::add_last_cube(DNF &F)
   =========================*/
 void CompInfo::gen_out_fun(DNF &H,int shift,bool short_version)
 {
-
-  int count = 0;
-  for (int i=0; i < N->Gate_list.size();i++) {
+  for (size_t i=0; i < N->Gate_list.size();i++) {
     int gate_ind = Ordering[i];
     Gate &G =  N->Gate_list[gate_ind];
     if (G.gate_type == INPUT) continue;
@@ -98,7 +91,6 @@ void CompInfo::gen_out_fun(DNF &H,int shift,bool short_version)
     if (short_version)
 // skip the gates that are shared by transition relation and out function
       if (G.flags.transition) continue; 
-    int var_ind = Gate_to_var[gate_ind]-1;
     switch (G.func_type)
       {case CONST:
 	  add_const_gate_cube(H,gate_ind,shift);
@@ -137,7 +129,7 @@ void CompInfo::gen_out_fun(DNF &H,int shift,bool short_version)
   ====================================================*/
 void  CompInfo::gen_initial_state_cubes()
 {
-  for (int i=0; i < N->Latches.size();i++) {
+  for (size_t i=0; i < N->Latches.size();i++) {
     int gate_ind = N->Latches[i];
     Gate &G = N->get_gate(gate_ind);
     assert(G.gate_type == LATCH);
@@ -151,7 +143,7 @@ void  CompInfo::gen_initial_state_cubes()
       break;
     case 2:
       break;
-    defaul:
+    default:
       assert(false);
     }
     if (C.size() > 0) 
@@ -199,7 +191,7 @@ void CompInfo::add_buffer_gate_cubes(DNF &F,int gate_ind,int shift)
   Gate &G = N->Gate_list[gate_ind];
 
 
-  for (int i=0; i < G.Fanin_list.size();i++) {
+  for (size_t i=0; i < G.Fanin_list.size();i++) {
     int gate_ind1 =  G.Fanin_list[i];
     int var_ind = Gate_to_var[gate_ind1];
     var_indexes.push_back(var_ind);

src/ic3/build_prob/g1en_cnf.cc

@@ -48,7 +48,7 @@ void  CompInfo::add_or_gate_cubes(DNF &F,int gate_ind,int shift)
   Gate &G =  N->Gate_list[gate_ind];
 
 
-  for (int i=0; i < G.Fanin_list.size();i++) {
+  for (size_t i=0; i < G.Fanin_list.size();i++) {
     int gate_ind1 = G.Fanin_list[i];
     int var_ind = Gate_to_var[gate_ind1];
     var_indexes.push_back(var_ind);
@@ -62,7 +62,7 @@ void  CompInfo::add_or_gate_cubes(DNF &F,int gate_ind,int shift)
   // generate the long clause
   //
   CUBE C;
-  for (int i=0; i <  G.Fanin_list.size();i++)
+  for (size_t i=0; i <  G.Fanin_list.size();i++)
     if (G.Polarity[i] == 0)   C.push_back(var_indexes[i]+shift); 
     else C.push_back(-(var_indexes[i]+shift)); 
   C.push_back(-(var_indexes.back()+shift));
@@ -73,7 +73,7 @@ void  CompInfo::add_or_gate_cubes(DNF &F,int gate_ind,int shift)
   //  generate short claueses
   //
   //
-  for (int i=0; i < G.Fanin_list.size();i++)
+  for (size_t i=0; i < G.Fanin_list.size();i++)
     {C.clear();
       if (G.Polarity[i] == 0)   C.push_back(-(var_indexes[i]+shift)); 
       else C.push_back(var_indexes[i]+shift); 
@@ -97,7 +97,7 @@ void CompInfo::add_and_gate_cubes(DNF &F,int gate_ind,int shift)
   CUBE var_indexes;
   Gate &G =  N->Gate_list[gate_ind];
 
-  for (int i=0; i < G.Fanin_list.size();i++) {
+  for (size_t i=0; i < G.Fanin_list.size();i++) {
     int gate_ind1 = G.Fanin_list[i];
     int var_ind = Gate_to_var[gate_ind1];
     var_indexes.push_back(var_ind);
@@ -111,7 +111,7 @@ void CompInfo::add_and_gate_cubes(DNF &F,int gate_ind,int shift)
   // generate the long clause
   //
   CUBE C;
-  for (int i=0; i < G.Fanin_list.size();i++)
+  for (size_t i=0; i < G.Fanin_list.size();i++)
     if (G.Polarity[i] == 0)   C.push_back(-(var_indexes[i]+shift)); 
     else C.push_back(var_indexes[i]+shift); 
   C.push_back(var_indexes.back()+shift);
@@ -122,7 +122,7 @@ void CompInfo::add_and_gate_cubes(DNF &F,int gate_ind,int shift)
   //  generate short claueses
   //
   //
-  for (int i=0; i < G.Fanin_list.size();i++) {
+  for (size_t i=0; i < G.Fanin_list.size();i++) {
     C.clear();
     if (G.Polarity[i] == 0)   C.push_back(var_indexes[i]+shift); 
     else C.push_back(-(var_indexes[i]+shift)); 
@@ -146,7 +146,7 @@ void  CompInfo::add_truth_table_gate_cubes(DNF &F,int gate_ind,int shift)
   Gate &G =  N->Gate_list[gate_ind];
 
 
-  for (int i=0; i < G.Fanin_list.size();i++) {
+  for (size_t i=0; i < G.Fanin_list.size();i++) {
     int gate_ind1 = G.Fanin_list[i];
     int var_ind = Gate_to_var[gate_ind1];
     var_indexes.push_back(var_ind);
@@ -156,20 +156,20 @@ void  CompInfo::add_truth_table_gate_cubes(DNF &F,int gate_ind,int shift)
   var_indexes.push_back(Gate_to_var[gate_ind]);
 
   CUBE TT(1 << G.ninputs);
-  for (int i=0; i < TT.size(); i++)
+  for (size_t i=0; i < TT.size(); i++)
     TT[i] = 0;
 
   DNF &D = G.F;
-  for (int i=0; i < D.size(); i++) {
+  for (size_t i=0; i < D.size(); i++) {
     int index=form_index(D[i]);
     TT[index] = 1;
   }
 
   // form the cubes describing the ON-set
-  for (int i=0; i < D.size();i++) {
+  for (size_t i=0; i < D.size();i++) {
     CUBE &C = D[i];
     CUBE C1;
-    for (int j=0; j < C.size(); j++) {
+    for (size_t j=0; j < C.size(); j++) {
       C1.push_back(var_indexes[abs(C[j])-1]+shift);
       if (C[j] > 0) C1[j] = -C1[j];
     }
@@ -179,11 +179,11 @@ void  CompInfo::add_truth_table_gate_cubes(DNF &F,int gate_ind,int shift)
 
   // form the cubes describing the OFF-set
 
-  for (int i=0; i < TT.size(); i++)
+  for (size_t i=0; i < TT.size(); i++)
     {CUBE C,C1;
       if (TT[i] == 1) continue;
       make_cube(i,G.ninputs,C);
-      for (int j=0; j < C.size(); j++)
+      for (size_t j=0; j < C.size(); j++)
 	{C1.push_back(var_indexes[abs(C[j])-1]+shift);
 	  if (C[j] >  0) C1[j] = -C1[j];
 	}

src/ic3/build_prob/g2en_cnf.cc

@@ -26,7 +26,7 @@ void CompInfo::add_constrs()
 {
   printf("adding %d unit constraints\n",(int) (Constr_ilits.size() +
 					       Constr_nilits.size()));
-  for (int i=0; i < Constr_ilits.size(); i++) {
+  for (size_t i=0; i < Constr_ilits.size(); i++) {
     CLAUSE U;
     U.push_back(Constr_ilits[i]);
     Tr.push_back(U);
@@ -53,7 +53,7 @@ void CompInfo::add_constrs()
 bool empty_cube(CUBE &C)
 {SCUBE Lits;
 
-  for (int i=0; i < C.size(); i++) {
+  for (size_t i=0; i < C.size(); i++) {
     if (Lits.find(-C[i]) != Lits.end())
       return(true); // empty cube
     Lits.insert(C[i]);
@@ -71,7 +71,7 @@ bool empty_cube(CUBE &C)
 int form_index(CUBE &C)
 {
   int result = 0;
-  for (int i=0; i < C.size();i++)
+  for (size_t i=0; i < C.size();i++)
     {assert(abs(C[i]) == i+1);
       if (C[i] > 0)  result |= 1 << i;
     }
@@ -91,15 +91,14 @@ int form_index(CUBE &C)
 void CompInfo::gen_trans_rel(int shift)
 {
 
-  for (int i=0; i < N->Gate_list.size();i++) {
+  for (size_t i=0; i < N->Gate_list.size();i++) {
     int gate_ind = Ordering[i];
     Gate &G =  N->Gate_list[gate_ind];
     if (G.gate_type == INPUT) continue;
     if (G.gate_type == LATCH) continue;
 // skip the gates that are not part of the transition function
     if (G.flags.transition == 0) 
       if (G.flags.tran_constr == 0) continue; 
-    int var_ind = Gate_to_var[gate_ind]-1;
     switch (G.func_type)
       {case CONST:
 	  add_const_gate_cube(Tr,gate_ind,shift);
@@ -146,11 +145,11 @@ void CompInfo::print_var_indexes(char *fname)
   marked_vars.assign(2*N->Gate_list.size(),0);
 
    // print var indexes in topological order
-   for (int i=0; i <= N->max_levels; i++)
+   for (size_t i=0; i <= N->max_levels; i++)
      {fprintf(fp,"--------------------------------------\n");
-       fprintf(fp,"topological level %d\n",i);
+       fprintf(fp,"topological level %zu\n",i);
       CUBE &Gates = topol_levels[i];
-      for (int j=0; j < Gates.size(); j++)
+      for (size_t j=0; j < Gates.size(); j++)
 	{int gate_ind = Gates[j];
 	 Gate &G = N->get_gate(gate_ind);
          switch (G.gate_type)
@@ -183,7 +182,7 @@ void CompInfo::print_var_indexes(char *fname)
 void CompInfo::set_constr_flag()
 {
 
-  for (int i=0; i < N->Gate_list.size();i++) {
+  for (size_t i=0; i < N->Gate_list.size();i++) {
     Gate &G = N->get_gate(i);
     G.flags.label = 0;  
     G.flags.fun_constr = 0;