← Back to branch summary

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

« back to all changes in this revision

Viewing changes to tests/security/forward.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/forward.c
 
1
/* run.config
 
2
   GCC:
 
3
   OPT: -security-analysis -security-lattice strong -lib-entry -main h -journal-disable
 
4
   */
 
5
 
 
6
/*@ requires security_status(s) == public; */
 
7
void send(const int s);
 
8
 
 
9
int a,b;
 
10
void f(void) {
 
11
  a = (int /*@ public */) 0;
 
12
  if (a) b = 0; else b = 1;
 
13
  send(a);                   // faille potentielle si dep. de ctrl. :
 
14
                             // d�duction d'info sur b
 
15
}
 
16
 
 
17
int c,d;
 
18
void g(void) {
 
19
  c = (int /*@ public */) 0;
 
20
  send(c);                   // faille potentielle si dep. de ctrl.
 
21
                             // d�duction d'info sur d
 
22
  if (c) d = 0; else d = 1;
 
23
}
 
24
 
 
25
int h(void) {
 
26
  f();
 
27
  g();
 
28
  return 0;
 
29
}