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

« back to all changes in this revision

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

 

1

/* run.config

 

2

   DONTRUN: FS#394

 

3

*/

 

4

typedef struct { int a; } las;

 

5

las * p;

 

6

//@ logic las** p_ref{L} = &p;

 

7

 

 

8

/*@

 

9

requires \valid(p);

 

10

assigns p->a;

 

11

*/

 

12

void f3()

 

13

{ p->a = 5; }

 

14

 

 

15

/*@

 

16

requires \valid(p);

 

17

assigns (*p_ref)->a;

 

18

*/

 

19

void g3(int * p)

 

20

{ f3(); }

 

21

 

 

22

/* 

 

23

Local Variables:

 

24

compile-command: "LC_ALL=C make -j dillon2"

 

25

End:

 

26

*/

• Older »

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