[LFSC] Fix memory leaks when creating CExprs

In certain cases, LFSC was creating CExprs with the single-argument
constructor, which allocates an array of one child, only to immediately
replace it with a new array (without deleting the old one).
Additionally, this commit fixes the construction of TYPE/KIND/MPZ/MPQ
expressions (the null pointer is appended automatically by the single
argument constructor, an array with two null pointer entries should not
be necessary).

diff --git a/proofs/lfsc_checker/check.cpp b/proofs/lfsc_checker/check.cpp
index 22e326cdae86a89f9ff4a8d685dfda61b31831d8..222c10615f5e6286ede197db5591146cea5396f8 100644 (file)
--- 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 784a0ad2f2a534109f4f614e23dc2af94f2391ea..7bd26db2cde89ae7a40d1da226bb51cd5a33ec42 100644 (file)
--- 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();
-         counter++;
+        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,13 @@ 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;
-    for( int a=0; a<(int)args.size(); a++ )
-    {
-      nce->kids[a+1] = convert_to_flat_app( args[a] );
+    Expr **kids = new Expr *[args.size() + 2];
+    kids[0] = hd;
+    for (size_t a = 0; a < args.size(); a++) {
+      kids[a + 1] = convert_to_flat_app(args[a]);
     }
-    nce->kids[(int)args.size()+1] = 0;
+    kids[args.size() + 1] = 0;
+    CExpr *nce = new CExpr(APP, true /* dummy */, kids);
     nce->inc();
     return nce;
   }
@@ -647,8 +645,7 @@ bool Expr::free_in(Expr *x) {
       Expr *tmp;
       Expr **cur = e->kids;
       while ((tmp = *cur++))
-         if (tmp->free_in(x))
-                return true;
+        if (tmp->free_in(x)) return true;
       return false;
    }
    }