~ubuntu-branches/debian/sid/frama-c/sid

« back to all changes in this revision

Viewing changes to tests/jessie/behavior.c

• browse files at revision 1
• compare with another revision
• download diff
• download tarball
• view history from revision 1

Show diffs side-by-side

added

removed

tests/jessie/behavior.c

 

1

int x;

 

2

 

 

3

/*@ behavior one:

 

4

  @   assumes x == 1;

 

5

  @   ensures x == 10;

 

6

  @*/

 

7

void f(int z) {

 

8

  if (z)

 

9

    //@ for one: loop invariant 1 <= x <= 10;

 

10

    while (x < 10) x++;

 

11

  else

 

12

    //@ for one: assert x == 1;

 

13

    x = 10;

 

14

}

 

15

 

 

16

/*

 

17

Local Variables:

 

18

compile-command: "LC_ALL=C make behavior"

 

19

End:

 

20

*/

• Older »

Loggerhead is a web-based interface for Breezy
Version: 2.0.1