assigns crash on incorrect locations
ID0001844: This issue was created automatically from Mantis Issue 1844. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001844 | Frama-C | Plug-in > wp | public | 2014-07-17 | 2014-07-17 |
| Reporter | boulme | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | crash | Reproducibility | always |
| Platform | - | OS | Linux Ubuntu 14.04 LTS | OS Version | - |
| Product Version | Frama-C Neon-20140301 | Target Version | - | Fixed in Version | - |
Description :
On the file "crash_assigns.c", an invalid assign clause makes wp crash with the message:
Current source was: crash_assigns.c:5 The full backtrace is: Raised at file "hashtbl.ml", line 353, characters 18-27 Called from file "hashtbl.ml", line 361, characters 22-38
Plug-in wp aborted: internal error. Please report as 'crash' at http://bts.frama-c.com/. Your Frama-C version is Neon-20140301.
Additional Information :
Replacing the invalid assigns clause with a valid one like assigns t[0..9]; makes the pb disappear...
Steps To Reproduce :
run frama-c-gui crash_assigns.c
and try to prove assigns clause using wp.
Attachments
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information