Upgrading WP causes crash in Jessie
ID0001225: This issue was created automatically from Mantis Issue 1225. Further discussion may take place here.
Id | Project | Category | View | Due Date | Updated |
---|---|---|---|---|---|
ID0001225 | Frama-C | Plug-in > wp | public | 2012-07-02 | 2012-09-19 |
Reporter | boris | Assigned To | signoles | Resolution | fixed |
Priority | normal | Severity | crash | Reproducibility | always |
Platform | - | OS | - | OS Version | - |
Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | Frama-C Oxygen-20120901 |
Description :
I 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.