Frama-C Bug Tracking System - Frama-C
View Issue Details
0002330Frama-CPlug-in > wppublic2017-10-26 12:552019-10-17 17:30
Jochen 
correnson 
normalminoralways
resolvedfixed 
Phosphorus-20170501xubuntu 17.04
 
 
0002330: known, but inferrable, yet not inferred, property not given as precodition to provers
Running "frama-c -wp foo.c -wp-out wp-out -wp-prop=D" on the attached program fails to prove the property D, although it follows immediately from A and C. A look at the generated file "foo_assert_D_Alt-Ergo.mlw" reveals that the condition "y<=15" from C is not given to Alt-Ergo, while "0<=y" is. If the former is inserted into the mlw file, Alt-Ergo proves the goal without problems. Probably, "y<=15" is considered a trivial consequence of "y==(x&0xf)" by Qed; however, it shouldn't, since (e.g.) Alt-Ergo is unable to to infer this: goal C cannot be proven by Alt-Ergo.
Name translation c -> mlw for convenience: x -> i y -> x z -> x_1
No tags attached.
c foo.c (246) 2017-10-26 12:55
https://bts.frama-c.com/file_download.php?file_id=1210&type=bug
Issue History
2017-10-26 12:55JochenNew Issue
2017-10-26 12:55JochenStatusnew => assigned
2017-10-26 12:55JochenAssigned To => correnson
2017-10-26 12:55JochenFile Added: foo.c
2019-10-17 17:29corrensonNote Added: 0006909
2019-10-17 17:30corrensonStatusassigned => resolved
2019-10-17 17:30corrensonResolutionopen => fixed

Notes
(0006909)
correnson   
2019-10-17 17:29   
Proved under TIP by using the bit-range tactic and the instance tactic.