cvc5/LFSC

Reference counting bug

Closed this issue · 5 comments

In expr.h expressions have a 21 bit reference counter.
Method inc() properly checks for overflows in this counter.

Once the max ref count is reached, the expression should never be
deleted and its reference counter should never be decremented.

But method dec() in expr.h and macro destroydec(rr) in expr.cpp
do not do this. They should be fixed to be no-op when the refcount has
reached its max value.

Yes, you're right, I will commit a fix for this soon.

Thanks,

While you're at it, here are a few more issues:

  1. I'm getting compiler errors because of a missing
    #include <istream> in lfscc.h.

  2. It looks like there's a memory leak in code.cpp (lines 1025--1034).

     if (r1 < r2)
     {
       r1->dec();
       _e = e->kids[2];
       goto start_run_code;
     }
     // else
     r2->dec();
     _e = e->kids[3];
    

    I think you should call r1->dec() and r2->dec() on both branches.

  3. maybe call delete s_lexer at the end of check_file.

I've opened #64 to address 2 and 3. For 1, don't see #include <istream> in lfscc.h?

The include is missing.

For some mysterious reason, this used to be no-problem, but now I'm getting this error from g++:

In file included from /home/dutebrun/Repos/LFSC/src/lfscc.cpp:1:0:
/home/dutebrun/Repos/LFSC/src/lfscc.h:24:28: error: variable or field ‘lfscc_check_file’ declared void
 void lfscc_check_file(std::istream& in,
                            ^~~~~~~
/home/dutebrun/Repos/LFSC/src/lfscc.h:24:28: error: ‘istream’ is not a member of ‘std’
/home/dutebrun/Repos/LFSC/src/lfscc.h:24:37: error: ‘in’ was not declared in this scope
 void lfscc_check_file(std::istream& in,
                                     ^~
/home/dutebrun/Repos/LFSC/src/lfscc.h:24:37: note: suggested alternative: ‘int’
 void lfscc_check_file(std::istream& in,
                                     ^~
                                     int

Adding the include fixes this.

Ah, I misunderstood, I thought you meant that #include <istream> should be removed, not added. I can add this.