Frama-C Bug Tracking System - Frama-C
View Issue Details
0000750Frama-CKernel > ACSL implementationpublic2011-03-08 17:272014-02-12 16:54
0000750: Several [invariant] at a program point
If 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] ?
No tags attached.
Issue History
2011-03-08 17:27AnneNew Issue
2011-03-08 17:27AnneStatusnew => assigned
2011-03-08 17:27AnneAssigned To => virgile
2011-03-08 18:35virgileNote Added: 0001570
2011-03-08 18:35virgileStatusassigned => acknowledged
2011-03-10 14:50patrickRelationship addedchild of 0000494
2011-03-11 08:38patrickNote Added: 0001588
2011-03-11 08:40svnCheckin
2011-03-11 08:47patrickNote Added: 0001590
2011-09-30 15:25patrickRelationship addedrelated to 0000975

2011-03-08 18:35   
This seems reasonable, but requires a change in ACSL specification itself before modifying the implementation.
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.
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.