Frama-C Bug Tracking System - Frama-C
View Issue Details
0000790Frama-CKernel > ACSL implementationpublic2011-04-12 15:052014-02-12 16:59
normalminorhave not tried
Frama-C GIT, precise the release id 
Frama-C Nitrogen-20111001 
0000790: integrity problem of the AST on calls to functions with __attribute__ ((noreturn))
Calls 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?
The 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.
No tags attached.
Issue History
2011-04-12 15:05patrickNew Issue
2011-04-12 15:05patrickStatusnew => assigned
2011-04-12 15:05patrickAssigned To => Anne
2011-04-12 16:05patrickAssigned ToAnne => virgile
2011-04-12 16:05patrickCategoryPlug-in > slicing => Kernel > ACSL implementation
2011-04-12 16:05patrickSummaryintegrity problem on the exported AST => integrity problem of the AST on calls to functions with __attribute__ ((noreturn))
2011-04-12 16:05patrickDescription Updated
2011-04-12 16:05patrickAdditional Information Updated
2011-04-12 16:08patrickNote Added: 0001740
2011-04-12 21:05virgileNote Added: 0001742
2011-04-13 08:08patrickNote Added: 0001743
2011-04-13 18:09svnCheckin
2011-04-13 18:09svnStatusassigned => resolved
2011-04-13 18:09svnResolutionopen => fixed
2011-04-14 14:01svnCheckin
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed
2014-02-12 16:59Note Added: 0004807
2014-02-12 16:59Statusclosed => resolved

2011-04-12 16:08   
A call to a function with no successor means the function makes no return, nor exit! Isn't it?
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).
2011-04-13 08:08   
Don't the kernel should add an "ensures \false;" to the specs of such function?
2014-02-12 16:59   
Fix committed to stable/neon branch.