Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000846Frama-CPlug-in > jessiepublic2011-05-30 17:382011-05-30 17:38
ReporterJochen 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in Version 
Summary0000846: array access in "decreases"-clause causes "Unexpected internal region in logic"
DescriptionJessie reports an uncaught exception: Failure("Unexpected internal region in logic") on the attached file. That message vanishes if either - the array access "b[f]" in line 4 is replaced e.g. by "0", - the "decreases" clause in line 8 is deleted, or - the recursive call in line 11 is deleted. (The code is nonsensical, but has been boiled down from a reasonable program.)
TagsNo tags attached.
Attached Filesc file icon ftest.c [^] (200 bytes) 2011-05-30 17:38 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

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


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker