Merge branch 'develop' into arrays-proof

8 files changed, 1160 insertions, 56 deletions

diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index e719070..204451c 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -21,7 +21,7 @@ From compcert Require Import Globalenvs.
 From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap.
 From coqup Require HTL Verilog.
 
-Import AssocMapNotation.
+Local Open Scope assocmap.
 
 Hint Resolve Smallstep.forward_simulation_plus : htlproof.
 Hint Resolve AssocMap.gss : htlproof.
@@ -37,25 +37,40 @@ Inductive match_assocmaps : RTL.function -> RTL.regset -> assocmap -> Prop :=
 Hint Constructors match_assocmaps : htlproof.
 
 Definition state_st_wf (m : HTL.module) (s : HTL.state) :=
-  forall st assoc,
-  s = HTL.State m st assoc ->
+  forall st assoc res,
+  s = HTL.State res m st assoc ->
   assoc!(m.(HTL.mod_st)) = Some (posToValue 32 st).
 Hint Unfold state_st_wf : htlproof.
 
+Inductive match_stacks : list RTL.stackframe -> list HTL.stackframe -> Prop :=
+| match_stacks_nil :
+    match_stacks nil nil
+| match_stacks_cons :
+    forall cs lr r f sp pc rs m assoc
+           (TF : tr_module f m)
+           (ST: match_stacks cs lr)
+           (MA: match_assocmaps f rs assoc),
+      match_stacks (RTL.Stackframe r f sp pc rs :: cs)
+                   (HTL.Stackframe r m pc assoc :: lr).
+
 Inductive match_states : RTL.state -> HTL.state -> Prop :=
-| match_state : forall (rs : RTL.regset) assoc sf f sp rs mem m st
+| match_state : forall assoc sf f sp rs mem m st res
     (MASSOC : match_assocmaps f rs assoc)
     (TF : tr_module f m)
-    (WF : state_st_wf m (HTL.State m st assoc)),
+    (WF : state_st_wf m (HTL.State res m st assoc))
+    (MS : match_stacks sf res),
     match_states (RTL.State sf f sp st rs mem)
-                 (HTL.State m st assoc)
-| match_returnstate : forall v v' stack m,
-    val_value_lessdef v v' ->
-    match_states (RTL.Returnstate stack v m) (HTL.Returnstate v')
+                 (HTL.State res m st assoc)
+| match_returnstate :
+    forall
+      v v' stack m res
+      (MS : match_stacks stack res),
+      val_value_lessdef v v' ->
+      match_states (RTL.Returnstate stack v m) (HTL.Returnstate res v')
 | match_initial_call :
-    forall f m m0 st
+    forall f m m0
     (TF : tr_module f m),
-      match_states (RTL.Callstate nil (AST.Internal f) nil m0) (HTL.State m st empty_assocmap).
+      match_states (RTL.Callstate nil (AST.Internal f) nil m0) (HTL.Callstate nil m nil).
 Hint Constructors match_states : htlproof.
 
 Definition match_prog (p: RTL.program) (tp: HTL.program) :=
@@ -156,6 +171,20 @@ Ltac unfold_func H :=
   | ?f _ _ _ _ = _ => unfold f in H; repeat (unfold_match H)
   end.
 
+Lemma init_reg_assoc_empty :
+  forall f l,
+    match_assocmaps f (RTL.init_regs nil l) (HTL.init_regs nil l).
+Proof.
+  induction l; simpl; constructor; intros.
+  - rewrite Registers.Regmap.gi. unfold find_assocmap.
+    unfold AssocMapExt.get_default. rewrite AssocMap.gempty.
+    constructor.
+
+  - rewrite Registers.Regmap.gi. unfold find_assocmap.
+    unfold AssocMapExt.get_default. rewrite AssocMap.gempty.
+    constructor.
+Qed.
+
 Section CORRECTNESS.
 
   Variable prog : RTL.program.
@@ -234,10 +263,10 @@ Section CORRECTNESS.
    *)
 
   Definition transl_instr_prop (instr : RTL.instruction) : Prop :=
-    forall m assoc fin rtrn st stmt trans,
+    forall m assoc fin rtrn st stmt trans res,
       tr_instr fin rtrn st instr stmt trans ->
       exists assoc',
-        HTL.step tge (HTL.State m st assoc) Events.E0 (HTL.State m st assoc').
+        HTL.step tge (HTL.State res m st assoc) Events.E0 (HTL.State res m st assoc').
 
   Theorem transl_step_correct:
     forall (S1 : RTL.state) t S2,
@@ -329,7 +358,7 @@ Section CORRECTNESS.
       (* match_states *)
       assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit.
       rewrite <- H1.
-      constructor. apply rs0.
+      constructor.
       unfold_merge.
       apply regs_lessdef_add_match.
       constructor.
@@ -343,6 +372,7 @@ Section CORRECTNESS.
       rewrite AssocMap.gso.
       apply AssocMap.gss.
       apply st_greater_than_res.
+      assumption.
 
       - econstructor. split. apply Smallstep.plus_one.
       eapply HTL.step_module; eauto.
@@ -367,7 +397,7 @@ Section CORRECTNESS.
 
       destruct b.
       rewrite assumption_32bit.
-      apply match_state. apply rs0.
+      apply match_state.
       unfold_merge.
       apply regs_lessdef_add_greater. apply greater_than_max_func.
       assumption. assumption.
@@ -375,8 +405,9 @@ Section CORRECTNESS.
       unfold state_st_wf. intros. inversion H1.
       subst. unfold_merge.
       apply AssocMap.gss.
+      assumption.
       rewrite assumption_32bit.
-      apply match_state. apply rs0.
+      apply match_state.
       unfold_merge.
       apply regs_lessdef_add_greater. apply greater_than_max_func. assumption.
       assumption.
@@ -384,6 +415,7 @@ Section CORRECTNESS.
       unfold state_st_wf. intros. inversion H1.
       subst. unfold_merge.
       apply AssocMap.gss.
+      assumption.
 
     - (* Return *)
       econstructor. split.
@@ -400,7 +432,7 @@ Section CORRECTNESS.
       trivial.
       rewrite AssocMap.gso.
       rewrite AssocMap.gso.
-      unfold state_st_wf in WF. apply WF. trivial.
+      unfold state_st_wf in WF. eapply WF. trivial.
       apply st_greater_than_res. apply st_greater_than_res. trivial.
 
       apply HTL.step_finish.
@@ -410,10 +442,10 @@ Section CORRECTNESS.
       apply finish_not_return.
       apply AssocMap.gss.
       rewrite Events.E0_left. trivial.
-
-      constructor. constructor.
-    - destruct (assoc!r) eqn:?.
-      inversion H11. subst.
+      constructor.
+      assumption.
+      constructor.
+    - inversion H11. subst.
       econstructor. split.
       eapply Smallstep.plus_two.
       eapply HTL.step_module; eauto.
@@ -422,14 +454,11 @@ Section CORRECTNESS.
       econstructor; simpl; trivial.
       constructor.
       econstructor; simpl; trivial.
-      apply Verilog.erun_Vvar.
-      rewrite AssocMap.gso.
-      apply Heqo. apply not_eq_sym. apply finish_not_res.
+      apply Verilog.erun_Vvar. trivial.
       unfold_merge.
-      trivial.
       rewrite AssocMap.gso.
       rewrite AssocMap.gso.
-      unfold state_st_wf in WF. apply WF. trivial.
+      unfold state_st_wf in WF. eapply WF. trivial.
       apply st_greater_than_res. apply st_greater_than_res. trivial.
 
       apply HTL.step_finish.
@@ -440,8 +469,38 @@ Section CORRECTNESS.
       apply AssocMap.gss.
       rewrite Events.E0_left. trivial.
 
-      constructor. simpl.
-      Admitted.
+      constructor. assumption. simpl. inversion MASSOC. subst.
+      unfold find_assocmap, AssocMapExt.get_default. rewrite AssocMap.gso.
+      apply H1. eapply RTL.max_reg_function_use. eauto. simpl; tauto.
+      apply st_greater_than_res.
+
+    - inversion MSTATE; subst. inversion TF; subst.
+      econstructor. split. apply Smallstep.plus_one.
+      eapply HTL.step_call.
+
+      constructor. apply regs_lessdef_add_greater.
+      apply greater_than_max_func.
+      apply init_reg_assoc_empty. assumption. unfold state_st_wf.
+      intros. inv H1. apply AssocMap.gss. constructor.
+    - inversion MSTATE; subst. inversion MS; subst. econstructor.
+      split. apply Smallstep.plus_one.
+      constructor.
+
+      constructor; auto. constructor; auto. apply regs_lessdef_add_match; auto.
+      apply regs_lessdef_add_greater. apply greater_than_max_func. auto.
+
+      unfold state_st_wf. intros. inv H. rewrite AssocMap.gso.
+      rewrite AssocMap.gss. trivial. apply st_greater_than_res.
+
+      Unshelve.
+      exact (AssocMap.empty value).
+      exact (AssocMap.empty value).
+      exact (ZToValue 32 0).
+      exact (AssocMap.empty value).
+      exact (AssocMap.empty value).
+      exact (AssocMap.empty value).
+      exact (AssocMap.empty value).
+  Qed.
   Hint Resolve transl_step_correct : htlproof.
 
   Lemma transl_initial_states :
@@ -467,12 +526,14 @@ Section CORRECTNESS.
   Hint Resolve transl_initial_states : htlproof.
 
   Lemma transl_final_states :
-    forall (s1 : Smallstep.state (RTL.semantics prog)) (s2 : Smallstep.state (HTL.semantics tprog))
+    forall (s1 : Smallstep.state (RTL.semantics prog))
+           (s2 : Smallstep.state (HTL.semantics tprog))
            (r : Integers.Int.int),
       match_states s1 s2 ->
-      Smallstep.final_state (RTL.semantics prog) s1 r -> Smallstep.final_state (HTL.semantics tprog) s2 r.
+      Smallstep.final_state (RTL.semantics prog) s1 r ->
+      Smallstep.final_state (HTL.semantics tprog) s2 r.
   Proof.
-    intros. inv H0. inv H. inv H4. constructor. trivial.
+    intros. inv H0. inv H. inv H4. inv MS. constructor. trivial.
   Qed.
   Hint Resolve transl_final_states : htlproof.
 
diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v
index 88b13a6..5d531d5 100644
--- a/src/verilog/AssocMap.v
+++ b/src/verilog/AssocMap.v
@@ -202,9 +202,16 @@ Ltac unfold_merge :=
   unfold merge_assocmap; try (repeat (rewrite merge_add_assoc));
   rewrite AssocMapExt.merge_base_1.
 
-Module AssocMapNotation.
-  Notation "a ! b" := (AssocMap.get b a) (at level 1).
-  Notation "a # ( b , c )" := (find_assocmap c b a) (at level 1).
-  Notation "a # b" := (find_assocmap 32 b a) (at level 1).
-  Notation "a ## b" := (List.map (fun c => find_assocmap 32 c a) b) (at level 1).
-End AssocMapNotation.
+Declare Scope assocmap.
+Notation "a ! b" := (AssocMap.get b a) (at level 1) : assocmap.
+Notation "a # ( b , c )" := (find_assocmap c b a) (at level 1) : assocmap.
+Notation "a # b" := (find_assocmap 32 b a) (at level 1) : assocmap.
+Notation "a ## b" := (List.map (fun c => find_assocmap 32 c a) b) (at level 1) : assocmap.
+Notation "a # b '<-' c" := (AssocMap.set b c a) (at level 1, b at next level) : assocmap.
+
+Local Open Scope assocmap.
+Lemma find_get_assocmap :
+  forall assoc r v,
+  assoc ! r = Some v ->
+  assoc # r = v.
+Proof. intros. unfold find_assocmap, AssocMapExt.get_default. rewrite H. trivial. Qed.
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index cb081b2..2e4ef1a 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -30,6 +30,8 @@ hardware-like layout that is still similar to the register transfer language
 instantiations and that we now describe a state machine instead of a
 control-flow graph. *)
 
+Local Open Scope assocmap.
+
 Definition reg := positive.
 Definition node := positive.
 
@@ -52,22 +54,42 @@ Definition fundef := AST.fundef module.
 
 Definition program := AST.program fundef unit.
 
+Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} :=
+  match rl, vl with
+  | r :: rl', v :: vl' => AssocMap.set r v (init_regs vl' rl')
+  | _, _ => empty_assocmap
+  end.
+
 (** * Operational Semantics *)
 
 Definition genv := Globalenvs.Genv.t fundef unit.
 
+Inductive stackframe : Type :=
+  Stackframe :
+    forall  (res : reg)
+            (m : module)
+            (pc : node)
+            (assoc : assocmap),
+      stackframe.
+
 Inductive state : Type :=
 | State :
-    forall (m : module)
+    forall (stack : list stackframe)
+           (m : module)
            (st : node)
            (reg_assoc : assocmap)
-           (arr_assoc : AssocMap.t (list value)),
-  state
-| Returnstate : forall v : value, state.
+           (arr_assoc : AssocMap.t (list value)), state
+| Returnstate :
+    forall (res : list stackframe)
+           (v : value), state
+| Callstate :
+    forall (stack : list stackframe)
+           (m : module)
+           (args : list value), state.
 
 Inductive step : genv -> state -> Events.trace -> state -> Prop :=
 | step_module :
-    forall g t m st ctrl data
+    forall g m st sf ctrl data
       asr asa
       basr1 basa1 nasr1 nasa1
       basr2 basa2 nasr2 nasa2
@@ -91,27 +113,40 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
       asa' = AssocMapExt.merge (list value) nasa2 basa2 ->
       asr'!(m.(mod_st)) = Some stval ->
       valueToPos stval = pstval ->
-      step g (State m st asr asa) t (State m pstval asr' asa')
+      step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa')
 | step_finish :
-    forall g t m st asr asa retval,
+    forall g m st asr asa retval sf,
     asr!(m.(mod_finish)) = Some (1'h"1") ->
     asr!(m.(mod_return)) = Some retval ->
-    step g (State m st asr asa) t (Returnstate retval).
+    step g (State sf m st asr asa) Events.E0 (Returnstate sf retval)
+| step_call :
+    forall g m args res,
+      step g (Callstate res m args) Events.E0
+           (State res m m.(mod_entrypoint)
+             (AssocMap.set (mod_st m) (posToValue 32 m.(mod_entrypoint))
+                           (init_regs args m.(mod_params)))
+              (AssocMap.empty (list value)))
+| step_return :
+    forall g m asr i r sf pc mst,
+      mst = mod_st m ->
+      step g (Returnstate (Stackframe r m pc asr :: sf) i) Events.E0
+           (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i)
+                  (AssocMap.empty (list value))).
 Hint Constructors step : htl.
 
 Inductive initial_state (p: program): state -> Prop :=
-  | initial_state_intro: forall b m0 st m,
+  | initial_state_intro: forall b m0 m,
       let ge := Globalenvs.Genv.globalenv p in
       Globalenvs.Genv.init_mem p = Some m0 ->
       Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b ->
       Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal m) ->
-      st = m.(mod_entrypoint) ->
-      initial_state p (State m st empty_assocmap (AssocMap.empty (list value))).
+      initial_state p (Callstate nil m nil).
 
 Inductive final_state : state -> Integers.int -> Prop :=
 | final_state_intro : forall retval retvali,
     retvali = valueToInt retval ->
-    final_state (Returnstate retval) retvali.
+    final_state (Returnstate nil retval) retvali.
 
 Definition semantics (m : program) :=
-  Smallstep.Semantics step (initial_state m) final_state (Globalenvs.Genv.globalenv m).
+  Smallstep.Semantics step (initial_state m) final_state
+                      (Globalenvs.Genv.globalenv m).
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 74c08fe..845d706 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -32,7 +32,8 @@ From compcert Require Integers Events.
 From compcert Require Import Errors Smallstep Globalenvs.
 
 Import HexNotationValue.
-Import AssocMapNotation.
+
+Local Open Scope assocmap.
 
 Set Implicit Arguments.
 
@@ -291,17 +292,13 @@ Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop
       expr_runp fext reg stack (Vlit v) v
   | erun_Vvar :
       forall fext reg stack v r,
-      reg!r = Some v ->
+      reg#r = v ->
       expr_runp fext reg stack (Vvar r) v
   | erun_Vvari :
       forall fext reg stack v iexp i r,
       expr_runp fext reg stack iexp i ->
       arr_assocmap_lookup stack r (valueToNat i) = Some v ->
       expr_runp fext reg stack (Vvari r iexp) v
-  | erun_Vvar_empty :
-      forall fext reg stack r sz,
-      reg!r = None ->
-      expr_runp fext reg stack (Vvar r) (ZToValue sz 0)
   | erun_Vinputvar :
       forall fext reg stack r v,
       fext!r = Some v ->
diff --git a/test/dhrystone/Makefile b/test/dhrystone/Makefile
new file mode 100644
index 0000000..6a10d2a
--- /dev/null
+++ b/test/dhrystone/Makefile
@@ -0,0 +1,8 @@
+CC := gcc
+CFLAGS := -O3
+
+all:
+	$(CC) $(CFLAGS) -DHZ=60 dhry_1.c dhry_2.c -o dhry
+
+clean:
+	rm -f dhry
diff --git a/test/dhrystone/dhry.h b/test/dhrystone/dhry.h
new file mode 100644
index 0000000..0c46375
--- /dev/null
+++ b/test/dhrystone/dhry.h
@@ -0,0 +1,422 @@
+/*
+ ****************************************************************************
+ *
+ *                   "DHRYSTONE" Benchmark Program
+ *                   -----------------------------
+ *
+ *  Version:    C, Version 2.1
+ *
+ *  File:       dhry.h (part 1 of 3)
+ *
+ *  Date:       May 25, 1988
+ *
+ *  Author:     Reinhold P. Weicker
+ *                      Siemens AG, AUT E 51
+ *                      Postfach 3220
+ *                      8520 Erlangen
+ *                      Germany (West)
+ *                              Phone:  [+49]-9131-7-20330
+ *                                      (8-17 Central European Time)
+ *                              Usenet: ..!mcsun!unido!estevax!weicker
+ *
+ *              Original Version (in Ada) published in
+ *              "Communications of the ACM" vol. 27., no. 10 (Oct. 1984),
+ *              pp. 1013 - 1030, together with the statistics
+ *              on which the distribution of statements etc. is based.
+ *
+ *              In this C version, the following C library functions are used:
+ *              - strcpy, strcmp (inside the measurement loop)
+ *              - printf, scanf (outside the measurement loop)
+ *              In addition, Berkeley UNIX system calls "times ()" or "time ()"
+ *              are used for execution time measurement. For measurements
+ *              on other systems, these calls have to be changed.
+ *
+ *  Collection of Results:
+ *              Reinhold Weicker (address see above) and
+ *
+ *              Rick Richardson
+ *              PC Research. Inc.
+ *              94 Apple Orchard Drive
+ *              Tinton Falls, NJ 07724
+ *                      Phone:  (201) 389-8963 (9-17 EST)
+ *                      Usenet: ...!uunet!pcrat!rick
+ *
+ *      Please send results to Rick Richardson and/or Reinhold Weicker.
+ *      Complete information should be given on hardware and software used.
+ *      Hardware information includes: Machine type, CPU, type and size
+ *      of caches; for microprocessors: clock frequency, memory speed
+ *      (number of wait states).
+ *      Software information includes: Compiler (and runtime library)
+ *      manufacturer and version, compilation switches, OS version.
+ *      The Operating System version may give an indication about the
+ *      compiler; Dhrystone itself performs no OS calls in the measurement loop.
+ *
+ *      The complete output generated by the program should be mailed
+ *      such that at least some checks for correctness can be made.
+ *
+ ***************************************************************************
+ *
+ *  History:    This version C/2.1 has been made for two reasons:
+ *
+ *              1) There is an obvious need for a common C version of
+ *              Dhrystone, since C is at present the most popular system
+ *              programming language for the class of processors
+ *              (microcomputers, minicomputers) where Dhrystone is used most.
+ *              There should be, as far as possible, only one C version of
+ *              Dhrystone such that results can be compared without
+ *              restrictions. In the past, the C versions distributed
+ *              by Rick Richardson (Version 1.1) and by Reinhold Weicker
+ *              had small (though not significant) differences.
+ *
+ *              2) As far as it is possible without changes to the Dhrystone
+ *              statistics, optimizing compilers should be prevented from
+ *              removing significant statements.
+ *
+ *              This C version has been developed in cooperation with
+ *              Rick Richardson (Tinton Falls, NJ), it incorporates many
+ *              ideas from the "Version 1.1" distributed previously by
+ *              him over the UNIX network Usenet.
+ *              I also thank Chaim Benedelac (National Semiconductor),
+ *              David Ditzel (SUN), Earl Killian and John Mashey (MIPS),
+ *              Alan Smith and Rafael Saavedra-Barrera (UC at Berkeley)
+ *              for their help with comments on earlier versions of the
+ *              benchmark.
+ *
+ *  Changes:    In the initialization part, this version follows mostly
+ *              Rick Richardson's version distributed via Usenet, not the
+ *              version distributed earlier via floppy disk by Reinhold Weicker.
+ *              As a concession to older compilers, names have been made
+ *              unique within the first 8 characters.
+ *              Inside the measurement loop, this version follows the
+ *              version previously distributed by Reinhold Weicker.
+ *
+ *              At several places in the benchmark, code has been added,
+ *              but within the measurement loop only in branches that
+ *              are not executed. The intention is that optimizing compilers
+ *              should be prevented from moving code out of the measurement
+ *              loop, or from removing code altogether. Since the statements
+ *              that are executed within the measurement loop have NOT been
+ *              changed, the numbers defining the "Dhrystone distribution"
+ *              (distribution of statements, operand types and locality)
+ *              still hold. Except for sophisticated optimizing compilers,
+ *              execution times for this version should be the same as
+ *              for previous versions.
+ *
+ *              Since it has proven difficult to subtract the time for the
+ *              measurement loop overhead in a correct way, the loop check
+ *              has been made a part of the benchmark. This does have
+ *              an impact - though a very minor one - on the distribution
+ *              statistics which have been updated for this version.
+ *
+ *              All changes within the measurement loop are described
+ *              and discussed in the companion paper "Rationale for
+ *              Dhrystone version 2".
+ *
+ *              Because of the self-imposed limitation that the order and
+ *              distribution of the executed statements should not be
+ *              changed, there are still cases where optimizing compilers
+ *              may not generate code for some statements. To a certain
+ *              degree, this is unavoidable for small synthetic benchmarks.
+ *              Users of the benchmark are advised to check code listings
+ *              whether code is generated for all statements of Dhrystone.
+ *
+ *              Version 2.1 is identical to version 2.0 distributed via
+ *              the UNIX network Usenet in March 1988 except that it corrects
+ *              some minor deficiencies that were found by users of version 2.0.
+ *              The only change within the measurement loop is that a
+ *              non-executed "else" part was added to the "if" statement in
+ *              Func_3, and a non-executed "else" part removed from Proc_3.
+ *
+ ***************************************************************************
+ *
+ * Defines:     The following "Defines" are possible:
+ *              -DREG=register          (default: Not defined)
+ *                      As an approximation to what an average C programmer
+ *                      might do, the "register" storage class is applied
+ *                      (if enabled by -DREG=register)
+ *                      - for local variables, if they are used (dynamically)
+ *                        five or more times
+ *                      - for parameters if they are used (dynamically)
+ *                        six or more times
+ *                      Note that an optimal "register" strategy is
+ *                      compiler-dependent, and that "register" declarations
+ *                      do not necessarily lead to faster execution.
+ *              -DNOSTRUCTASSIGN        (default: Not defined)
+ *                      Define if the C compiler does not support
+ *                      assignment of structures.
+ *              -DNOENUMS               (default: Not defined)
+ *                      Define if the C compiler does not support
+ *                      enumeration types.
+ *              -DTIMES                 (default)
+ *              -DTIME
+ *                      The "times" function of UNIX (returning process times)
+ *                      or the "time" function (returning wallclock time)
+ *                      is used for measurement.
+ *                      For single user machines, "time ()" is adequate. For
+ *                      multi-user machines where you cannot get single-user
+ *                      access, use the "times ()" function. If you have
+ *                      neither, use a stopwatch in the dead of night.
+ *                      "printf"s are provided marking the points "Start Timer"
+ *                      and "Stop Timer". DO NOT use the UNIX "time(1)"
+ *                      command, as this will measure the total time to
+ *                      run this program, which will (erroneously) include
+ *                      the time to allocate storage (malloc) and to perform
+ *                      the initialization.
+ *              -DHZ=nnn
+ *                      In Berkeley UNIX, the function "times" returns process
+ *                      time in 1/HZ seconds, with HZ = 60 for most systems.
+ *                      CHECK YOUR SYSTEM DESCRIPTION BEFORE YOU JUST APPLY
+ *                      A VALUE.
+ *
+ ***************************************************************************
+ *
+ *  Compilation model and measurement (IMPORTANT):
+ *
+ *  This C version of Dhrystone consists of three files:
+ *  - dhry.h (this file, containing global definitions and comments)
+ *  - dhry_1.c (containing the code corresponding to Ada package Pack_1)
+ *  - dhry_2.c (containing the code corresponding to Ada package Pack_2)
+ *
+ *  The following "ground rules" apply for measurements:
+ *  - Separate compilation
+ *  - No procedure merging
+ *  - Otherwise, compiler optimizations are allowed but should be indicated
+ *  - Default results are those without register declarations
+ *  See the companion paper "Rationale for Dhrystone Version 2" for a more
+ *  detailed discussion of these ground rules.
+ *
+ *  For 16-Bit processors (e.g. 80186, 80286), times for all compilation
+ *  models ("small", "medium", "large" etc.) should be given if possible,
+ *  together with a definition of these models for the compiler system used.
+ *
+ **************************************************************************
+ *
+ *  Dhrystone (C version) statistics:
+ *
+ *  [Comment from the first distribution, updated for version 2.
+ *   Note that because of language differences, the numbers are slightly
+ *   different from the Ada version.]
+ *
+ *  The following program contains statements of a high level programming
+ *  language (here: C) in a distribution considered representative:
+ *
+ *    assignments                  52 (51.0 %)
+ *    control statements           33 (32.4 %)
+ *    procedure, function calls    17 (16.7 %)
+ *
+ *  103 statements are dynamically executed. The program is balanced with
+ *  respect to the three aspects:
+ *
+ *    - statement type
+ *    - operand type
+ *    - operand locality
+ *         operand global, local, parameter, or constant.
+ *
+ *  The combination of these three aspects is balanced only approximately.
+ *
+ *  1. Statement Type:
+ *  -----------------             number
+ *
+ *     V1 = V2                     9
+ *       (incl. V1 = F(..)
+ *     V = Constant               12
+ *     Assignment,                 7
+ *       with array element
+ *     Assignment,                 6
+ *       with record component
+ *                                --
+ *                                34       34
+ *
+ *     X = Y +|-|"&&"|"|" Z        5
+ *     X = Y +|-|"==" Constant     6
+ *     X = X +|- 1                 3
+ *     X = Y *|/ Z                 2
+ *     X = Expression,             1
+ *           two operators
+ *     X = Expression,             1
+ *           three operators
+ *                                --
+ *                                18       18
+ *
+ *     if ....                    14
+ *       with "else"      7
+ *       without "else"   7
+ *           executed        3
+ *           not executed    4
+ *     for ...                     7  |  counted every time
+ *     while ...                   4  |  the loop condition
+ *     do ... while                1  |  is evaluated
+ *     switch ...                  1
+ *     break                       1
+ *     declaration with            1
+ *       initialization
+ *                                --
+ *                                34       34
+ *
+ *     P (...)  procedure call    11
+ *       user procedure      10
+ *       library procedure    1
+ *     X = F (...)
+ *             function  call      6
+ *       user function        5
+ *       library function     1
+ *                                --
+ *                                17       17
+ *                                        ---
+ *                                        103
+ *
+ *    The average number of parameters in procedure or function calls
+ *    is 1.82 (not counting the function values as implicit parameters).
+ *
+ *
+ *  2. Operators
+ *  ------------
+ *                          number    approximate
+ *                                    percentage
+ *
+ *    Arithmetic             32          50.8
+ *
+ *       +                     21          33.3
+ *       -                      7          11.1
+ *       *                      3           4.8
+ *       / (int div)            1           1.6
+ *
+ *    Comparison             27           42.8
+ *
+ *       ==                     9           14.3
+ *       /=                     4            6.3
+ *       >                      1            1.6
+ *       <                      3            4.8
+ *       >=                     1            1.6
+ *       <=                     9           14.3
+ *
+ *    Logic                   4            6.3
+ *
+ *       && (AND-THEN)          1            1.6
+ *       |  (OR)                1            1.6
+ *       !  (NOT)               2            3.2
+ *
+ *                           --          -----
+ *                           63          100.1
+ *
+ *
+ *  3. Operand Type (counted once per operand reference):
+ *  ---------------
+ *                          number    approximate
+ *                                    percentage
+ *
+ *     Integer               175        72.3 %
+ *     Character              45        18.6 %
+ *     Pointer                12         5.0 %
+ *     String30                6         2.5 %
+ *     Array                   2         0.8 %
+ *     Record                  2         0.8 %
+ *                           ---       -------
+ *                           242       100.0 %
+ *
+ *  When there is an access path leading to the final operand (e.g. a record
+ *  component), only the final data type on the access path is counted.
+ *
+ *
+ *  4. Operand Locality:
+ *  -------------------
+ *                                number    approximate
+ *                                          percentage
+ *
+ *     local variable              114        47.1 %
+ *     global variable              22         9.1 %
+ *     parameter                    45        18.6 %
+ *        value                        23         9.5 %
+ *        reference                    22         9.1 %
+ *     function result               6         2.5 %
+ *     constant                     55        22.7 %
+ *                                 ---       -------
+ *                                 242       100.0 %
+ *
+ *
+ *  The program does not compute anything meaningful, but it is syntactically
+ *  and semantically correct. All variables have a value assigned to them
+ *  before they are used as a source operand.
+ *
+ *  There has been no explicit effort to account for the effects of a
+ *  cache, or to balance the use of long or short displacements for code or
+ *  data.
+ *
+ ***************************************************************************
+ */
+
+/* Compiler and system dependent definitions: */
+
+#ifndef TIME
+#define TIMES
+#endif
+                /* Use times(2) time function unless    */
+                /* explicitly defined otherwise         */
+
+#ifdef TIMES
+#include <sys/types.h>
+#include <sys/times.h>
+                /* for "times" */
+#endif
+
+#define Mic_secs_Per_Second     1000000.0
+                /* Berkeley UNIX C returns process times in seconds/HZ */
+
+#ifdef  NOSTRUCTASSIGN
+#define structassign(d, s)      memcpy(&(d), &(s), sizeof(d))
+#else
+#define structassign(d, s)      d = s
+#endif
+
+#ifdef  NOENUM
+#define Ident_1 0
+#define Ident_2 1
+#define Ident_3 2
+#define Ident_4 3
+#define Ident_5 4
+  typedef int   Enumeration;
+#else
+  typedef       enum    {Ident_1, Ident_2, Ident_3, Ident_4, Ident_5}
+                Enumeration;
+#endif
+        /* for boolean and enumeration types in Ada, Pascal */
+
+/* General definitions: */
+
+#include <stdio.h>
+#include <string.h>
+                /* for strcpy, strcmp */
+
+#define Null 0
+                /* Value of a Null pointer */
+#define true  1
+#define false 0
+
+typedef int     One_Thirty;
+typedef int     One_Fifty;
+typedef char    Capital_Letter;
+typedef int     Boolean;
+typedef char    Str_30 [31];
+typedef int     Arr_1_Dim [50];
+typedef int     Arr_2_Dim [50] [50];
+
+typedef struct record
+    {
+    struct record *Ptr_Comp;
+    Enumeration    Discr;
+    union {
+          struct {
+                  Enumeration Enum_Comp;
+                  int         Int_Comp;
+                  char        Str_Comp [31];
+                  } var_1;
+          struct {
+                  Enumeration E_Comp_2;
+                  char        Str_2_Comp [31];
+                  } var_2;
+          struct {
+                  char        Ch_1_Comp;
+                  char        Ch_2_Comp;
+                  } var_3;
+          } variant;
+      } Rec_Type, *Rec_Pointer;
diff --git a/test/dhrystone/dhry_1.c b/test/dhrystone/dhry_1.c
new file mode 100644
index 0000000..19e73d7
--- /dev/null
+++ b/test/dhrystone/dhry_1.c
@@ -0,0 +1,383 @@
+/*
+ ****************************************************************************
+ *
+ *                   "DHRYSTONE" Benchmark Program
+ *                   -----------------------------
+ *
+ *  Version:    C, Version 2.1
+ *
+ *  File:       dhry_1.c (part 2 of 3)
+ *
+ *  Date:       May 25, 1988
+ *
+ *  Author:     Reinhold P. Weicker
+ *
+ ****************************************************************************
+ */
+
+#include "dhry.h"
+
+/* Global Variables: */
+
+Rec_Pointer     Ptr_Glob,
+                Next_Ptr_Glob;
+int             Int_Glob;
+Boolean         Bool_Glob;
+char            Ch_1_Glob,
+                Ch_2_Glob;
+int             Arr_1_Glob [50];
+int             Arr_2_Glob [50] [50];
+
+// extern char     *malloc ();
+Enumeration     Func_1 ();
+  /* forward declaration necessary since Enumeration may not simply be int */
+
+#ifndef REG
+        Boolean Reg = false;
+#define REG
+        /* REG becomes defined as empty */
+        /* i.e. no register variables   */
+#else
+        Boolean Reg = true;
+#endif
+
+/* variables for time measurement: */
+
+#ifdef TIMES
+struct tms      time_info;
+// extern  int     times ();
+                /* see library function "times" */
+#define Too_Small_Time 120
+                /* Measurements should last at least about 2 seconds */
+#endif
+#ifdef TIME
+extern long     time();
+                /* see library function "time"  */
+#define Too_Small_Time 2
+                /* Measurements should last at least 2 seconds */
+#endif
+
+long            Begin_Time,
+                End_Time,
+                User_Time;
+float           Microseconds,
+                Dhrystones_Per_Second;
+
+/* end of variables for time measurement */
+
+
+main ()
+/*****/
+
+  /* main program, corresponds to procedures        */
+  /* Main and Proc_0 in the Ada version             */
+{
+        One_Fifty       Int_1_Loc;
+  REG   One_Fifty       Int_2_Loc;
+        One_Fifty       Int_3_Loc;
+  REG   char            Ch_Index;
+        Enumeration     Enum_Loc;
+        Str_30          Str_1_Loc;
+        Str_30          Str_2_Loc;
+  REG   int             Run_Index;
+  REG   int             Number_Of_Runs;
+
+  /* Initializations */
+
+  Next_Ptr_Glob = (Rec_Pointer) malloc (sizeof (Rec_Type));
+  Ptr_Glob = (Rec_Pointer) malloc (sizeof (Rec_Type));
+
+  Ptr_Glob->Ptr_Comp                    = Next_Ptr_Glob;
+  Ptr_Glob->Discr                       = Ident_1;
+  Ptr_Glob->variant.var_1.Enum_Comp     = Ident_3;
+  Ptr_Glob->variant.var_1.Int_Comp      = 40;
+  strcpy (Ptr_Glob->variant.var_1.Str_Comp,
+          "DHRYSTONE PROGRAM, SOME STRING");
+  strcpy (Str_1_Loc, "DHRYSTONE PROGRAM, 1'ST STRING");
+
+  Arr_2_Glob [8][7] = 10;
+        /* Was missing in published program. Without this statement,    */
+        /* Arr_2_Glob [8][7] would have an undefined value.             */
+        /* Warning: With 16-Bit processors and Number_Of_Runs > 32000,  */
+        /* overflow may occur for this array element.                   */
+
+  printf ("\n");
+  printf ("Dhrystone Benchmark, Version 2.1 (Language: C)\n");
+  printf ("\n");
+  if (Reg)
+  {
+    printf ("Program compiled with 'register' attribute\n");
+    printf ("\n");
+  }
+  else
+  {
+    printf ("Program compiled without 'register' attribute\n");
+    printf ("\n");
+  }
+  printf ("Please give the number of runs through the benchmark: ");
+  {
+    int n;
+    scanf ("%d", &n);
+    Number_Of_Runs = n;
+  }
+  printf ("\n");
+
+  printf ("Execution starts, %d runs through Dhrystone\n", Number_Of_Runs);
+
+  /***************/
+  /* Start timer */
+  /***************/
+
+#ifdef TIMES
+  times (&time_info);
+  Begin_Time = (long) time_info.tms_utime;
+#endif
+#ifdef TIME
+  Begin_Time = time ( (long *) 0);
+#endif
+
+  for (Run_Index = 1; Run_Index <= Number_Of_Runs; ++Run_Index)
+  {
+
+    Proc_5();
+    Proc_4();
+      /* Ch_1_Glob == 'A', Ch_2_Glob == 'B', Bool_Glob == true */
+    Int_1_Loc = 2;
+    Int_2_Loc = 3;
+    strcpy (Str_2_Loc, "DHRYSTONE PROGRAM, 2'ND STRING");
+    Enum_Loc = Ident_2;
+    Bool_Glob = ! Func_2 (Str_1_Loc, Str_2_Loc);
+      /* Bool_Glob == 1 */
+    while (Int_1_Loc < Int_2_Loc)  /* loop body executed once */
+    {
+      Int_3_Loc = 5 * Int_1_Loc - Int_2_Loc;
+        /* Int_3_Loc == 7 */
+      Proc_7 (Int_1_Loc, Int_2_Loc, &Int_3_Loc);
+        /* Int_3_Loc == 7 */
+      Int_1_Loc += 1;
+    } /* while */
+      /* Int_1_Loc == 3, Int_2_Loc == 3, Int_3_Loc == 7 */
+    Proc_8 (Arr_1_Glob, Arr_2_Glob, Int_1_Loc, Int_3_Loc);
+      /* Int_Glob == 5 */
+    Proc_1 (Ptr_Glob);
+    for (Ch_Index = 'A'; Ch_Index <= Ch_2_Glob; ++Ch_Index)
+                             /* loop body executed twice */
+    {
+      if (Enum_Loc == Func_1 (Ch_Index, 'C'))
+          /* then, not executed */
+        {
+        Proc_6 (Ident_1, &Enum_Loc);
+        strcpy (Str_2_Loc, "DHRYSTONE PROGRAM, 3'RD STRING");
+        Int_2_Loc = Run_Index;
+        Int_Glob = Run_Index;
+        }
+    }
+      /* Int_1_Loc == 3, Int_2_Loc == 3, Int_3_Loc == 7 */
+    Int_2_Loc = Int_2_Loc * Int_1_Loc;
+    Int_1_Loc = Int_2_Loc / Int_3_Loc;
+    Int_2_Loc = 7 * (Int_2_Loc - Int_3_Loc) - Int_1_Loc;
+      /* Int_1_Loc == 1, Int_2_Loc == 13, Int_3_Loc == 7 */
+    Proc_2 (&Int_1_Loc);
+      /* Int_1_Loc == 5 */
+
+  } /* loop "for Run_Index" */
+
+  /**************/
+  /* Stop timer */
+  /**************/
+
+#ifdef TIMES
+  times (&time_info);
+  End_Time = (long) time_info.tms_utime;
+#endif
+#ifdef TIME
+  End_Time = time ( (long *) 0);
+#endif
+
+  printf ("Execution ends\n");
+  printf ("\n");
+  printf ("Final values of the variables used in the benchmark:\n");
+  printf ("\n");
+  printf ("Int_Glob:            %d\n", Int_Glob);
+  printf ("        should be:   %d\n", 5);
+  printf ("Bool_Glob:           %d\n", Bool_Glob);
+  printf ("        should be:   %d\n", 1);
+  printf ("Ch_1_Glob:           %c\n", Ch_1_Glob);
+  printf ("        should be:   %c\n", 'A');
+  printf ("Ch_2_Glob:           %c\n", Ch_2_Glob);
+  printf ("        should be:   %c\n", 'B');
+  printf ("Arr_1_Glob[8]:       %d\n", Arr_1_Glob[8]);
+  printf ("        should be:   %d\n", 7);
+  printf ("Arr_2_Glob[8][7]:    %d\n", Arr_2_Glob[8][7]);
+  printf ("        should be:   Number_Of_Runs + 10\n");
+  printf ("Ptr_Glob->\n");
+  printf ("  Ptr_Comp:          %d\n", (int) Ptr_Glob->Ptr_Comp);
+  printf ("        should be:   (implementation-dependent)\n");
+  printf ("  Discr:             %d\n", Ptr_Glob->Discr);
+  printf ("        should be:   %d\n", 0);
+  printf ("  Enum_Comp:         %d\n", Ptr_Glob->variant.var_1.Enum_Comp);
+  printf ("        should be:   %d\n", 2);
+  printf ("  Int_Comp:          %d\n", Ptr_Glob->variant.var_1.Int_Comp);
+  printf ("        should be:   %d\n", 17);
+  printf ("  Str_Comp:          %s\n", Ptr_Glob->variant.var_1.Str_Comp);
+  printf ("        should be:   DHRYSTONE PROGRAM, SOME STRING\n");
+  printf ("Next_Ptr_Glob->\n");
+  printf ("  Ptr_Comp:          %d\n", (int) Next_Ptr_Glob->Ptr_Comp);
+  printf ("        should be:   (implementation-dependent), same as above\n");
+  printf ("  Discr:             %d\n", Next_Ptr_Glob->Discr);
+  printf ("        should be:   %d\n", 0);
+  printf ("  Enum_Comp:         %d\n", Next_Ptr_Glob->variant.var_1.Enum_Comp);
+  printf ("        should be:   %d\n", 1);
+  printf ("  Int_Comp:          %d\n", Next_Ptr_Glob->variant.var_1.Int_Comp);
+  printf ("        should be:   %d\n", 18);
+  printf ("  Str_Comp:          %s\n",
+                                Next_Ptr_Glob->variant.var_1.Str_Comp);
+  printf ("        should be:   DHRYSTONE PROGRAM, SOME STRING\n");
+  printf ("Int_1_Loc:           %d\n", Int_1_Loc);
+  printf ("        should be:   %d\n", 5);
+  printf ("Int_2_Loc:           %d\n", Int_2_Loc);
+  printf ("        should be:   %d\n", 13);
+  printf ("Int_3_Loc:           %d\n", Int_3_Loc);
+  printf ("        should be:   %d\n", 7);
+  printf ("Enum_Loc:            %d\n", Enum_Loc);
+  printf ("        should be:   %d\n", 1);
+  printf ("Str_1_Loc:           %s\n", Str_1_Loc);
+  printf ("        should be:   DHRYSTONE PROGRAM, 1'ST STRING\n");
+  printf ("Str_2_Loc:           %s\n", Str_2_Loc);
+  printf ("        should be:   DHRYSTONE PROGRAM, 2'ND STRING\n");
+  printf ("\n");
+
+  User_Time = End_Time - Begin_Time;
+
+  if (User_Time < Too_Small_Time)
+  {
+    printf ("Measured time too small to obtain meaningful results\n");
+    printf ("Please increase number of runs\n");
+    printf ("\n");
+  }
+  else
+  {
+#ifdef TIME
+    Microseconds = (float) User_Time * Mic_secs_Per_Second
+                        / (float) Number_Of_Runs;
+    Dhrystones_Per_Second = (float) Number_Of_Runs / (float) User_Time;
+#else
+    Microseconds = (float) User_Time * Mic_secs_Per_Second
+                        / ((float) HZ * ((float) Number_Of_Runs));
+    Dhrystones_Per_Second = ((float) HZ * (float) Number_Of_Runs)
+                        / (float) User_Time;
+#endif
+    printf ("Microseconds for one run through Dhrystone: ");
+    printf ("%6.1f \n", Microseconds);
+    printf ("Dhrystones per Second:                      ");
+    printf ("%6.1f \n", Dhrystones_Per_Second);
+    printf ("\n");
+  }
+
+}
+
+
+Proc_1 (Ptr_Val_Par)
+/******************/
+
+REG Rec_Pointer Ptr_Val_Par;
+    /* executed once */
+{
+  REG Rec_Pointer Next_Record = Ptr_Val_Par->Ptr_Comp;
+                                        /* == Ptr_Glob_Next */
+  /* Local variable, initialized with Ptr_Val_Par->Ptr_Comp,    */
+  /* corresponds to "rename" in Ada, "with" in Pascal           */
+
+  structassign (*Ptr_Val_Par->Ptr_Comp, *Ptr_Glob);
+  Ptr_Val_Par->variant.var_1.Int_Comp = 5;
+  Next_Record->variant.var_1.Int_Comp
+        = Ptr_Val_Par->variant.var_1.Int_Comp;
+  Next_Record->Ptr_Comp = Ptr_Val_Par->Ptr_Comp;
+  Proc_3 (&Next_Record->Ptr_Comp);
+    /* Ptr_Val_Par->Ptr_Comp->Ptr_Comp
+                        == Ptr_Glob->Ptr_Comp */
+  if (Next_Record->Discr == Ident_1)
+    /* then, executed */
+  {
+    Next_Record->variant.var_1.Int_Comp = 6;
+    Proc_6 (Ptr_Val_Par->variant.var_1.Enum_Comp,
+           &Next_Record->variant.var_1.Enum_Comp);
+    Next_Record->Ptr_Comp = Ptr_Glob->Ptr_Comp;
+    Proc_7 (Next_Record->variant.var_1.Int_Comp, 10,
+           &Next_Record->variant.var_1.Int_Comp);
+  }
+  else /* not executed */
+    structassign (*Ptr_Val_Par, *Ptr_Val_Par->Ptr_Comp);
+} /* Proc_1 */
+
+
+Proc_2 (Int_Par_Ref)
+/******************/
+    /* executed once */
+    /* *Int_Par_Ref == 1, becomes 4 */
+
+One_Fifty   *Int_Par_Ref;
+{
+  One_Fifty  Int_Loc;
+  Enumeration   Enum_Loc;
+
+  Int_Loc = *Int_Par_Ref + 10;
+  do /* executed once */
+    if (Ch_1_Glob == 'A')
+      /* then, executed */
+    {
+      Int_Loc -= 1;
+      *Int_Par_Ref = Int_Loc - Int_Glob;
+      Enum_Loc = Ident_1;
+    } /* if */
+  while (Enum_Loc != Ident_1); /* true */
+} /* Proc_2 */
+
+
+Proc_3 (Ptr_Ref_Par)
+/******************/
+    /* executed once */
+    /* Ptr_Ref_Par becomes Ptr_Glob */
+
+Rec_Pointer *Ptr_Ref_Par;
+
+{
+  if (Ptr_Glob != Null)
+    /* then, executed */
+    *Ptr_Ref_Par = Ptr_Glob->Ptr_Comp;
+  Proc_7 (10, Int_Glob, &Ptr_Glob->variant.var_1.Int_Comp);
+} /* Proc_3 */
+
+
+Proc_4 () /* without parameters */
+/*******/
+    /* executed once */
+{
+  Boolean Bool_Loc;
+
+  Bool_Loc = Ch_1_Glob == 'A';
+  Bool_Glob = Bool_Loc | Bool_Glob;
+  Ch_2_Glob = 'B';
+} /* Proc_4 */
+
+
+Proc_5 () /* without parameters */
+/*******/
+    /* executed once */
+{
+  Ch_1_Glob = 'A';
+  Bool_Glob = false;
+} /* Proc_5 */
+
+
+        /* Procedure for the assignment of structures,          */
+        /* if the C compiler doesn't support this feature       */
+#ifdef  NOSTRUCTASSIGN
+memcpy (d, s, l)
+register char   *d;
+register char   *s;
+register int    l;
+{
+        while (l--) *d++ = *s++;
+}
+#endif
diff --git a/test/dhrystone/dhry_2.c b/test/dhrystone/dhry_2.c
new file mode 100644
index 0000000..a7c4f50
--- /dev/null
+++ b/test/dhrystone/dhry_2.c
@@ -0,0 +1,191 @@
+/*
+ ****************************************************************************
+ *
+ *                   "DHRYSTONE" Benchmark Program
+ *                   -----------------------------
+ *
+ *  Version:    C, Version 2.1
+ *
+ *  File:       dhry_2.c (part 3 of 3)
+ *
+ *  Date:       May 25, 1988
+ *
+ *  Author:     Reinhold P. Weicker
+ *
+ ****************************************************************************
+ */
+
+#include "dhry.h"
+
+#ifndef REG
+#define REG
+        /* REG becomes defined as empty */
+        /* i.e. no register variables   */
+#endif
+
+extern  int     Int_Glob;
+extern  char    Ch_1_Glob;
+
+
+Proc_6 (Enum_Val_Par, Enum_Ref_Par)
+/*********************************/
+    /* executed once */
+    /* Enum_Val_Par == Ident_3, Enum_Ref_Par becomes Ident_2 */
+
+Enumeration  Enum_Val_Par;
+Enumeration *Enum_Ref_Par;
+{
+  *Enum_Ref_Par = Enum_Val_Par;
+  if (! Func_3 (Enum_Val_Par))
+    /* then, not executed */
+    *Enum_Ref_Par = Ident_4;
+  switch (Enum_Val_Par)
+  {
+    case Ident_1:
+      *Enum_Ref_Par = Ident_1;
+      break;
+    case Ident_2:
+      if (Int_Glob > 100)
+        /* then */
+      *Enum_Ref_Par = Ident_1;
+      else *Enum_Ref_Par = Ident_4;
+      break;
+    case Ident_3: /* executed */
+      *Enum_Ref_Par = Ident_2;
+      break;
+    case Ident_4: break;
+    case Ident_5:
+      *Enum_Ref_Par = Ident_3;
+      break;
+  } /* switch */
+} /* Proc_6 */
+
+
+Proc_7 (Int_1_Par_Val, Int_2_Par_Val, Int_Par_Ref)
+/**********************************************/
+    /* executed three times                                      */
+    /* first call:      Int_1_Par_Val == 2, Int_2_Par_Val == 3,  */
+    /*                  Int_Par_Ref becomes 7                    */
+    /* second call:     Int_1_Par_Val == 10, Int_2_Par_Val == 5, */
+    /*                  Int_Par_Ref becomes 17                   */
+    /* third call:      Int_1_Par_Val == 6, Int_2_Par_Val == 10, */
+    /*                  Int_Par_Ref becomes 18                   */
+One_Fifty       Int_1_Par_Val;
+One_Fifty       Int_2_Par_Val;
+One_Fifty      *Int_Par_Ref;
+{
+  One_Fifty Int_Loc;
+
+  Int_Loc = Int_1_Par_Val + 2;
+  *Int_Par_Ref = Int_2_Par_Val + Int_Loc;
+} /* Proc_7 */
+
+
+Proc_8 (Arr_1_Par_Ref, Arr_2_Par_Ref, Int_1_Par_Val, Int_2_Par_Val)
+/*********************************************************************/
+    /* executed once      */
+    /* Int_Par_Val_1 == 3 */
+    /* Int_Par_Val_2 == 7 */
+Arr_1_Dim       Arr_1_Par_Ref;
+Arr_2_Dim       Arr_2_Par_Ref;
+int             Int_1_Par_Val;
+int             Int_2_Par_Val;
+{
+  REG One_Fifty Int_Index;
+  REG One_Fifty Int_Loc;
+
+  Int_Loc = Int_1_Par_Val + 5;
+  Arr_1_Par_Ref [Int_Loc] = Int_2_Par_Val;
+  Arr_1_Par_Ref [Int_Loc+1] = Arr_1_Par_Ref [Int_Loc];
+  Arr_1_Par_Ref [Int_Loc+30] = Int_Loc;
+  for (Int_Index = Int_Loc; Int_Index <= Int_Loc+1; ++Int_Index)
+    Arr_2_Par_Ref [Int_Loc] [Int_Index] = Int_Loc;
+  Arr_2_Par_Ref [Int_Loc] [Int_Loc-1] += 1;
+  Arr_2_Par_Ref [Int_Loc+20] [Int_Loc] = Arr_1_Par_Ref [Int_Loc];
+  Int_Glob = 5;
+} /* Proc_8 */
+
+
+Enumeration Func_1 (Ch_1_Par_Val, Ch_2_Par_Val)
+/*************************************************/
+    /* executed three times                                         */
+    /* first call:      Ch_1_Par_Val == 'H', Ch_2_Par_Val == 'R'    */
+    /* second call:     Ch_1_Par_Val == 'A', Ch_2_Par_Val == 'C'    */
+    /* third call:      Ch_1_Par_Val == 'B', Ch_2_Par_Val == 'C'    */
+
+Capital_Letter   Ch_1_Par_Val;
+Capital_Letter   Ch_2_Par_Val;
+{
+  Capital_Letter        Ch_1_Loc;
+  Capital_Letter        Ch_2_Loc;
+
+  Ch_1_Loc = Ch_1_Par_Val;
+  Ch_2_Loc = Ch_1_Loc;
+  if (Ch_2_Loc != Ch_2_Par_Val)
+    /* then, executed */
+    return (Ident_1);
+  else  /* not executed */
+  {
+    Ch_1_Glob = Ch_1_Loc;
+    return (Ident_2);
+   }
+} /* Func_1 */
+
+
+Boolean Func_2 (Str_1_Par_Ref, Str_2_Par_Ref)
+/*************************************************/
+    /* executed once */
+    /* Str_1_Par_Ref == "DHRYSTONE PROGRAM, 1'ST STRING" */
+    /* Str_2_Par_Ref == "DHRYSTONE PROGRAM, 2'ND STRING" */
+
+Str_30  Str_1_Par_Ref;
+Str_30  Str_2_Par_Ref;
+{
+  REG One_Thirty        Int_Loc;
+      Capital_Letter    Ch_Loc;
+
+  Int_Loc = 2;
+  while (Int_Loc <= 2) /* loop body executed once */
+    if (Func_1 (Str_1_Par_Ref[Int_Loc],
+                Str_2_Par_Ref[Int_Loc+1]) == Ident_1)
+      /* then, executed */
+    {
+      Ch_Loc = 'A';
+      Int_Loc += 1;
+    } /* if, while */
+  if (Ch_Loc >= 'W' && Ch_Loc < 'Z')
+    /* then, not executed */
+    Int_Loc = 7;
+  if (Ch_Loc == 'R')
+    /* then, not executed */
+    return (true);
+  else /* executed */
+  {
+    if (strcmp (Str_1_Par_Ref, Str_2_Par_Ref) > 0)
+      /* then, not executed */
+    {
+      Int_Loc += 7;
+      Int_Glob = Int_Loc;
+      return (true);
+    }
+    else /* executed */
+      return (false);
+  } /* if Ch_Loc */
+} /* Func_2 */
+
+
+Boolean Func_3 (Enum_Par_Val)
+/***************************/
+    /* executed once        */
+    /* Enum_Par_Val == Ident_3 */
+Enumeration Enum_Par_Val;
+{
+  Enumeration Enum_Loc;
+
+  Enum_Loc = Enum_Par_Val;
+  if (Enum_Loc == Ident_3)
+    /* then, executed */
+    return (true);
+  else /* not executed */
+    return (false);
+} /* Func_3 */