0000750: Several [invariant] at a program point

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0000750

Frama-C

Kernel > ACSL implementation

public

2011-03-08 17:27

2014-02-12 16:54

Reporter

Anne

Assigned To

virgile

Priority

normal

Severity

feature

Reproducibility

always

Status

acknowledged

Resolution

open

Platform

OS Version

Product Version

Target Version

Fixed in Version

Summary

0000750: Several [invariant] at a program point

Description

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] ?

Tags

No 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