error in wp_behav.c
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