Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000790Frama-CKernel > ACSL implementationpublic2011-04-12 15:052014-02-12 16:59
Reporterpatrick 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000790: integrity problem of the AST on calls to functions with __attribute__ ((noreturn))
DescriptionCalls to function with __attribute__ ((noreturn)) have no successor.
If it is wright, that raises an ACSL problem on the specification of such functions. What are their specification?

Additional InformationThe command:
> frama-c -check -print tests/slicing/loops.c

gives:
tests/slicing/loops.c:63:[kernel] failure: [AST Integrity Check] AST after normalization
                  statement stop();(35) in function stop_f1 has no successor.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0001740)
patrick (developer)
2011-04-12 16:08

A call to a function with no successor means the function makes no return, nor exit! Isn't it?
(0001742)
virgile (developer)
2011-04-12 21:05

Gcc's attribute noreturn means indeed that the called function will never give back control to its caller. That's why a call to such a function has no successor (the integrity checker is wrong here). In practice, an ACSL spec of such a function would always include ensures \false; (and quite often exits \true; though gcc's documentation mentions the fact that the function might in fact do a longjmp).
(0001743)
patrick (developer)
2011-04-13 08:08

Don't the kernel should add an "ensures \false;" to the specs of such function?
(0004807)

2014-02-12 16:59

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2011-04-12 15:05 patrick New Issue
2011-04-12 15:05 patrick Status new => assigned
2011-04-12 15:05 patrick Assigned To => Anne
2011-04-12 16:05 patrick Assigned To Anne => virgile
2011-04-12 16:05 patrick Category Plug-in > slicing => Kernel > ACSL implementation
2011-04-12 16:05 patrick Summary integrity problem on the exported AST => integrity problem of the AST on calls to functions with __attribute__ ((noreturn))
2011-04-12 16:05 patrick Description Updated
2011-04-12 16:05 patrick Additional Information Updated
2011-04-12 16:08 patrick Note Added: 0001740
2011-04-12 21:05 virgile Note Added: 0001742
2011-04-13 08:08 patrick Note Added: 0001743
2011-04-13 18:09 svn Checkin
2011-04-13 18:09 svn Status assigned => resolved
2011-04-13 18:09 svn Resolution open => fixed
2011-04-14 14:01 svn Checkin
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
2014-02-12 16:59 Note Added: 0004807
2014-02-12 16:59 Status closed => resolved


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker