← Back to branch summary

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

« back to all changes in this revision

Viewing changes to tests/security/simple_example.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/security/simple_example.c
 
1
/* run.config
 
2
   GCC:
 
3
   OPT: -security-analysis -lib-entry -main f -security-lattice weak -journal-disable
 
4
   OPT: -security-analysis -lib-entry -main f -security-lattice strong -journal-disable
 
5
   */
 
6
 
 
7
/*@ requires security_status(x) == public; */
 
8
void send(int x);
 
9
 
 
10
/*@ ensures security_status( *x ) == public; */
 
11
void crypt(int* x);
 
12
 
 
13
/*@ ensures security_status( *x ) == private; */
 
14
void uncrypt(int* x);
 
15
 
 
16
int c;
 
17
int /*@ public */ d;
 
18
 
 
19
int f() {
 
20
  int x = (int /*@ public */) 0;
 
21
  int y = 1;
 
22
  int z = x;
 
23
 
 
24
  send(y);   /* faille averee */
 
25
  send(z);
 
26
  crypt(&y); /* y devient public */
 
27
  send(y);
 
28
 
 
29
  if (x) uncrypt(&y); /* code mort */
 
30
  send(y);
 
31
 
 
32
  if (d) uncrypt(&y);
 
33
  send(y);   /* faille potentielle */
 
34
 
 
35
  crypt(&y); /* y devient public */
 
36
  if (c) y = z;
 
37
  send(y);   /* faille potentielle si dep de ctrl */
 
38
 
 
39
  return 0;
 
40
}
 
41
 
 
42
 
 
43
/*
 
44
Local Variables:
 
45
compile-command: "../../bin/toplevel.opt  -security-analysis -lib-entry -main f \
 
46
                  -security-lattice weak simple_example.c"
 
47
End:
 
48
*/