← Back to branch summary

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

« back to all changes in this revision

Viewing changes to tests/sparecode/intra.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/sparecode/intra.c
 
1
/* run.config
 
2
   OPT: -sparecode-analysis -journal-disable
 
3
   OPT: -slicing-level 2 -slice-return main -slice-print -journal-disable
 
4
   OPT: -main main2 -sparecode-analysis -journal-disable
 
5
   OPT: -main main2 -slice-return main2 -slice-print -journal-disable
 
6
   OPT: -main main2 -slice-return main2 -slice-assert f10 -slice-print -journal-disable
 
7
*/
 
8
 
 
9
/* Waiting for results such as:
 
10
 * spare code analysis removes statements having variables with
 
11
 * prefix "spare_"
 
12
 *
 
13
 * slicing analysis removes statement having variables with
 
14
 * prefix "spare_" and "any_"
 
15
 */
 
16
 
 
17
int G;
 
18
 
 
19
int tmp (int a) {
 
20
  int x = a;
 
21
  //@ assert x == a ;
 
22
  int w = 1;
 
23
  //@ assert w == 1 ; // w is not spare or else
 
24
                      // the assertion should be removed !
 
25
  int spare_z = 1;
 
26
  int spare_y = a+spare_z;
 
27
  return x;
 
28
}
 
29
 
 
30
int param (int a, int spare_b) {
 
31
  return a;
 
32
}
 
33
 
 
34
int spare_called_fct (int a) {
 
35
  return a;
 
36
}
 
37
 
 
38
int two_outputs (int a, int b) {
 
39
  G += b;
 
40
  return a;
 
41
}
 
42
 
 
43
int call_two_outputs (void) {
 
44
  int x, spare_y;
 
45
  int any_b = 1;
 
46
  int any_a = 2;
 
47
  int a = 1;
 
48
  int b = any_b;
 
49
  x = two_outputs (a, b);
 
50
  G = 1; /* don't use b = any_b; */
 
51
  b = 2;
 
52
  a = any_a;
 
53
  spare_y = two_outputs (a, b);
 
54
      /* don't use spare_y so don't use a = any_a */
 
55
  return x;
 
56
}
 
57
 
 
58
void assign (int *p, int *q) {
 
59
  *p = *q ;
 
60
}
 
61
 
 
62
int loop (int x, int y, int z) {
 
63
  int i = 0;
 
64
  //@ assert i < z ;
 
65
  //@ loop invariant i < y ;
 
66
  /* should keep y in sparecode analysis even if it is not used in the function */
 
67
  while (i < x) {
 
68
    i ++;
 
69
  }
 
70
  return i;
 
71
}
 
72
 
 
73
void stop(void) __attribute__ ((noreturn)) ;
 
74
 
 
75
int main (int noreturn, int halt) {
 
76
  int res = 0;
 
77
  int spare_tmp = 3;
 
78
  int spare_param = 2 + spare_tmp;
 
79
  int spare_ref = 3;
 
80
  int x = 1;
 
81
  int y = 2;
 
82
  res += param (2, spare_param);
 
83
  res += tmp (4);
 
84
  spare_called_fct (5);
 
85
  res += call_two_outputs ();
 
86
  res += loop (10, 15, 20);
 
87
  assign (&x, &spare_ref) ; /* <- Here, best can be done for spare analysis */
 
88
  assign (&x, &y) ;
 
89
  if (noreturn) {
 
90
    if (halt)
 
91
      stop () ;
 
92
    else
 
93
      while (1);
 
94
    //@ assert \false ; // What should be done with
 
95
                        // assertions related to dead code?
 
96
    }
 
97
 
 
98
  return res + G + x;
 
99
}
 
100
 
 
101
/*-------------------------------------*/
 
102
struct { struct { int x; int y; } a; int b; } X10;
 
103
int Y10;
 
104
int f10 (int x) {
 
105
  //@ slice pragma expr X10;
 
106
  //@ slice pragma expr X10.a;
 
107
  //@ slice pragma expr X10.a.x;
 
108
  //@ slice pragma expr Y10;
 
109
  //@ assert X10.a.x >= 0;
 
110
  return x;
 
111
}
 
112
int main2 () {
 
113
  Y10 = 0;
 
114
  X10.b = 0;
 
115
  X10.a.y += f10 (3);
 
116
  return X10.a.x + X10.a.y;
 
117
}
 
118
/*-------------------------------------*/