Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000080Frama-CPlug-in > jessiepublic2009-05-11 17:022009-11-25 11:18
Reporterboris 
Assigned Tocmarche 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionduplicate 
PlatformOSOS Version
Product VersionFrama-C Lithium-20081201 
Target VersionFixed in Version 
Summary0000080: Assertion failed in jc_interp_misc.ml
DescriptionJessie crashes on code [1] with error message [2]. Environment: Windows XP, cygwin --------------------------------------- [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; } /*@ requires \valid(a+ (0..k)); */ void foo(int a[], int k) { Swap(&a[0], &a[k]); } [2] memory (mem-field(int_M),q_21) in memory set (mem-field(int_M),p_20), (mem-field(int_M),q_21) File "jc/jc_interp_misc.ml", line 707, characters 7-7: Uncaught exception: File "jc/jc_interp_misc.ml", line 707, characters 7-13: Assertion failed Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs tst2.cloc tst2.jc
Additional InformationThis bug is likely related to bug 38 http://bts.frama-c.com/view.php?id=38
TagsNo tags attached.
Attached Files

- Relationships
duplicate of 0000039confirmedcmarche Frama-C/Jessie: memory set problem 
has duplicate 0000303closedcmarche assign makes Jessie crash 

-  Notes
(0000511)
cmarche (developer)
2009-11-03 16:11

In Why 2.22, it will now pass the jessie phase but yields an invalid Why file (application creates an alias)
(0000576)
cmarche (developer)
2009-11-24 15:17

Julien, pourquoi tu fermes des bugs qui existent encore ?
(0000580)
cmarche (developer)
2009-11-25 10:11

I agree it is a duplicate of 0039

- Issue History
Date Modified Username Field Change
2009-05-11 17:02 boris New Issue
2009-05-11 19:52 signoles Status new => assigned
2009-05-11 19:52 signoles Assigned To => cmarche
2009-10-15 10:51 cmarche Status assigned => confirmed
2009-10-27 09:57 signoles Relationship added has duplicate 0000303
2009-11-03 16:11 cmarche Note Added: 0000511
2009-11-24 12:15 signoles Relationship added duplicate of 0000039
2009-11-24 14:15 signoles Status confirmed => closed
2009-11-24 14:15 signoles Resolution open => duplicate
2009-11-24 15:17 cmarche Note Added: 0000576
2009-11-24 15:17 cmarche Status closed => feedback
2009-11-24 15:17 cmarche Resolution duplicate => reopened
2009-11-25 10:11 cmarche Note Added: 0000580
2009-11-25 10:11 cmarche Status feedback => resolved
2009-11-25 10:11 cmarche Resolution reopened => duplicate
2009-11-25 11:18 signoles Status resolved => closed


Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker