AST check failure : problem with generated block-local variables
ID0001126: This issue was created automatically from Mantis Issue 1126. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001126 | Frama-C | Kernel | public | 2012-03-20 | 2014-02-12 |
| Reporter | pherrmann | Assigned To | virgile | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | Frama-C Oxygen-20120901 |
Description :
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.