Skip to content

known, but inferrable, yet not inferred, property not given as precodition to provers

ID0002330: This issue was created automatically from Mantis Issue 2330. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0002330 Frama-C Plug-in > wp public 2017-10-26 2020-02-17
Reporter Jochen Assigned To correnson Resolution fixed
Priority normal Severity minor Reproducibility always
Platform Phosphorus-20170501 OS - OS Version xubuntu 17.04
Product Version - Target Version - Fixed in Version Frama-C 20-Calcium

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

Attachments

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information