| View Issue Details [ Jump to Notes ] [ Related Changesets ] | [ Issue History ] [ Print ] |
| ID | 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 | | 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 
Relationships