Frama-C Bug Tracking System - Frama-C
View Issue Details
0001161Frama-CPlug-in > jessiepublic2012-04-16 12:022012-04-17 22:12
nmuller 
cmarche 
normalfeaturealways
assignedopen 
Frama-C Nitrogen-20111001 
 
0001161: error in wp_behav.c
The following file does not pass the analysis (the resulting trace is supplied in additional informations)
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
No tags attached.
c wp_behav.c (1,145) 2012-04-16 12:02
https://bts.frama-c.com/file_download.php?file_id=379&type=bug
Issue History
2012-04-16 12:02nmullerNew Issue
2012-04-16 12:02nmullerStatusnew => assigned
2012-04-16 12:02nmullerAssigned To => virgile
2012-04-16 12:02nmullerFile Added: wp_behav.c
2012-04-17 17:51virgileNote Added: 0002933
2012-04-17 17:51virgileAssigned Tovirgile => cmarche
2012-04-17 17:51virgileSeverityminor => feature
2012-04-17 17:51virgileReproducibilityhave not tried => always
2012-04-17 17:51virgileCategoryKernel > ACSL implementation => Plug-in > jessie
2012-04-17 17:51virgileProduct VersionFrama-C Carbon-20110201 => Frama-C Hydrogen-20080301
2012-04-17 22:12yakobowskiProduct VersionFrama-C Hydrogen-20080301 => Frama-C Nitrogen-20111001

Notes
(0002933)
virgile   
2012-04-17 17:51   
The issue lies in the statement contract at line 62 of attached file: apparently Jessie (the compiler, not the plugin) does not support behavior with assumes clauses in this case.