View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0002201 | Frama-C | Plug-in > wp | public | 2016-01-22 12:29 | 2016-06-21 14:08 | ||||
Reporter | rcl | ||||||||
Assigned To | correnson | ||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Platform | Linux | OS | Ubuntu | OS Version | 14.04 | ||||
Product Version | Frama-C Sodium | ||||||||
Target Version | Fixed in Version | Frama-C Aluminium | |||||||
Summary | 0002201: Unexpected error (Invalid_argument("Z.shift_left: count argument must be positive")) | ||||||||
Description | With the help of a custom csmith variant, a program was discovered that causes an unexpected error in the wp plugin. The following program is a reduced minimal example of the failing program discovered by csmith: /*@ assigns \nothing; */ int main() { int foo = 1; 1 & (foo & 0x80000000000001LL) << 1; return 0; } The crash message is: Raised at file "src/wp/register.ml", line 579, characters 30-32 Called from file "queue.ml", line 134, characters 6-20 Called from file "src/kernel/boot.ml", line 37, characters 4-20 Called from file "src/kernel/cmdline.ml", line 763, characters 2-9 Called from file "src/kernel/cmdline.ml", line 216, characters 4-8 Unexpected error (Invalid_argument("Z.shift_left: count argument must be positive")). Please report as 'crash' at http://bts.frama-c.com/. Your Frama-C version is Sodium-20150201. | ||||||||
Steps To Reproduce | Save the aforementioned program into a file named test.c, then execute frama-c -wp test.c to cause the crash. | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2016-01-22 12:29 | rcl | New Issue | |
2016-01-22 12:29 | rcl | Status | new => assigned |
2016-01-22 12:29 | rcl | Assigned To | => correnson |
2016-01-22 12:29 | rcl | File Added: test.c | |
2016-01-25 09:38 | correnson | Assigned To | correnson => patrick |
2016-01-26 11:16 | patrick | Status | assigned => confirmed |
2016-01-26 12:07 | patrick | Source_changeset_attached | => framac master ac3d0437 |
2016-01-26 12:07 | correnson | Source_changeset_attached | => framac master a78cc759 |
2016-01-26 12:07 | correnson | Note Added: 0006123 | |
2016-01-26 12:07 | correnson | Assigned To | patrick => correnson |
2016-01-26 12:07 | correnson | Status | confirmed => resolved |
2016-01-26 12:07 | correnson | Resolution | open => fixed |
2016-06-21 14:08 | signoles | Fixed in Version | => Frama-C Aluminium |
2016-06-21 14:08 | signoles | Status | resolved => closed |