Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 173
    • Issues 173
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #1719
Closed
Open
Issue created Aug 26, 2010 by Fabrice Derepas@fderepas

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

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


Id Project Category View Due Date Updated
ID0000576 Frama-C Plug-in > wp public 2010-08-26 2014-02-12
Reporter derepas Assigned To Anne Resolution fixed
Priority normal Severity minor Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C GIT, precise the release id Target Version - Fixed in Version Frama-C Nitrogen-20111001

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.

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