--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on August 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem of "\separated" with WP



Hi,
Thank you for this example.
It was actually a bug in the WP, related to the treatment of 'Here' in  
loop invariants.
We also optimized the traduction of separation predicates, which  
results in your copy2.c is now entirely proved but the last assertion.
Regards,
	L.