← Back to branch summary

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

« back to all changes in this revision

Viewing changes to tests/security/dep.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/dep.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
// #define GCC
 
8
#ifdef GCC
 
9
  #include <stdlib.h>
 
10
#else
 
11
  #define FRAMA_C_MALLOC_INDIVIDUAL
 
12
  #include "share/malloc.c"
 
13
#endif
 
14
 
 
15
/*@ requires security_status(x) == public; */
 
16
void send(int x);
 
17
 
 
18
/*@ ensures security_status( *x) == public; */
 
19
void crypt(int* x);
 
20
 
 
21
int a, b, c, d;
 
22
 
 
23
void g(int x) { send(x); }
 
24
 
 
25
void f() {
 
26
  a = 0;
 
27
  b = 0;
 
28
  crypt(&a);
 
29
  crypt(&b);
 
30
  send(a);
 
31
 
 
32
  if (c) send(a);  /* faille potentielle si dep de ctrl */
 
33
  if (!c) g(a);    /* faille potentielle si dep de ctrl */
 
34
 
 
35
  if (c)
 
36
    g(a);    /* failles potentielles si dep de ctrl */
 
37
  else
 
38
    send(b); /* failles potentielles si dep de ctrl */
 
39
 
 
40
  c = 0; crypt(&c);
 
41
  send(c);
 
42
 
 
43
  if (d) { d = 1; crypt(&d); } else { d = 2; crypt(&d); }
 
44
  send(d);   /* faille potentielle si dep de ctrl */
 
45
}