Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000813Frama-CPlug-in > jessiepublic2011-05-09 12:322011-05-09 12:32
ReporterJochen 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in Version 
Summary0000813: struct dereferencing causes uncaught exception
DescriptionJessie reports an uncaught exception "Unexpected internal region in logic" when run on the attached program.

If the definition of "IsList" is expanded, i.e. if line 16 is used as the contract rather than line 15, the error message changes to "Unbound variable _elem_next_Last_12", coming from why. This behavior resembles to that reported in issue 0000811.

If axiom a1 in line 8 is activated rather than commented out, the error disappears in both cases (contract line 15/16).
TagsNo tags attached.
Attached Filesc file icon ftest.c [^] (438 bytes) 2011-05-09 12:32 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2011-05-09 12:32 Jochen New Issue
2011-05-09 12:32 Jochen Status new => assigned
2011-05-09 12:32 Jochen Assigned To => cmarche
2011-05-09 12:32 Jochen File Added: ftest.c


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker