0002098: overloading of predicate fails - Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0002098

Frama-C

Kernel > ACSL implementation

public

2015-03-31 15:44

2016-01-26 18:30

Reporter

jens

Assigned To

virgile

Priority

normal

Severity

major

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C Sodium

Target Version

Frama-C Magnesium

Fixed in Version

Frama-C Magnesium

Summary

0002098: overloading of predicate fails

Description

Overloading of ACSL predicates does not work anymore.

Steps To Reproduce

the 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 Information

the problem does NOT occur under Neon.

Tags

No tags attached.

Attached Files

overloading.c [^] (141 bytes) 2015-03-31 15:44 [Show Content] [Hide Content]

/*@
    predicate A{L}(int x) = \true;

    predicate A{L}(short x) = \true;
*/


/*@
    ensures A(x);
*/
int foo(int x)
{
    return x;
}

overloading2.c [^] (440 bytes) 2015-04-03 12:47 [Show Content] [Hide Content]

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;
}

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

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	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