← Back to branch summary

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

« back to all changes in this revision

Viewing changes to tests/misc/FP5.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/misc/FP5.c
 
1
/*@ requires \valid(b);
 
2
  @ requires \valid(c);
 
3
  @ assigns *b;
 
4
  @ assigns *c;
 
5
  @*/
 
6
void main(int a, int *b, int *c)
 
7
{
 
8
    int i=0;
 
9
    
 
10
    if (a==1)
 
11
    {
 
12
        *b=1;
 
13
        *c=1;
 
14
    }
 
15
    else if (a==-1)
 
16
    {
 
17
        *b=-1;
 
18
        *c=-1;
 
19
    }
 
20
    else
 
21
    {
 
22
        while (i<a)
 
23
        {
 
24
            *b=0;
 
25
            i++;
 
26
        }
 
27
        *c=0;
 
28
    }
 
29
 
 
30
}