--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on February 2011 ---
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