|Anonymous | Login | Signup for a new account||2019-05-21 16:10 CEST|
|Main | My View | View Issues | Change Log | Roadmap | Repositories|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0002330||Frama-C||Plug-in > wp||public||2017-10-26 12:55||2017-10-26 12:55|
|Platform||Phosphorus-20170501||OS||OS Version||xubuntu 17.04|
|Target Version||Fixed in Version|
|Summary||0002330: known, but inferrable, yet not inferred, property not given as precodition to provers|
|Description||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.
|Steps To Reproduce||Name translation c -> mlw for convenience:|
x -> i
y -> x
z -> x_1
|Tags||No tags attached.|
|Attached Files||foo.c [^] (246 bytes) 2017-10-26 12:55 [Show Content]|
|2017-10-26 12:55||Jochen||New Issue|
|2017-10-26 12:55||Jochen||Status||new => assigned|
|2017-10-26 12:55||Jochen||Assigned To||=> correnson|
|2017-10-26 12:55||Jochen||File Added: foo.c|
|Copyright © 2000 - 2019 MantisBT Team|