| Anonymous | Login | Signup for a new account | 2019-08-17 13:55 CEST |  |
| Main | My View | View Issues | Change Log | Roadmap | Repositories |
| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
| 0000672 | Frama-C | Kernel | public | 2011-01-17 14:55 | 2012-09-19 17:16 | ||||
| Reporter | yakobowski | ||||||||
| Assigned To | virgile | ||||||||
| Priority | normal | Severity | crash | Reproducibility | always | ||||
| Status | closed | Resolution | fixed | ||||||
| Platform | OS | OS Version | |||||||
| Product Version | Frama-C Carbon-20101202-beta2 | ||||||||
| Target Version | Fixed in Version | Frama-C Oxygen-20120901 | |||||||
| Summary | 0000672: Incorrect cil merging in presence of ACSL annotations | ||||||||
| 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. | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |  files.tgz [^] (374 bytes) 2011-01-17 14:55 | ||||||||
 Relationships |
|
 Relationships |
|
Notes |
|
|
(0002400) virgile (developer) 2011-10-19 16:01 |
- Only two files are necessary (builtin.h and main.c) - There are at least two issues: the presence of a prototype for Frama_C_nondet in main.c will trigger a different check issue than without. |
|
Notes |
|
Issue History |
|||
| Date Modified | Username | Field | Change |
| 2011-01-17 14:55 | yakobowski | New Issue | |
| 2011-01-17 14:55 | yakobowski | File Added: files.tgz | |
| 2011-01-17 15:10 | signoles | Status | new => assigned |
| 2011-01-17 15:10 | signoles | Assigned To | => virgile |
| 2011-10-19 16:01 | virgile | Note Added: 0002400 | |
| 2011-10-19 16:01 | virgile | Status | assigned => acknowledged |
| 2011-10-20 14:41 | svn | Checkin | |
| 2011-10-20 14:41 | svn | Status | acknowledged => resolved |
| 2011-10-20 14:41 | svn | Resolution | open => fixed |
| 2012-09-19 17:15 | signoles | Fixed in Version | => Frama-C Oxygen-20120901 |
| 2012-09-19 17:16 | signoles | Status | resolved => closed |
|
Issue History |
| Copyright © 2000 - 2019 MantisBT Team |
|