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

« back to all changes in this revision

Viewing changes to tests/jessie/dillon5.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/dillon5.c

 

1

 

 

2

typedef struct { int a; } las2;

 

3

typedef struct { las2 s; } las1;

 

4

 

 

5

//@ predicate inv{L}(las1 * v) = \valid(v) ==> \valid(&(v->s));

 

6

 

 

7

las1 v1;

 

8

 

 

9

/*@

 

10

  @requires \valid(v2);

 

11

@assigns v2->a;

 

12

@ensures v2->a==3;

 

13

*/

 

14

void g(las2 * v2)

 

15

{

 

16

v2->a = 3;

 

17

}

 

18

 

 

19

/*@

 

20

requires \valid(&v1.s);

 

21

assigns v1.s.a;

 

22

ensures v1.s.a==3;

 

23

*/

 

24

int main()

 

25

{

 

26

g(&v1.s);

 

27

return v1.s.a;

 

28

}

• Older »

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