Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001162Frama-CKernel > ACSL implementationpublic2012-04-16 18:262012-09-19 17:16
Reporternmuller 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001162: "for" clause is refused
DescriptionThe following annotation is refused :
    ensures \result == {s for a = (int)4 };

in the file StructTestPos.c
Additional Information[kernel] preprocessing with "gcc -C -E -I. -dD StructTestPos.c"
StructTestPos.c:38:[kernel] user error: unexpected token 'for'
[kernel] user error: skipping file "StructTestPos.c" that has errors.
[kernel] Frama-C aborted because of invalid user input.
TagsNo tags attached.
Attached Filesc file icon StructTestPos.c [^] (624 bytes) 2012-04-16 18:26 [Show Content]

- Relationships

-  Notes
(0002932)
virgile (developer)
2012-04-17 17:41

Correct syntax for functional update is { s \with .a = 4 } (see ACSL manual at http://frama-c.com/download/acsl_1.5.pdf [^]). It is supported by Frama-C's kernel in Nitrogen (although the implementation manual does not reflect it). Not all plug-ins have support for it, though.

- Issue History
Date Modified Username Field Change
2012-04-16 18:26 nmuller New Issue
2012-04-16 18:26 nmuller Status new => assigned
2012-04-16 18:26 nmuller Assigned To => virgile
2012-04-16 18:26 nmuller File Added: StructTestPos.c
2012-04-17 17:41 virgile Note Added: 0002932
2012-04-17 17:41 virgile Status assigned => resolved
2012-04-17 17:41 virgile Fixed in Version => Frama-C Nitrogen-20111001
2012-04-17 17:41 virgile Resolution open => fixed
2012-09-19 17:15 signoles Fixed in Version Frama-C Nitrogen-20111001 => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker