--- layout: fc_discuss_archives title: Message 74 from Frama-C-discuss on January 2014 ---
Hi, The following code has a useless if statement, which is always true, I was hoping to get some feedback on that issue, but all the behaviors are proved correct; This code is a representative of a real error, which was manually detected during code review. I was trying to see whether WP can detect it... [formal_verification]$ frama-c -wp -wp-rte always_true.c -lib-entry [kernel] preprocessing with "gcc -C -E -I. always_true.c" [wp] Running WP plugin... [wp] Collecting axiomatic usage [rte] annotating function main [wp] 4 goals scheduled [wp] [Qed] Goal typed_main_complete_Low_High : Valid [wp] [Qed] Goal typed_main_disjoint_Low_High : Valid [wp] [Qed] Goal typed_main_High_post : Valid (4ms) [wp] [Qed] Goal typed_main_Low_post : Valid int MAX_VALUE = 100; float x = 0.0; int status = 0; /*@ requires MAX_VALUE == 100; behavior High: assumes x > MAX_VALUE; ensures status == -1; behavior Low: assumes x <= MAX_VALUE; ensures status == -1; complete behaviors; disjoint behaviors; */ int main() { if((x > MAX_VALUE) || (x <= MAX_VALUE)) { status = -1; } }