Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000750Frama-CKernel > ACSL implementationpublic2011-03-08 17:272014-02-12 16:54
ReporterAnne 
Assigned Tovirgile 
PrioritynormalSeverityfeatureReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0000750: Several [invariant] at a program point
DescriptionIf we want to put several [invariant] annotations at a program point, we have to have several ACSL comment, else we get :
  [kernel] user error: Only one code annotation is allowed per comment
But with several comments, several program points are created, and it is then difficult to interpret the invariants, because it seems that they have to be considered as a sequence, while we want to see them as a conjunction...

Would it be possible to have several invariants at the same point like it is done for le [loop invariant] ?
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0001570)
virgile (developer)
2011-03-08 18:35

This seems reasonable, but requires a change in ACSL specification itself before modifying the implementation.
(0001588)
patrick (developer)
2011-03-11 08:38

In fact, plug-ins can generate several code annotations related to a unique statement. The kind of these code annotations may be different.
An order as been defined between these kinds at the pretty printing:
  asserts < stmt contract < invariants < pragmas < loop annotations
but it wasn't used until next commit.
(0001590)
patrick (developer)
2011-03-11 08:47

Anyway, something seems to be needed at the ACSL level to ensure re-entrance.
Today, pretty printing a C project having several code annotations at the same points, and parsing that output doesn't produce the same links between stmts and code annotations.

- Issue History
Date Modified Username Field Change
2011-03-08 17:27 Anne New Issue
2011-03-08 17:27 Anne Status new => assigned
2011-03-08 17:27 Anne Assigned To => virgile
2011-03-08 18:35 virgile Note Added: 0001570
2011-03-08 18:35 virgile Status assigned => acknowledged
2011-03-10 14:50 patrick Relationship added child of 0000494
2011-03-11 08:38 patrick Note Added: 0001588
2011-03-11 08:40 svn Checkin
2011-03-11 08:47 patrick Note Added: 0001590
2011-09-30 15:25 patrick Relationship added related to 0000975


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker