2020-12-04 23:43 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001225Frama-CPlug-in > wppublic2012-09-19 17:16
Reporterboris 
Assigned Tosignoles 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
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
+Relationships

-Notes

~0003211

virgile (developer)

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)

Last edited: 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)

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

-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
+Issue History