| Anonymous | Login | Signup for a new account | This BTS is being migrated to Gitlab, consider using those issues instead |  |
| Main | My View | View Issues | Change Log | Roadmap | Repositories |
| View Issue Details [ Jump to Notes ] [ Related Changesets ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
| 0000576 | Frama-C | Plug-in > wp | public | 2010-08-26 11:11 | 2014-02-12 16:55 | ||||
| Reporter | derepas | ||||||||
| Assigned To | Anne | ||||||||
| Priority | normal | Severity | minor | Reproducibility | always | ||||
| Status | closed | Resolution | fixed | ||||||
| Platform | OS | OS Version | |||||||
| Product Version | Frama-C GIT, precise the release id | ||||||||
| Target Version | Fixed in Version | Frama-C Nitrogen-20111001 | |||||||
| Summary | 0000576: axiom ignored because of label, but no label is present in axiom. | ||||||||
| Description | svn release id is 'r9704'. I have the following code in file ex.c: /*@ @ axiomatic MyAxio { @ logic integer my_super_fun (char * x,char * y); @ axiom my_super_axiom_1: \forall char* x; \forall char* y; @ (*(x+0)==*(y+0)) ==> my_super_fun(x,y); @ axiom my_super_axiom_2: \forall char * x; \forall char * y; @ (x[0]==y[0]) ==> my_super_fun(x,y); @ } @*/ int main (char *x, char *y) { //@ assert my_super_fun (x,y); return 0; } Launching the wp on this code yields : > frama-c -wp -wp-out why_dir ex.c [kernel] preprocessing with "gcc -C -E -I. ex.c" ex.c:11:[wp] warning: Ignoring axiom my_super_axiom_2 (because of labels) ex.c:11:[wp] warning: Ignoring axiom my_super_axiom_1 (because of labels) But it seems to me that there are no labels in these axioms. | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files | |||||||||
 Relationships |
|
 Relationships |
|
Notes |
|
|
(0001103) Anne (reporter) 2010-08-26 11:15 |
In fact, there is an implicit label in the logic function definition because it has pointer parameters, so it needs a memory state to be evaluated. So the axioms have a label too. |
|
(0001104) derepas (reporter) 2010-08-26 11:25 |
Thank you for the explanation ! |
|
(0001769) signoles (manager) 2011-04-13 15:28 |
Fixed in WP 0.3 compatible with Frama-C Carbon. |
|
(0002359) correnson (manager) 2011-09-30 12:35 |
Parent bug. |
|
Notes |
|
Issue History |
|||
| Date Modified | Username | Field | Change |
| 2010-08-26 11:11 | derepas | New Issue | |
| 2010-08-26 11:11 | derepas | Status | new => assigned |
| 2010-08-26 11:11 | derepas | Assigned To | => Anne |
| 2010-08-26 11:15 | Anne | Note Added: 0001103 | |
| 2010-08-26 11:16 | Anne | Relationship added | child of 0000573 |
| 2010-08-26 11:25 | derepas | Note Added: 0001104 | |
| 2010-08-26 11:50 | Anne | Status | assigned => resolved |
| 2010-08-26 11:50 | Anne | Resolution | open => no change required |
| 2010-08-26 13:58 | signoles | Status | resolved => closed |
| 2011-04-04 09:30 | svn | Checkin | |
| 2011-04-04 09:30 | svn | Note Added: 0001682 | |
| 2011-04-04 09:30 | svn | Status | closed => resolved |
| 2011-04-04 09:30 | svn | Resolution | no change required => fixed |
| 2011-04-04 09:55 | signoles | Note Deleted: 0001682 | |
| 2011-04-04 09:56 | signoles | Status | resolved => closed |
| 2011-04-04 10:04 | svn | Checkin | |
| 2011-04-04 10:04 | svn | Status | closed => resolved |
| 2011-04-13 15:28 | signoles | Note Added: 0001769 | |
| 2011-04-13 15:28 | signoles | Fixed in Version | => Frama-C Carbon-20110201 |
| 2011-04-13 15:28 | signoles | Status | resolved => closed |
| 2011-09-30 12:35 | correnson | Note Added: 0002359 | |
| 2011-09-30 12:35 | correnson | Status | closed => resolved |
| 2011-10-10 14:13 | signoles | Fixed in Version | Frama-C Carbon-20110201 => Frama-C Nitrogen-20111001 |
| 2011-10-10 14:14 | signoles | Status | resolved => closed |
|
Issue History |
| Copyright © 2000 - 2020 MantisBT Team |
|