Fix memory leaks in proof-checker expressions

2 files changed, 22 insertions, 23 deletions

diff --git a/proofs/lfsc_checker/check.cpp b/proofs/lfsc_checker/check.cpp
index 22e326cda..222c10615 100644
--- a/proofs/lfsc_checker/check.cpp
+++ b/proofs/lfsc_checker/check.cpp
@@ -87,10 +87,10 @@ char our_getc_c = 0;
 int IDBUF_LEN = 2048;
 char idbuf[2048];
 
-Expr *statType = new CExpr(TYPE, 0);
-Expr *statKind = new CExpr(KIND, 0);
-Expr *statMpz = new CExpr(MPZ,0);
-Expr *statMpq = new CExpr(MPQ,0);
+Expr *statType = new CExpr(TYPE);
+Expr *statKind = new CExpr(KIND);
+Expr *statMpz = new CExpr(MPZ);
+Expr *statMpq = new CExpr(MPQ);
 
 int open_parens = 0;
 
@@ -466,7 +466,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
       SymExpr *sym = new SymExpr(id);
 #endif
       int prev_open = open_parens;
-      Expr *tp_of_trm;
+      Expr *tp_of_trm = NULL;
       Expr *trm = check(true, NULL, &tp_of_trm);
       eat_excess(prev_open);
 
diff --git a/proofs/lfsc_checker/expr.cpp b/proofs/lfsc_checker/expr.cpp
index 784a0ad2f..32f91c934 100644
--- a/proofs/lfsc_checker/expr.cpp
+++ b/proofs/lfsc_checker/expr.cpp
@@ -205,13 +205,12 @@ Expr* Expr::build_app(Expr *hd, const std::vector<Expr *> &args, int start) {
     return hd;
   else
   {
-    CExpr *ret = new CExpr( APP );
-    ret->kids = new Expr* [args.size()-start+2];
-    ret->kids[0] = hd;
+    Expr **kids = new Expr* [args.size()-start+2];
+    kids[0] = hd;
     for (int i = start, iend = args.size(); i < iend; i++)
-        ret->kids[i-start+1] = args[i];
-    ret->kids[args.size()-start+1] = NULL;
-    return ret;
+        kids[i-start+1] = args[i];
+    kids[args.size()-start+1] = NULL;
+    return new CExpr(APP, true /* dummy */, kids);
   }
 #endif
 }
@@ -229,16 +228,16 @@ Expr* Expr::make_app(Expr* e1, Expr* e2 )
       while( ((CExpr*)e1)->kids[counter] ){
          counter++;
       }
-      ret = new CExpr( APP );
-      ret->kids = new Expr* [counter+2];
+      Expr **kids = new Expr* [counter+2];
       counter = 0;
       while( ((CExpr*)e1)->kids[counter] ){
-         ret->kids[counter] = ((CExpr*)e1)->kids[counter];
-         ret->kids[counter]->inc();
+         kids[counter] = ((CExpr*)e1)->kids[counter];
+         kids[counter]->inc();
          counter++;
       }
-      ret->kids[counter] = e2;
-      ret->kids[counter+1] = NULL;
+      kids[counter] = e2;
+      kids[counter+1] = NULL;
+      ret = new CExpr(APP, true /* dummy */, kids);
    }else{
       ret = new CExpr( APP, e1, e2 );
    }
@@ -369,14 +368,14 @@ Expr* CExpr::convert_to_flat_app( Expr* e )
   {
     std::vector< Expr* > args;
     Expr* hd = ((CExpr*)e)->collect_args( args );
-    CExpr* nce = new CExpr( APP );
-    nce->kids = new Expr *[(int)args.size()+2];
-    nce->kids[0] = hd;
+    Expr **kids = new Expr *[(int)args.size()+2];
+    kids[0] = hd;
     for( int a=0; a<(int)args.size(); a++ )
     {
-      nce->kids[a+1] = convert_to_flat_app( args[a] );
+      kids[a+1] = convert_to_flat_app( args[a] );
     }
-    nce->kids[(int)args.size()+1] = 0;
+    kids[(int)args.size()+1] = 0;
+    CExpr* nce = new CExpr(APP, true /* dummy */, kids);
     nce->inc();
     return nce;
   }
@@ -648,7 +647,7 @@ bool Expr::free_in(Expr *x) {
       Expr **cur = e->kids;
       while ((tmp = *cur++))
          if (tmp->free_in(x))
-	         return true;
+            return true;
       return false;
    }
    }