lfsc_checker: fix some warnings reported by _both_ gcc and clang

diff --git a/proofs/lfsc_checker/code.cpp b/proofs/lfsc_checker/code.cpp
index 34c6c133b37d21197d7265a81aa58fc12c8aa67b..ee143a7102c77888a8f00ce23a3dff4a4c01eceb 100644 (file)
--- a/proofs/lfsc_checker/code.cpp
+++ b/proofs/lfsc_checker/code.cpp
@@ -1141,7 +1141,7 @@ Expr *run_code(Expr *_e) {
     if (!r1)
       return NULL;
 
-    bool cond;
+    bool cond = true;
     if( r1->getclass() == INT_EXPR ){
       if( e->getop() == IFNEG )
         cond = mpz_sgn( ((IntExpr *)r1)->n )<0;
@@ -1244,7 +1244,7 @@ Expr *run_code(Expr *_e) {
     vector<Expr *> args;
     Expr *hd = scrut->collect_args(args);
     Expr **cases = &e->kids[1];
-    CExpr *c;
+    // CExpr *c;
     Expr *c_or_default;
     while ((c_or_default = *cases++)) {
 
@@ -1382,4 +1382,4 @@ int read_index()
     index = atoi( v.c_str() );
   }
   return index;
-}
\ No newline at end of file
+}

diff --git a/proofs/lfsc_checker/print_smt2.cpp b/proofs/lfsc_checker/print_smt2.cpp
index bf068c248a786f2d40243e4509161579705133da..34cb00cc46ee16ba9b13dd96eb3fe1757749b464 100644 (file)
--- a/proofs/lfsc_checker/print_smt2.cpp
+++ b/proofs/lfsc_checker/print_smt2.cpp
@@ -54,7 +54,7 @@ void print_smt2( Expr* p, std::ostream& s, short mode )
             s << " ";\r
             for( int a=0; a<(int)args.size(); a++ ){\r
               print_smt2( args[a], s, newMode );\r
-              if( a!=args.size()-1 )\r
+              if( a!=(int)args.size()-1 )\r
                 s << " ";\r
             }\r
             s << ")";\r

diff --git a/proofs/lfsc_checker/scccode.cpp b/proofs/lfsc_checker/scccode.cpp
index cff762a088dc09751bc821396ee5a7ea41405026..22f26ec8893c81f058f06062e67756fea62e1ae0 100644 (file)
--- a/proofs/lfsc_checker/scccode.cpp
+++ b/proofs/lfsc_checker/scccode.cpp
@@ -99,11 +99,11 @@ Expr* f_litpol( Expr* l ){
    e3 = e_neg;
    e3->inc();
    if( e1==e2 ){
-      Expr* x = ((CExpr*)l->followDefs())->kids[1];
+      // Expr* x = ((CExpr*)l->followDefs())->kids[1];
       e0 = e_tt;
       e0->inc();
    }else if( e1==e3 ){
-      Expr* x = ((CExpr*)l->followDefs())->kids[1];
+      // Expr* x = ((CExpr*)l->followDefs())->kids[1];
       e0 = e_ff;
       e0->inc();
    }else{