search

scylla / loop-invariant

Automatically exported from code.google.com/p/loop-invariant
0 stars 0 forks source link

calculus failed on strategy #1

Open GoogleCodeExporter opened 8 years ago

GoogleCodeExporter commented 8 years ago 
calculus failed on strategy
              for 'parse_dns_reply', behavior 'default!', property
loop_inv_60382, both assigns or not
              because unsupported non-natural loop without invariant property.
(abort);

Original issue reported on code.google.com by zhliu.w...@gmail.com on 5 Apr 2012 at 3:10

GoogleCodeExporter commented 8 years ago 
A loop is not a natural loop if it has several entries (no loop header), or if 
it has some irreducible region (no back edge).

Original comment by zhliu.w...@gmail.com on 5 Apr 2012 at 3:10

GoogleCodeExporter commented 8 years ago 
sendmail中CIL转化后的有non-natural 
loop，因为没有后向边。如果跳过这样的分析？

Original comment by zhliu.w...@gmail.com on 5 Apr 2012 at 3:11

GoogleCodeExporter commented 8 years ago 
手工去除while(1){a=b;break;}这样的循环

Original comment by zhliu.w...@gmail.com on 5 Apr 2012 at 3:26