Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Related Changesets ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000576Frama-CPlug-in > wppublic2010-08-26 11:112014-02-12 16:55
Reporterderepas 
Assigned ToAnne 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000576: axiom ignored because of label, but no label is present in axiom.
Descriptionsvn 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.
TagsNo tags attached.
Attached Files

- 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.

- 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

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker