Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002265Frama-CKernel > ACSL implementationpublic2017-01-02 06:272017-01-02 06:27
Reporterjens 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C 14-Silicon 
Target VersionFixed in Version 
Summary0002265: label Pre in function contracts
DescriptionI have recently noted that we use both 'Pre' and 'Old' in function contracts of "ACSL by Example".
The ACSL description, however, mentions the label 'Pre' only for statement annotations.

Is there a reason to allow both labels in function contracts?
If not, then I would suggest to forbid 'Pre' in function contracts.
TagsNo tags attached.
Attached Filesc file icon swap.c [^] (197 bytes) 2017-01-02 06:27 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2017-01-02 06:27 jens New Issue
2017-01-02 06:27 jens Status new => assigned
2017-01-02 06:27 jens Assigned To => virgile
2017-01-02 06:27 jens File Added: swap.c


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker