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

« back to all changes in this revision

Viewing changes to tests/spec/complete_behaviors.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/spec/complete_behaviors.c

 

1

typedef enum { Max, Min } kind;

 

2

int extremum (kind k, int x, int y) {

 

3

  return ((k == Max ? x > y : x < y) ? x: y);

 

4

}

 

5

/*@ requires k == Max || k == Min;

 

6

    assigns \nothing;

 

7

    ensures \result == x || \result == y;

 

8

    behavior is_max:

 

9

      assumes k == Max;

 

10

      ensures \result >= x && \result >= y;

 

11

    behavior is_min:

 

12

      assumes k == Min;

 

13

      ensures \result <= x && \result <= y;

 

14

    complete behaviors is_max, is_min;

 

15

    disjoint behaviors is_max, is_min;

 

16

*/

 

17

int extremum (kind k, int x, int y);

• Older »

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