Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001225Frama-CPlug-in > wppublic2012-07-02 15:352012-09-19 17:16
Reporterboris 
Assigned Tosignoles 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001225: Upgrading WP causes crash in Jessie
DescriptionI just upgraded WP to 0.5 and I've discovered that Jessie crashes on a file that shouldn't cause any problems:

[kernel] preprocessing with "gcc -C -E -I. -dD test-pc4.c"
[jessie] Starting Jessie translation
[kernel] The full backtrace is:
         Called from file "src/project/state_builder.ml", line 439, characters 10-31
         Called from file "src/project/project.ml", line 119, characters 28-67
         Called from file "hashtbl.ml", line 157, characters 23-35
         Called from file "hashtbl.ml", line 161, characters 12-33
         Called from file "src/project/project.ml", line 116, characters 6-364
         Called from file "list.ml", line 69, characters 12-15
         Called from file "src/lib/qstack.ml", line 107, characters 4-23
         Called from file "src/kernel/file.ml", line 1376, characters 2-33
         Called from file "register.ml", line 96, characters 4-93
         Called from file "register.ml", line 290, characters 6-12
         Called from file "queue.ml", line 134, characters 6-20
         Called from file "src/kernel/boot.ml", line 36, characters 4-20
         Called from file "src/kernel/cmdline.ml", line 723, characters 2-9
         Called from file "src/kernel/cmdline.ml", line 200, characters 4-8
         
         Unexpected error (File "src/type/datatype.ml", line 98, characters 18-24: Assertion failed).

I called Jessie with frama-c -jessie -jessie-atp=gui -pp-annot. Both why2 and why3 are installed.

Everything works with Jessie after I uninstalled WP-0.5 and reinstalled Nitrogen from scratch.

This is strange since an update of WP should only affect files in src/wp.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0003211)
virgile (developer)
2012-07-03 09:53

I'm not able to reproduce the issue on a random C source. Could you provide a file that shows the issue?
(0003212)
signoles (manager)
2012-07-03 09:55
edited on: 2012-07-03 09:56

I just reproduced this issue with a random C file by running:
$ frama-c -jessie test.c

The issue is the definition of module VarUsage.Domain in WP 0.5. Under investigation to see if the issue is still present in the development version.

(0003213)
signoles (manager)
2012-07-03 10:22

Already fixed in the current development version. Will be part of Frama-C Oxygen.

- Issue History
Date Modified Username Field Change
2012-07-02 15:35 boris New Issue
2012-07-02 15:35 boris Status new => assigned
2012-07-02 15:35 boris Assigned To => cmarche
2012-07-03 09:02 signoles Assigned To cmarche => signoles
2012-07-03 09:53 virgile Note Added: 0003211
2012-07-03 09:53 virgile Assigned To signoles =>
2012-07-03 09:53 virgile Status assigned => feedback
2012-07-03 09:55 signoles Note Added: 0003212
2012-07-03 09:55 signoles Assigned To => signoles
2012-07-03 09:55 signoles Status feedback => confirmed
2012-07-03 09:56 signoles Category Plug-in > jessie => Plug-in > wp
2012-07-03 09:56 signoles Note Edited: 0003212
2012-07-03 10:22 signoles Note Added: 0003213
2012-07-03 10:22 signoles Status confirmed => resolved
2012-07-03 10:22 signoles Fixed in Version => Frama-C Oxygen-2012xx01
2012-07-03 10:22 signoles Resolution open => fixed
2012-09-19 17:16 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker