2021-03-01 05:46 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002098Frama-CKernel > ACSL implementationpublic2016-01-26 18:30
Reporterjens 
Assigned Tovirgile 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Sodium 
Target VersionFrama-C MagnesiumFixed in VersionFrama-C Magnesium 
Summary0002098: overloading of predicate fails
DescriptionOverloading of ACSL predicates does not work anymore.

Steps To Reproducethe attached program reports the following error when called with 'frama-c overloading.c'

[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing overloading.c (with preprocessing)
overloading.c:10:[kernel] user error: invalid implicit conversion from 'int' to 'short' in annotation.
[kernel] user error: stopping on file "overloading.c" that has errors. Add '-kernel-msg-key pp'
                     for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
Additional Informationthe problem does NOT occur under Neon.
TagsNo tags attached.
Attached Files
  • c file icon overloading.c (141 bytes) 2015-03-31 15:44 -
    /*@
        predicate A{L}(int x) = \true;
    
        predicate A{L}(short x) = \true;
    */
    
    
    /*@
        ensures A(x);
    */
    int foo(int x)
    {
        return x;
    }
    
    c file icon overloading.c (141 bytes) 2015-03-31 15:44 +
  • c file icon overloading2.c (440 bytes) 2015-04-03 12:47 -
    struct X { int n; };
    
    typedef struct X X;
    
    /*@
        predicate A{L}(long x) = \true;
    
        predicate A{L}(short x) = \true;
    
        predicate A{L}(char x) = \true;
    
        predicate A{L}(int x) = \true;
    
        predicate A{L}(long long x) = \true;
    
        predicate A{L}(X x) = \true;
    */
    
    
    /*@
        requires A(x);
    */
    long long foo(long long x)
    {
        return x;
    }
    
    
    /*@
       requires A(*x);
    
       ensures \result == x->n;
    */
    int bar(X* x)
    {
        return x->n;
    }
    
    
    c file icon overloading2.c (440 bytes) 2015-04-03 12:47 +

-Relationships
+Relationships

-Notes

~0005863

jens (reporter)

I added another example file overloading2.c and I experimented a bit with reordering the various overloaded versions.
I am not sure this is relevant but the error message

  overloading.c:22:[kernel] user error: invalid implicit conversion from 'long long' to 'int' in annotation.

refers to the 'int' version which is declared immediately before the 'long long' version.
Seems to be a pattern.

~0005886

virgile (developer)

Fix committed to master branch.

~0006140

virgile (developer)

Fait dans le commit da16395
+Notes

-Issue History
Date Modified Username Field Change
2015-03-31 15:44 jens New Issue
2015-03-31 15:44 jens File Added: overloading.c
2015-03-31 16:56 virgile Assigned To => virgile
2015-03-31 16:56 virgile Status new => confirmed
2015-03-31 16:56 virgile Category Kernel => Kernel > ACSL implementation
2015-03-31 16:56 virgile Target Version => Frama-C Magnesium
2015-04-03 12:47 jens File Added: overloading2.c
2015-04-03 12:52 jens Note Added: 0005863
2015-04-14 18:13 virgile Source_changeset_attached => framac master 5e67952e
2015-04-14 18:13 virgile Note Added: 0005886
2015-04-14 18:13 virgile Status confirmed => resolved
2015-04-14 18:13 virgile Resolution open => fixed
2016-01-26 08:51 signoles Fixed in Version => Frama-C Magnesium
2016-01-26 08:52 signoles Status resolved => closed
2016-01-26 18:30 virgile Note Added: 0006140
+Issue History