unproven property used in a behavior in Typed model
ID0001299: This issue was created automatically from Mantis Issue 1299. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001299 | Frama-C | Plug-in > wp | public | 2012-11-06 | 2013-04-19 |
| Reporter | sduprat | Assigned To | correnson | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Oxygen-20120901 | Target Version | - | Fixed in Version | Frama-C Fluorine-20130401 |
Description :
In the attached example, the b1_P1 property is unproven while the equivalent whithout the use of behavior is well proven.
This is in case if Typed model. In Store, all is proved.
Seeing the generated goals, perhaps a lack of relation between Mint_1 and Mint_0?
Or a problem in my assigns ? In case of problem, is there any workaround ?
Regards.
Stéphane
Additional Information :
Used with Alt-Ergo 0.94.
command used : //frama-c -wp -wp-print -wp-byreference -wp-model Typed report1.c
Attachments
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information