delcypher / freeboogie

Automatically exported from code.google.com/p/freeboogie
0 stars 1 forks source link

getting rid of cycles is unsound #60

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago
The combination HavocMaker+LoopCutter does *not* lead to a sound
transformation as I thought. It works for the fancy example of the smallest
irreducible graph (1->2,1->3,2<->3) but fails for simper things like two
nested loops :P I am not sure how I managed to convinced myself that it is
correct before but I need to fix it.

Original issue reported on code.google.com by radugrig...@gmail.com on 20 Sep 2009 at 6:43