Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002191Frama-CPlug-in > E-ACSLpublic2015-12-04 10:322017-01-18 15:09
Reporterkvorobyov 
Assigned Tosignoles 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Magnesium 
Target VersionFixed in VersionFrama-C 14-Silicon 
Summary0002191: Assertion failure when unrolling types of struct members
Description/* The following program leads to a failure of an assertion in translate.ml. The failure seems to be due to E-ACSL inability to determine the type of the term _G[0].str. */ struct ST { char *str; int num; }; struct ST _G[] = { { .str = "Struct_G[0]", .num = 99 }, { .str = "Struct_G[1]", .num = 147 } }; int main(int argc, char **argv) { /*@ assert \valid_read(_G[0].str); */ return 0; }
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0006344)
signoles (manager)
2017-01-18 15:09

Fixed in E-ACSL 0.8 compatible with Frama-C Silicon.

- Issue History
Date Modified Username Field Change
2015-12-04 10:32 kvorobyov New Issue
2015-12-04 10:32 kvorobyov Status new => assigned
2015-12-04 10:32 kvorobyov Assigned To => kvorobyov
2015-12-30 20:08 signoles Assigned To kvorobyov => signoles
2015-12-30 20:10 signoles Status assigned => confirmed
2016-09-09 11:31 kvorobyov Status confirmed => resolved
2017-01-18 15:09 signoles Fixed in Version => Frama-C 14-Silicon
2017-01-18 15:09 signoles Note Added: 0006344
2017-01-18 15:09 signoles Status resolved => closed


Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker