2021-03-01 04:45 CET

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

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




patrick (developer)

A call to a function with no successor means the function makes no return, nor exit! Isn't it?


virgile (developer)

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).


patrick (developer)

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


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
2011-04-13 18:09 svn Status assigned => resolved
2011-04-13 18:09 svn Resolution open => fixed
2011-04-14 14:01 svn
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
2013-12-19 01:12 patrick Source_changeset_attached => framac master 43f5c70f
2013-12-19 01:12 Source_changeset_attached => framac master 23598dbf
2014-02-12 16:54 patrick Source_changeset_attached => framac stable/neon 43f5c70f
2014-02-12 16:54 Source_changeset_attached => framac stable/neon 23598dbf
2014-02-12 16:59 Note Added: 0004807
2014-02-12 16:59 Status closed => resolved
+Issue History