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

[Frama-c-discuss] WP-plugin



Hello,

I've tried to verify my linear search example, which verifies with
Jessie, with the wp-plugin in Carbon beta2. For most properties, I get
warnings about missing RTE guards or timeouts. For example:

[wp] warning: Missing RTE guards
[wp] [Alt-Ergo] Goal store_lsearch_loop_inv_1_established : Valid
[wp] [Alt-Ergo] Goal store_lsearch_loop_inv_1_preserved : Timeout

Setting the check mark in RTE doesn't improve this.

Also, there is a "The property has not been validated" icon for a
precondition of linear search. What does that mean?

-- 
Regards,
Boris