← Back to branch summary

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

« back to all changes in this revision

Viewing changes to tests/jessie/ref.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/ref.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
 
 
26
 
 
27
/*@ requires \valid(p);
 
28
  @ assigns *p;
 
29
  @ ensures *p == 1;
 
30
  @*/
 
31
void g(int *p) {
 
32
  *p = 1;
 
33
}
 
34
 
 
35
/*@ assigns \empty;
 
36
  @ ensures \result == 1;
 
37
  @*/
 
38
int f() {
 
39
  int i;
 
40
  g(&i);
 
41
  return i;
 
42
}
 
43
 
 
44
/* 
 
45
Local Variables:
 
46
compile-command: "LC_ALL=C make ref"
 
47
End:
 
48
*/