Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000068Frama-CPlug-in > Evapublic2009-04-28 12:052014-02-12 16:56
Reporterddelmas 
Assigned Topascal 
PrioritynormalSeverityfeatureReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Lithium-20081201 
Target VersionFrama-C Boron-20100401Fixed in VersionFrama-C Beryllium-20090902 
Summary0000068: Plug-in inout fails to parse clause /*@ assigns s[..]; */
DescriptionConsider the following example:

//@ assigns s[..];
void F1(char *s);

char T[100];

void F2(int c)
{
    if (c) F1(T);
}

Running "frama-c file.c -main F2 -lib-entry -out" yields a parse error.
TagsNo tags attached.
Attached Files

- Relationships
parent of 0000230closedpascal Missing functions to convert logic terms directly to abstract values 

-  Notes
(0000039)
virgile (developer)
2009-04-29 09:17

There is no parse error in the file. Is the issue related to the following warnings:

bug068.c:8: Warning: Can not interpret assigns in function F1; effects will be ignored
bug068.c:8: Warning: unsupported assigns clause for function F1; Ignoring it.
?

If yes, the real issue is that such assigns could indeed be better supported by the value analysis.

- Issue History
Date Modified Username Field Change
2009-04-28 12:05 ddelmas New Issue
2009-04-29 09:17 virgile Note Added: 0000039
2009-04-29 15:19 virgile Status new => assigned
2009-04-29 15:19 virgile Assigned To => virgile
2009-06-17 13:35 signoles Assigned To virgile => pascal
2009-06-17 13:35 signoles Category plug-in > inout => plug-in > value analysis
2009-08-26 10:43 signoles Severity major => feature
2009-08-28 18:01 signoles Status assigned => confirmed
2009-08-28 18:01 signoles Target Version => Frama-C Bore
2009-09-08 11:08 pascal Relationship added parent of 0000230
2009-09-08 19:03 svn Checkin
2009-09-09 22:53 svn Checkin
2009-09-10 14:57 svn Checkin
2009-09-10 14:57 svn Status confirmed => resolved
2009-09-10 14:57 svn Resolution open => fixed
2009-09-23 15:26 signoles Fixed in Version => Frama-C Beryllium 2
2009-09-23 20:22 signoles Status resolved => closed
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker