Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000601Frama-CKernel > ACSL implementationpublic2010-10-12 20:202010-12-16 10:06
Assigned Tovirgile 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in Version 
Summary0000601: no multiple assert-clauses accepted in /*@...*/-style comment
DescriptionSee attached program: when #define multipleAsserts is in force, the kernel complains about line 11-12, containing two assert-clauses in a single /*@...*/ comment. I'm not sure this contradicts some ASCL-syntax definition. However, it appears strange to me, since multiple requires, ensures, and loop invariant are admitted (although they could be joined into a single one by &&, as for assert, too).
TagsNo tags attached.
Attached Filesc file icon ftest.c [^] (285 bytes) 2010-10-12 20:20 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2010-10-12 20:20 Jochen New Issue
2010-10-12 20:20 Jochen File Added: ftest.c
2010-10-13 07:00 signoles Status new => assigned
2010-10-13 07:00 signoles Assigned To => virgile
2010-12-16 10:06 signoles Category Kernel => Kernel > ACSL implementation

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker