← Back to branch summary

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

« back to all changes in this revision

Viewing changes to tests/slicing/unravel-point.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/slicing/unravel-point.c
 
1
/* run.config
 
2
   GCC:
 
3
   OPT: -slice-print -calldeps -slice-return send1 -journal-disable
 
4
   OPT: -slice-print -calldeps -slice-return send2 -journal-disable
 
5
   OPT: -slice-print -calldeps -slice-return send3 -journal-disable
 
6
   OPT: -slice-print -calldeps -slice-return send4 -journal-disable
 
7
 
 
8
 
 
9
 
 
10
 
 
11
 
 
12
 
 
13
 
 
14
 
 
15
   */
 
16
 
 
17
/* Small example devired from examples given for UNRAVEL tool : */
 
18
 
 
19
 
 
20
 
 
21
/*@ assigns *p \from \empty;
 
22
    assigns \result ; */
 
23
int scanf (char const *, int * p);
 
24
 
 
25
 
 
26
 
 
27
int printf (char const *, int);
 
28
 
 
29
 
 
30
 
 
31
 
 
32
 
 
33
 
 
34
 
 
35
 
 
36
int send1 (int x) {
 
37
  printf ("%d\n", x) ;
 
38
  return x;
 
39
}
 
40
int send2 (int x) {
 
41
  printf ("%d\n", x) ;
 
42
  return x;
 
43
}
 
44
int send3 (int x) {
 
45
  printf ("%d\n", x) ;
 
46
  return x;
 
47
}
 
48
int send4 (int x) {
 
49
  printf ("%d\n", x) ;
 
50
  return x;
 
51
}
 
52
 
 
53
main()
 
54
{
 
55
        int             input1,input2,input3,cond1,cond2;
 
56
        int             a,b,c;
 
57
        int             *x,*y,*z;
 
58
        int             output1,output2,output3;
 
59
 
 
60
        scanf("%d",&input1);
 
61
        a = input1;
 
62
        scanf("%d",&input2);
 
63
        b = input2;
 
64
        scanf("%d",&input3);
 
65
        c = input3;
 
66
        scanf("%d",&cond1);
 
67
        scanf("%d",&cond2);
 
68
        x = &a;
 
69
        if (cond1) x = &b;
 
70
        y = &c;
 
71
        z = &b;
 
72
        output2 = *z + 1;
 
73
        *z = *y + *x;
 
74
        output1 = *z;
 
75
        output3 = *x;
 
76
        send1 (output1);
 
77
        send2 (output2);
 
78
        send3 (output3);
 
79
        send4 (cond2);
 
80
}