Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000303Frama-CPlug-in > jessiepublic2009-10-26 16:432014-02-12 16:56
Reporterboris 
Assigned Tocmarche 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionduplicate 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090901 
Target VersionFixed in Version 
Summary0000303: assign makes Jessie crash
DescriptionCode [1] makes Jessie crash [2] on Beryllium-20090901. [1] /*@ requires \valid(p) && \valid(q); ensures *p == \old(*q); ensures *q == \old(*p); assigns *p, *q; */ void Swap(int *p, int *q) { int temp; temp = *p; *p = *q; *q = temp; } void Foo() { const int n=10; int a[n]; int i; for(i=0; i
Additional InformationSee also bug 80 http://bts.frama-c.com/view.php?id=80
TagsNo tags attached.
Attached Files

- Relationships
duplicate of 0000080closedcmarche Assertion failed in jc_interp_misc.ml 
duplicate of 0000039confirmedcmarche Frama-C/Jessie: memory set problem 

-  Notes
(0000493)
signoles (manager)
2009-10-27 09:58

The bug is still present in Beryllium-20090902 + Why-2.21. It seems that it is the very same bug that http://bts.frama-c.com/view.php?id=80.
(0000577)
cmarche (developer)
2009-11-24 15:19

Il faut eviter de declarer un bug comme duplicate sans en etre sur. Des fois le meme message peut sortir pour des raisons differentes.
(0000579)
cmarche (developer)
2009-11-25 10:10

I agree this is a duplicate of 0039 (and of 0080)

- Issue History
Date Modified Username Field Change
2009-10-26 16:43 boris New Issue
2009-10-27 09:57 signoles Relationship added duplicate of 0000080
2009-10-27 09:58 signoles Note Added: 0000493
2009-10-27 09:58 signoles Status new => assigned
2009-10-27 09:58 signoles Assigned To => cmarche
2009-11-24 14:15 signoles Relationship added duplicate of 0000039
2009-11-24 14:16 signoles Status assigned => closed
2009-11-24 14:16 signoles Resolution open => duplicate
2009-11-24 15:19 cmarche Note Added: 0000577
2009-11-24 15:19 cmarche Status closed => feedback
2009-11-24 15:19 cmarche Resolution duplicate => reopened
2009-11-25 10:10 cmarche Note Added: 0000579
2009-11-25 10:10 cmarche Status feedback => resolved
2009-11-25 10:10 cmarche Resolution reopened => duplicate
2009-11-25 11:18 signoles Status resolved => closed


Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker