← Back to branch summary

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

« back to all changes in this revision

Viewing changes to tests/jessie/zones2.c

  • Committer: Bazaar Package Importer
  • Author(s): Mehdi Dogguy
  • Date: 2009-06-03 08:19:25 UTC
  • Revision ID: james.westby@ubuntu.com-20090603081925-kihvxvt0wy3zc4ar
Tags: upstream-20081201.dfsg
Import upstream version 20081201.dfsg

Show diffs side-by-side

added added

removed removed

Lines of Context:
tests/jessie/zones2.c
 
1
/**************************************************************************/
 
2
/*                                                                        */
 
3
/*  The Why/Caduceus/Krakatoa tool suite for program certification        */
 
4
/*  Copyright (C) 2002-2006                                               */
 
5
/*    Jean-Fran�ois COUCHOT                                               */
 
6
/*    Mehdi DOGGUY                                                        */
 
7
/*    Jean-Christophe FILLI�TRE                                           */
 
8
/*    Thierry HUBERT                                                      */
 
9
/*    Claude MARCH�                                                       */
 
10
/*    Yannick MOY                                                         */
 
11
/*                                                                        */
 
12
/*  This software is free software; you can redistribute it and/or        */
 
13
/*  modify it under the terms of the GNU General Public                   */
 
14
/*  License version 2, as published by the Free Software Foundation.      */
 
15
/*                                                                        */
 
16
/*  This software is distributed in the hope that it will be useful,      */
 
17
/*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
 
18
/*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  */
 
19
/*                                                                        */
 
20
/*  See the GNU General Public License version 2 for more details         */
 
21
/*  (enclosed in the file GPL).                                           */
 
22
/*                                                                        */
 
23
/**************************************************************************/
 
24
 
 
25
struct S{ int x[1]; int y [2];}s;
 
26
 
 
27
/*@ ensures s.x[0] == 1; */
 
28
void f (){
 
29
  s.x[0] = 1;
 
30
  s.y[1] = 2;
 
31
}
 
32
 
 
33
 
 
34
typedef struct T {
 
35
  struct S *p;
 
36
} T;
 
37
 
 
38
T *t,*u;
 
39
 
 
40
 
 
41
int g() {
 
42
  return t->p->x[0] + u->p->x[0];
 
43
}
 
44
 
 
45
/* 
 
46
Local Variables:
 
47
compile-command: "LC_ALL=C make zones2"
 
48
End:
 
49
*/