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.