Frama-C Bug Tracking System - Frama-C
View Issue Details
0001126Frama-CKernelpublic2012-03-20 11:082014-02-12 16:59
pherrmann 
virgile 
normalminoralways
closedfixed 
Frama-C GIT, precise the release id 
Frama-C Oxygen-20120901 
0001126: AST check failure : problem with generated block-local variables
On submitted file : frama-c -check failchek.c produces failcheck.c:40:[kernel] failure: [AST Integrity Check] initial AST In function _gnutls_epoch_set_cipher_suite, variable tmp_0 is supposed to be local to a block but not mentioned in function's locals. [kernel] error occurring when exiting Frama-C: stopping exit procedure. Also, use of frama-c failcheck -print -then -check does not produce the problem, while frama-c failcheck.c -then -check does, thus -print seems to have an unintended side-effect.
No tags attached.
c failcheck.c (1,447) 2012-03-20 11:08
https://bts.frama-c.com/file_download.php?file_id=359&type=bug
Issue History
2012-03-20 11:08pherrmannNew Issue
2012-03-20 11:08pherrmannFile Added: failcheck.c
2012-03-20 21:05yakobowskiStatusnew => assigned
2012-03-20 21:05yakobowskiAssigned To => virgile
2012-03-30 16:44svnCheckin
2012-03-30 16:44svnStatusassigned => resolved
2012-03-30 16:44svnResolutionopen => fixed
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed
2014-02-12 16:59Note Added: 0004708
2014-02-12 16:59Statusclosed => resolved

Notes
(0004708)
   
2014-02-12 16:59   
Fix committed to stable/neon branch.