ID0002201: **This issue was created automatically from Mantis Issue 2201. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002201 | Frama-C | Plug-in > wp | public | 2016-01-22 | 2016-06-21 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | rcl | **Assigned To** | correnson | **Resolution** | fixed | | **Priority** | normal | **Severity** | minor | **Reproducibility** | always | | **Platform** | Linux | **OS** | Ubuntu | **OS Version** | 14.04 | | **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium | ### 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. ## Attachments - [test.c](/uploads/1538550928d60f17405b687f59ab5e2b/test.c)