Able to assert a false statement
ID0002087: This issue was created automatically from Mantis Issue 2087. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002087 | Frama-C | Plug-in > wp | public | 2015-03-03 | 2015-03-09 |
| Reporter | Ian | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | Ubuntu | OS Version | - |
| Product Version | Frama-C Neon-20140301 | Target Version | - | Fixed in Version | - |
Description :
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.
Steps To Reproduce :
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.