[PPL-devel] Bug in PPL?

[Enea Zaffanella]

Sriram Sankaranarayanan wrote:
> Dear Roberto,
> 
> If you run lsting invcheck < berkeley.in, you will notice that the 
> output of CH79 fails to be inductive.  The bug only happens when you compile
> the code with the boring diagnostic messages turned off.
> 
> I also noticed that adding the line
> 
>  ConSys cs = my_poly.constraints();
> 
> just before I widen my_poly (InvariantMap.cc Line 94) corrects this problem.
> I am still clueless  about this. It is not like I use "cs" for anything else.
> It is just a dummy call.
> 
> Does it have to do with the fact that the widening may not work properly
> if the constraint representation is stale or missing, or something?

[...]

Dear Sriram,

it seems like you have spotted a genuine bug in the PPL.
The bug is in a private method of GenSys and, as far as I can see, it 
affects (under somehow specific circumstances) the H79_widening_assign() 
method and all the limited/bounded extrapolation methods for polyhedra:
when the bug comes into play, you will obtain a polyhedron which is not 
an upper bound of the arguments. In contrast, the 
BHRZ03_widening_assign() method shouldn't be affected at all.

I have already corrected the bug in CVS. I will now go on with some 
regression testing and, if all goes as expected, I will produce a patch 
against PPL 0.6.1 by tomorrow.

Thanks for your contribution,
Enea.