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.