0001281: do { ... } while (0) pattern causes wp to fail

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0001281

Frama-C

Plug-in > wp

public

2012-10-15 08:37

2014-02-05 17:45

Reporter

sjw

Assigned To

correnson

Priority

normal

Severity

minor

Reproducibility

always

Status

acknowledged

Resolution

open

Platform

OS Version

Product Version

Frama-C Oxygen-20120901

Target Version

Fixed in Version

Summary

0001281: do { ... } while (0) pattern causes wp to fail

Description

The pattern do { ... } while (0) is used in a number of standard headers
to allow pre-processor macros to introduce a scope and still look like
a statement (you can put a semi-colon after them). This translates to
something like while(1) { ...; break; } as in the following

/*@ requires \valid(x);
   @ ensures \result == 0; */
int foo(int *x) {

    /* loop invariant 0 == 0; */
    while( 1 ) {
        *x = 0;
        break;
   }

    return *x;
}

which fails with
$ frama-c -wp do_while_test.c
[kernel] preprocessing with "gcc -C -E -I. do_while_test.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
do_while_test.c:6:[wp] warning: calculus failed on strategy
              for 'foo', behavior 'default!', all properties, both assigns or not because
              unsupported non-natural loop without invariant property. (abort)
[wp] 0 goal scheduled

It looks like the unconditional break (i.e., the results of optimising
if (!0) break; from the translation of the 'do') causes the cil2cfg pass
to throw out some loop edges, causing the above error.

Tags

No tags attached.

Attached Files

Relationships

Notes
(0004510) correnson (manager) 2014-02-05 17:00	To be fixed with the restructuration of WP calculus.

Issue History
Date Modified	Username	Field	Change
2012-10-15 08:37	sjw	New Issue
2012-10-15 08:37	sjw	Status	new => assigned
2012-10-15 08:37	sjw	Assigned To	=> correnson
2014-02-05 17:00	correnson	Note Added: 0004510
2014-02-05 17:01	correnson	Status	assigned => acknowledged
2014-02-05 17:45	correnson	Relationship added	has duplicate 0001491