Incorrect cil merging in presence of ACSL annotations
ID0000672: This issue was created automatically from Mantis Issue 672. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000672 | Frama-C | Kernel | public | 2011-01-17 | 2012-09-19 |
| Reporter | yakobowski | Assigned To | virgile | Resolution | fixed |
| Priority | normal | Severity | crash | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Carbon-20101202-beta2 | Target Version | - | Fixed in Version | Frama-C Oxygen-20120901 |
Description :
Launching Frama-C on the three attached files with the -check option causes a crash with the error builtin.h:6:[kernel] failure: [AST Integrity Check] initial ASTlogic variable Frama_C_entropy_source(728) is not declared
Additional Information :
Command-line: frama-c builtin.h builtin.c main.c -check
Three different files seem to be needed. The error also depends on the order the files are passed on the command line.