PROCEDURE UseAndChangePar* (VAR i: INTEGER): INTEGER; (** uses parameter, side-effects it, and then returns it (usage and non-killing definition of parameter) *)

BEGIN

INC(i); RETURN i

END UseAndChangePar;

PROCEDURE ChangePar* (VAR i: INTEGER): INTEGER; (** side-effects parameter, and then returns it (does not use it, killing definition of parameter) *)

BEGIN

i := 0; RETURN 0

END ChangePar;

PROCEDURE ChangeParSometimes* (VAR i: INTEGER): INTEGER; (** side-effects parameter, and then returns it (does not use it, non-killing definition of parameter) *)

VAR local: INTEGER;

BEGIN

IF local # 0 THEN

i := 0; RETURN 0

ELSE

RETURN 3

END

END ChangeParSometimes;

PROCEDURE DoNoELSE*; (** def in THEN branch, not killing previous defs *)

VAR i, j: INTEGER;

BEGIN

i := 1;

j :=2;

IF j # 0 THEN (* value of j used in expression, def of j must reach this expression *)

j := i; (* def of i must reach this assignment *)

END ;

j := j; (* both defs of j must reach this assignment *)

i := i (* def of i must reach this assignment *)

END DoNoELSE;

PROCEDURE DoWithELSE*; (** defs in both branches, killing previous defs *)

VAR i, j: INTEGER;

BEGIN

i := 1;

j :=2;

IF j # 0 THEN (* value of j used in expression, def of j must reach this expression *)

j := i; (* def of i must reach this assignment *)

ELSE

j := -i; (* def of i must reach this assignment *)

END ;

j := j; (* defs of j due to IF must reach this assignment, first def is used by expression *)

i := i (* def of i must reach this assignment *)

END DoWithELSE;

PROCEDURE DoWithELSE2*; (** defs in both branches, killing previous defs *)

VAR i, j: INTEGER;

BEGIN

i := 1;

j :=2;

IF i # 0 THEN (* value of i used in expression, def of i must reach this expression *)

j := i; (* def of i must reach this assignment *)

ELSE

j := -i; (* def of i must reach this assignment *)

END ;

j := j; (* defs of j due to IF must reach this assignment, first def must not reach *)

i := i (* def of i must reach this assignment *)

END DoWithELSE2;

PROCEDURE DoWithELSIFNoELSE*; (** def in THEN and ELSIF branch, not killing previous defs *)

VAR i, j: INTEGER;

BEGIN

i := 1;

j :=2;

IF i > 0 THEN (* value of i used in expression, def of i must reach this expression *)

j := i (* def of i must reach this assignment *)

ELSIF j < 0 THEN (* value of j used in expression, def of j must reach this expression *)

j := -i (* def of i must reach this assignment *)

END ;

j := j; (* all three defs of j must reach this assignment *)

i := i (* def of i must reach this assignment *)

END DoWithELSIFNoELSE;

PROCEDURE DoWithELSIFWithELSE*; (** defs in both branches, killing previous defs *)

VAR i, j: INTEGER;

BEGIN

i := 1;

j :=2;

IF i > 0 THEN (* value of i used in expression, def of i must reach this expression *)

j := i; (* def of i must reach this assignment *)

ELSIF i < 0 THEN (* value of i used in expression, def of i must reach this expression *)

j := -i (* def of i must reach this assignment *)

ELSE

j := 0;

END ;

j := j; (* defs of j due to IF must reach this assignment, first def must not reach *)

i := i (* def of i must reach this assignment *)

END DoWithELSIFWithELSE;

PROCEDURE DoSideEffects00*; (** side-effect in expression of IF (killing def), def and usage in THEN branch, no ELSE *)

VAR i, j: INTEGER;

BEGIN

i := 0;

j := 2;

IF ChangePar(i) < 0 THEN (* first def of i is killed by function call *)

INC(j)

END ;

i := i; (* first def of i is not reaching *)

j := j

END DoSideEffects00;

PROCEDURE DoSideEffects01*; (** side-effect in expression of IF (killing def), def in THEN branch, no ELSE *)

VAR i: INTEGER;

BEGIN

i := 0;

IF ChangePar(i) < 0 THEN (* first def of i is killed by function call *)

i := 2 (* kills def due to function call *)

END ;

i := i (* first def of i is not reaching, def due to function call (via non-existing ELSE) and def within IF are reaching *)

END DoSideEffects01;

PROCEDURE DoSideEffects02*; (** side-effect in expression of IF (killing def), defs in both branches *)

VAR i: INTEGER;

BEGIN

i := 0;

IF ChangePar(i) < 0 THEN (* first def of i is killed by function call *)

i := 2 (* kills def due to function call *)

ELSE

i := 1

END ;

i := i (* first def of i is not reaching, defs in THEN and in ELSE branch are reaching, def due to function call is not reaching*)

END DoSideEffects02;

PROCEDURE DoSideEffects10*; (** side-effect in expression with short circuit evaluation (&) of IF (killing def), defs in both branches *)

VAR i, j: INTEGER;

BEGIN

i := 0;

j := 2;

IF (ChangePar(i) < 0) & (ChangePar(j) < 0) THEN

(* i defined and j defined by function calls *)

i := i; (* first def of i is not reaching, only def of i due to function call is reaching *)

j := j (* first def of j is not reaching, only def of j due to function call is reaching *)

ELSE

(* i defined OR

i defined and j defined by function calls

*)

i := i; (* first def of i is not reaching, only def of i due to function call is reaching *)

j := j (* first def of j may be reaching (if left expression of & failed) *)

END ;

i := i; (* first def of i is not reaching, only defs of i within IF are reaching *)

j := j (* first def of j may be reaching, as well as defs of j within IF *)

END DoSideEffects10;

PROCEDURE DoSideEffects11*; (** side-effect in expression with short circuit evaluation (~, &) of IF (killing def), defs in both branches *)

VAR i, j: INTEGER;

BEGIN

i := 0;

j := 2;

IF ~((ChangePar(i) < 0) & (ChangePar(j) < 0)) THEN

(* i defined OR

i defined and j defined by function calls

*)

i := i; (* first def of i is not reaching, only def of i due to function call is reaching *)

j := j (* first def of j may be reaching (if left expression of & failed) *)

ELSE

(* i defined and j defined by function calls *)

i := i; (* first def of i is not reaching, only def of i due to function call is reaching *)

j := j (* first def of j is not reaching, only def of j due to function call is reaching *)

END ;

i := i; (* first def of i is not reaching, only defs of i within IF are reaching *)

j := j (* first def of j may be reaching, as well as defs of j within IF *)

END DoSideEffects11;

PROCEDURE DoSideEffects20*; (** side-effect in expression with short circuit evaluation (&) of IF (killing def), defs in both branches *)

VAR i, j, k: INTEGER;

BEGIN

i := 0;

j := 1;

k := 2;

IF (ChangePar(i) < 0) & ((ChangePar(j) < 0) & (ChangePar(k) < 0)) THEN

(* i defined, j defined, and k defined by function calls *)

i := i; (* first def of i is not reaching, only def of i due to function call is reaching *)

j := j; (* first def of j is not reaching, only def of j due to function call is reaching *)

k := k (* first def of k is not reaching, only def of k due to function call is reaching *)

ELSE

(* i defined OR

i defined and j defined OR

i defined, j defined and k defined by function calls

*)

i := i; (* first def of i is not reaching, only def of i due to function call is reaching *)

j := j; (* first def of j may be reaching (if left expression of & failed) *)

k := k (* first def of j may be reaching (if left expression of & failed) *)

END ;

i := i; (* only defs of i within IF must be reaching *)

j := j; (* all defs of j can be reaching *)

k := k (* all defs of j can be reaching *)

END DoSideEffects20;

PROCEDURE DoSideEffects30*; (** side-effect in expression with short circuit evaluation (OR) of IF (killing def), defs in both branches *)

VAR i, j, k: INTEGER;

BEGIN

i := 0;

j := 1;

k := 2;

IF (ChangePar(i) < 0) OR ((ChangePar(j) < 0) OR (ChangePar(k) < 0)) THEN

(* i defined OR

i defined and j defined OR

i defined, j defined and k defined by function calls

*)

i := i; (* first def of i is not reaching, only def of i due to function call is reaching *)

j := j; (* first def of j is may be reaching (if left expression of & failed) *)

k := k (* first def of k j may be reaching (if left expression of & failed) *)

ELSE (* i defined, j defined, and k defined by function calls *)

i := i; (* first def of i is not reaching, only def of i due to function call is reaching *)

j := j; (* first def of j is not reaching, only def of j due to function call is reaching *)

k := k (* first def of k is not reaching, only def of k due to function call is reaching *)

END ;

i := i; (* only defs of i within IF must be reaching *)

j := j; (* all defs of j can be reaching *)

k := k (* all defs of j can be reaching *)

END DoSideEffects30;

PROCEDURE DoSideEffects2*; (** side-effects in expressions of IF and ELSIF *)

VAR i, j: INTEGER;

BEGIN

i := 0;

j := 1;

IF ChangePar(i) < 0 THEN (* first def of i is killed by function call *)

j := 1

ELSIF ChangePar(i) > 0 THEN (* previous defs of i are killed by function call *)

j := 2;

i := 3

ELSE

j := 3

END ;

i := i; (* first def of i is not reaching, def of i due to function calls are reaching *)

j := j (* first def of j is not reaching, since all branches of IF define j *)

END DoSideEffects2;

PROCEDURE DoSideEffects3*; (** side-effect in expression of IF (non-killing def), def in THEN branch, no ELSE *)

VAR i: INTEGER;

BEGIN

i := 0;

IF ChangeParSometimes(i) < 0 THEN (* first def of i is not killed by function call *)

i := 2 (* kills def due to function call *)

END ;

i := i (* first def of i is reaching, def due to function call (via non-existing ELSE) and def within IF are reaching *)

END DoSideEffects3;

END TestIF.