← Back to branch summary

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

« back to all changes in this revision

Viewing changes to tests/scope/bts383.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/scope/bts383.c
 
1
/* run.config
 
2
   EXECNOW: make -s tests/scope/bts383.opt
 
3
   CMD: tests/scope/bts383.opt
 
4
   OPT: -val -print -journal-disable
 
5
*/
 
6
/* 
 
7
   echo '!Db.Scope.check_asserts();;' \
 
8
   | bin/toplevel.top -val tests/scope/bts383.c 
 
9
*/
 
10
 
 
11
void if1 (int * p) {
 
12
  if (*p > 0) 
 
13
    (*p)++;
 
14
}
 
15
int if2 (int c, int * p) {
 
16
  if (c)
 
17
    (*p)++;
 
18
  return *p;
 
19
}
 
20
void loop1 (int * p) {
 
21
  int i;
 
22
  int n = *p;
 
23
  for (i = 0; i < n; i++) {
 
24
    (*p)++;
 
25
  }
 
26
}
 
27
int loop2 (int n, int * p) {
 
28
  int i;
 
29
  for (i = 0; i < n; i++) {
 
30
    (*p)++;
 
31
  }
 
32
  return *p;
 
33
}
 
34
void out_char (char c);
 
35
void out_string (const char *value)
 
36
{
 
37
  for(; *value; value++)
 
38
    out_char(*value);
 
39
}
 
40
typedef struct { int a; int b; } Tstruct;
 
41
int fstruct (Tstruct * ps) {
 
42
  int x;
 
43
  ps->a = 3;
 
44
  ps->b = 5;
 
45
  x = ps->a + ps->b;
 
46
  ps++;
 
47
  ps->a = 3;
 
48
  ps->b = 5;
 
49
  x += ps->a + ps->b;
 
50
  return x;
 
51
}
 
52
int main (int * p, Tstruct * ps) {
 
53
  int x;
 
54
  x = *p;
 
55
  *p = 3;
 
56
  if1(p);
 
57
  if2(x,p);
 
58
  loop1(p);
 
59
  loop2(x,p);
 
60
  out_string(p);
 
61
  x += fstruct (ps);
 
62
  return x;
 
63
}