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?
I noticed this "fix" because I turned the printing diagnostics on, and the bug disappeared. The only extra thing I do when I print is to ask for the constraints and pretty print them.
As usual, I could be missing something obvious :-) , or it could be a bug. If you could point me out to the right direction, I am very grateful. In the meantime, the release I sent you has the same bug which is absent in the older version. So please ignore the code. I will send you a new version when I fix this bug.
Thanks, Sriram
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.
participants (2)
-
Enea Zaffanella -
Roberto Bagnara