0000332: goto generated by Frama-C and not supported by Jessie

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0000332

Frama-C

Kernel

public

2009-11-17 17:01

2010-04-13 15:33

Reporter

dpariente

Assigned To

virgile

Priority

normal

Severity

minor

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C GIT, precise the release id

Target Version

Fixed in Version

Frama-C Boron-20100401

Summary

0000332: goto generated by Frama-C and not supported by Jessie

Description

When slicing (or simply analyzing) a function like the following one: void f(int*p,int e,int t,int f,int r) { *p = ( (e || (t && f)) && (t || f) ); } Frama-C translates it into: /* Generated by Frama-C */ void f(int *p , int e , int t , int f_0 , int r ) { int tmp ; if (e) { goto _LOR; } else { if (t) { if (f_0) { _LOR: /* internal */ ; if (t) { tmp = 1; } else { if (f_0) { tmp = 1; } else { tmp = 0; } } } else { tmp = 0; } } else { tmp = 0; } } *p = tmp; return; } with a goto to a inner block. But Jessie doesn't support this feature: File "slicef.jc", line 42, characters 7-16: unsupported goto (backward or to some inner block) Category of this report is "kernel" as it is let up to Frama-C team to choose between an evolution of Jessie (in order to take this feature into account) or a change in the way the Kernel (CIL) transforms boolean equations.

Tags

No tags attached.

Attached Files

Relationships

Notes
(0000619) virgile (developer) 2010-01-12 18:36	Jessie relies on ad'hoc normalization of C code, which it sets when -jessie is enabled. If it used on code pretty-printed by frama-c and re-parsed, the ad'hoc normalization phase is no longer possible (it must occur at the first parsing). A new option -jessie-adhoc-normalization will force such normalization even if the jessie analysis is not triggered (allowing for instance a slicing phase before it). Is this an acceptable work-around?

(0000620) dpariente (reporter) 2010-01-12 19:08	At a first glance, it seems OK. Thanks.

Issue History
Date Modified	Username	Field	Change
2009-11-17 17:01	dpariente	New Issue
2010-01-12 18:36	virgile	Note Added: 0000619
2010-01-12 18:36	virgile	Status	new => feedback
2010-01-12 19:08	dpariente	Note Added: 0000620
2010-01-13 17:01	virgile	Status	feedback => resolved
2010-01-13 17:01	virgile	Resolution	open => fixed
2010-01-13 17:01	virgile	Assigned To	=> virgile
2010-04-13 15:30	signoles	Status	resolved => new
2010-04-13 15:31	signoles	Status	new => closed
2010-04-13 15:33	signoles	Fixed in Version	=> Frama-C Boron