Examples of Compiler-Based Information Flow 
Enforcement Mechanisms

Here are some examples.

copy2

procedure copy2(				x: integer class {x};

			var	y: integer class {x});

	"copy x to y"

	var z: integer class {x});

	begin

		z := 1;						Low  z

		y := -1;						Low  y

		while z = 1 do						z  y f z

			begin

				y := y + 1;				y  y

				if y = 0				y  z

					then z := x			x  z

					else z := 0			Low  z

			end

	end

end copy2.

copy2 with goto

procedure copy2(				x: integer class {x};

			var	y: integer class {x});

	"copy x to y"

	var z: integer class {x});

	begin

1:	z := 1;							b1

	y := -1;

2:	if z  1 then goto 6;							b2

3:	y := y + 1;							b3

	if y  0 then goto 5;

4:	z := x;							b4

	goto 2;

5:	z := 0;							b5

	goto 2;

6:	end

end copy2.