ID0001161: **This issue was created automatically from Mantis Issue 1161. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0001161 | Frama-C | Plug-in > jessie | public | 2012-04-16 | 2012-04-17 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | nmuller | **Assigned To** | cmarche | **Resolution** | open | | **Priority** | normal | **Severity** | feature | **Reproducibility** | always | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | - | ### Description : The following file does not pass the analysis (the resulting trace is supplied in additional informations) ### Additional Information : frama-c -jessie -jessie-atp alt-ergo wp_behav1.c [kernel] preprocessing with "gcc -C -E -I. -dD wp_behav1.c" [jessie] Starting Jessie translation [jessie] Producing Jessie files in subdir wp_behav1.jessie [jessie] File wp_behav1.jessie/wp_behav1.jc written. [jessie] File wp_behav1.jessie/wp_behav1.cloc written. [jessie] Calling Jessie tool in subdir wp_behav1.jessie Generating Why function f Generating Why function min Generating Why function bhv Generating Why function stmt_contract Generating Why function local_named_behavior File "jc/jc_interp.ml", line 2965, characters 7-7: Uncaught exception: File "jc/jc_interp.ml", line 2965, characters 7-13: Assertion failed [jessie] user error: Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs wp_behav1.cloc wp_behav1.jc ## Attachments - [wp_behav.c](/uploads/45b3d49d954bf8c924296a15770d19d5/wp_behav.c)