2021-03-01 05:46 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002098Frama-CKernel > ACSL implementationpublic2015-03-31 15:442016-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)

2015-04-03 12:52

 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)

2015-04-14 18:13

 Fix committed to master branch.

~0006140

virgile (developer)

2016-01-26 18:30

 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