ID0002126: **This issue was created automatically from Mantis Issue 2126. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002126 | Frama-C | Plug-in > wp | public | 2015-06-02 | 2016-01-26 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | virgile | **Assigned To** | correnson | **Resolution** | fixed | | **Priority** | normal | **Severity** | major | **Reproducibility** | always | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Magnesium | ### Description : On the example source below, frama-c -wp reduced.i crashes with the following error: File "src/wp/MemVar.ml", line 491, characters 54-60: Assertion failed Apparently (by inferring why the offending function in MemVar got called), the p1+0 in the assigns for fn1 leads WP to think that p1 should be instantiated with an array (in particular, if you remove the +0, everything is fine). -- reduced.i /*@ assigns *(p1); */ int fn1(char *p1); /*@ assigns \nothing; */ void fn2(void) { char pcr_index; fn1(&pcr_index); }