File: annot.c

package info (click to toggle)
frama-c 20140301%2Bneon%2Bdfsg-3
  • links: PTS, VCS
  • area: main
  • in suites: jessie, jessie-kfreebsd
  • size: 19,548 kB
  • ctags: 28,183
  • sloc: ml: 181,252; ansic: 13,776; makefile: 2,452; sh: 1,085; lisp: 178
file content (24 lines) | stat: -rw-r--r-- 387 bytes parent folder | download 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
 
/* run.config
   OPT: -main f1 -slice-assert f1  -then-on 'Slicing export' -print
   OPT: -main f2 -slice-assert f2  -then-on 'Slicing export' -print
*/

extern int x, z;
int t[10];

void f1() {
  int v = 3;
  x = x + x - x;
  int y = z;
  x = 3;
  int r = x;
  //@ assert x == \at(x, Pre);
}

void f2() {
  t[1] = 5;
  t[6] = 4;
  x = 2;
  x = 3;
  //@ assert \initialized(&t[x..9]);
}