3
OPT: -security-analysis -security-lattice weak -security-propagate-assertions -journal-disable
7
int x = (int /*@ public */) 0;;
9
//@ assert security_status(x) == public;
10
//@ assert security_status(a) == public; // alarm
11
//@ assert security_status(a) == public;