Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001844Frama-CPlug-in > wppublic2014-07-17 22:412014-07-17 22:41
Reporterboulme 
Assigned Tocorrenson 
PrioritynormalSeveritycrashReproducibilityalways
StatusassignedResolutionopen 
PlatformOSLinux Ubuntu 14.04 LTSOS Version
Product VersionFrama-C Neon-20140301 
Target VersionFixed in Version 
Summary0001844: assigns crash on incorrect locations
DescriptionOn the file "crash_assigns.c",
an invalid assign clause makes wp crash with the message:
 
Current source was: crash_assigns.c:5
The full backtrace is:
Raised at file "hashtbl.ml", line 353, characters 18-27
Called from file "hashtbl.ml", line 361, characters 22-38

Plug-in wp aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/. [^]
Your Frama-C version is Neon-20140301.
Steps To Reproducerun frama-c-gui crash_assigns.c

and try to prove assigns clause using wp.
Additional InformationReplacing the invalid assigns clause with a valid one like
  assigns t[0..9];
makes the pb disappear...
TagsNo tags attached.
Attached Filesc file icon crash_assigns.c [^] (77 bytes) 2014-07-17 22:41 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2014-07-17 22:41 boulme New Issue
2014-07-17 22:41 boulme Status new => assigned
2014-07-17 22:41 boulme Assigned To => correnson
2014-07-17 22:41 boulme File Added: crash_assigns.c


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker