← Back to branch summary

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

« back to all changes in this revision

Viewing changes to tests/jessie/dowhile.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/dowhile.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
C test file
 
28
 
 
29
*/
 
30
 
 
31
int x;
 
32
int i;
 
33
 
 
34
/*@ requires x >= 0;  ensures x == 10; */
 
35
void main()
 
36
{
 
37
  x = 0;
 
38
  i = 10;
 
39
  /*@ loop invariant x == 10 - i && 10 >= i > 0; loop variant i; */
 
40
  do {
 
41
    x = x + 1;
 
42
    i = i - 1;
 
43
  } while (i > 0);
 
44
}
 
45
 
 
46
 
 
47
/* 
 
48
Local Variables:
 
49
compile-command: "LC_ALL=C make dowhile"
 
50
End:
 
51
*/