0000576: axiom ignored because of label, but no label is present in axiom.

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

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

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

Date Modified	Username	Field	Change
Issue History
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: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
2011-04-04 09:30	svn	Status	closed => resolved
2011-04-04 09:30	svn	Resolution	no change required => fixed
2011-04-04 09:56	signoles	Status	resolved => closed
2011-04-04 10:04	svn
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
2013-12-19 01:12	patrick	Source_changeset_attached	=> framac master 027fe405
2014-02-12 16:55	patrick	Source_changeset_attached	=> framac stable/neon 027fe405

Issue History