2021-01-15 19:28 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000750Frama-CKernel > ACSL implementationpublic2014-02-12 16:54
Assigned Tovirgile 
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




virgile (developer)

This seems reasonable, but requires a change in ACSL specification itself before modifying the implementation.


patrick (developer)

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.


patrick (developer)

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-11 08:38 patrick Note Added: 0001588
2011-03-11 08:40 svn
2011-03-11 08:47 patrick Note Added: 0001590
2013-12-19 01:12 patrick Source_changeset_attached => framac master 71d60a65
2014-02-12 16:54 patrick Source_changeset_attached => framac stable/neon 71d60a65
+Issue History