Frama-C Bug Tracking System - Frama-C
View Issue Details
0001632Frama-CKernel > ACSL implementationpublic2014-01-27 09:212014-10-29 11:05
virgile 
virgile 
lowminoralways
assignedopen 
Frama-C GIT, precise the release id 
 
0001632: Translation of abrupt clause into assert do not take 'for :' clause into account
In the program written given below, the returns clause is translated into two assert that are not related to the foo behavior, resulting in an unprovable assertion in the else branch.
/*@ behavior foo: assumes a == 0; */ int foo(int a) { /*@ for foo: returns \result == 0; */ { if (a==0) { return 0; } else return 2; } }
No tags attached.
Issue History
2014-01-27 09:21virgileNew Issue
2014-01-27 09:21virgileStatusnew => assigned
2014-01-27 09:21virgileAssigned To => virgile
2014-10-29 11:05rajshuklaTag Attached: Windows
2014-10-29 11:05rajshuklaTag Attached: csmith
2014-10-29 11:05rajshuklaTag Detached: Windows
2014-10-29 11:05rajshuklaTag Detached: csmith

There are no notes attached to this issue.