Anonymous Login Frama-C issues should now be submitted on Frama-C's GitLab
2021-03-06 03:05 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000505Frama-CKernel > ACSL implementationpublic2014-02-12 16:55
Reportervirgile 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000505: Predicate/Functions depending only on a state are not handled correctly
Descriptiona predicate with only a label (and no formals) can be applied as a variable (see attached file for examples). In this case, ACSL type-checker fails to attach to it the current default label.
TagsNo tags attached.
Attached Files
  • ? file icon constant_predicate.i (148 bytes) 2010-06-09 18:33 -
    int x;
    
    /*@ predicate P{A} = x == 42; */
    
    /*@ logic integer f{B} = x + 42; */
    
    /*@ ensures f == 84; */
    void g () {
    
      x = 42;
      /*@ assert P; */
    
    }
    
    ? file icon constant_predicate.i (148 bytes) 2010-06-09 18:33 +

-Relationships
+Relationships

-Notes
There are no notes attached to this issue.
+Notes

-Issue History
Date Modified Username Field Change
2010-06-09 18:33 virgile New Issue
2010-06-09 18:33 virgile Status new => assigned
2010-06-09 18:33 virgile Assigned To => virgile
2010-06-09 18:33 virgile File Added: constant_predicate.i
2010-06-09 18:35 virgile Status assigned => acknowledged
2010-06-09 18:38 svn
2010-06-10 19:18 svn
2010-06-10 19:18 svn Status acknowledged => resolved
2010-06-10 19:18 svn Resolution open => fixed
2010-12-10 15:45 signoles Fixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:36 signoles Status resolved => closed
2013-12-19 01:13 Source_changeset_attached => framac master bd8dc916
2013-12-19 01:13 Source_changeset_attached => framac master 85452df2
2014-02-12 16:55 Source_changeset_attached => framac stable/neon bd8dc916
2014-02-12 16:55 Source_changeset_attached => framac stable/neon 85452df2
+Issue History