Frama-C Bug Tracking System - Frama-C
View Issue Details
0002087Frama-CPlug-in > wppublic2015-03-03 21:412015-03-09 10:06
Frama-C Neon-20140301 
0002087: Able to assert a false statement
In the attached program, 'absurd' validates when it should not. The is only observed when all of the following conditions are met. 'num' must be part of a struct, which can be global (as in the program below) or returned from split. Changing the assigns to only r.num cause the correct behavior. However, if the struct is returned from split, absurd still validates. 'split' must be called, if the body is inlined, the bad behavior is not observed. Alt-ergo 0.99.1 must be used, can not replicate using 0.95.2 The expression must be '5/2', I have not found any other numbers that causes this behavior.
Create struc_div.c (attached): struct result { int num; }; struct result r; /*@ assigns r; ensures r.num == 5/2; */ void split() { r.num = 5/2; } void test_split() { split(); //@ assert absurd: r.num == -99 && r.num == 99; } Run: frama-c struct_div.c -wp -wp-rte Results: [kernel] preprocessing with "gcc -C -E -I. struct_div.c" [wp] Running WP plugin... [wp] Collecting axiomatic usage [rte] annotating function split [rte] annotating function test_split [wp] 3 goals scheduled [wp] [Qed] Goal typed_split_post : Valid [wp] [Qed] Goal typed_split_assign : Valid [wp] [Alt-Ergo] Goal typed_test_split_assert_absurd : Valid (26ms) (18) [wp] Proved goals: 3 / 3 Qed: 2 Alt-Ergo: 1 (26ms-26ms) (18) Expected that 'absurd' assertion should not validate.
No tags attached.
c struct_div.c (236) 2015-03-03 21:41
? foo.mlw (379) 2015-03-05 13:30
Issue History
2015-03-03 21:41IanNew Issue
2015-03-03 21:41IanStatusnew => assigned
2015-03-03 21:41IanAssigned To => correnson
2015-03-03 21:41IanFile Added: struct_div.c
2015-03-05 13:30bobotFile Added: foo.mlw
2015-03-09 10:06corrensonNote Added: 0005803
2015-03-09 10:06corrensonStatusassigned => acknowledged

2015-03-09 10:06   
After reducing the bug to a minimal version, this is due to an Alt-Ergo bug.