Updated PR by removing whitespaces. Bug 17450.

7 files changed, 54 insertions, 54 deletions

diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index d9c21a9c..9d3697bd 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -52,7 +52,7 @@ let option_S = ref false
 let option_c = ref false
 let option_v = ref false
 let option_interp = ref false
-let option_small_data = 
+let option_small_data =
   ref (if Configuration.arch = "powerpc"
        && Configuration.abi = "eabi"
        && Configuration.system = "diab"
diff --git a/driver/Compiler.v b/driver/Compiler.v
index 3920665e..ea5849ec 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -159,7 +159,7 @@ Definition transf_cminor_program (p: Cminor.program) : res Asm.program :=
   @@@ transf_rtl_program.
 
 Definition transf_clight_program (p: Clight.program) : res Asm.program :=
-  OK p 
+  OK p
    @@ print print_Clight
   @@@ time "Simplification of locals" SimplLocals.transf_program
   @@@ time "C#minor generation" Cshmgen.transl_program
@@ -167,7 +167,7 @@ Definition transf_clight_program (p: Clight.program) : res Asm.program :=
   @@@ transf_cminor_program.
 
 Definition transf_c_program (p: Csyntax.program) : res Asm.program :=
-  OK p 
+  OK p
   @@@ time "Clight generation" SimplExpr.transl_program
   @@@ transf_clight_program.
 
@@ -182,14 +182,14 @@ Lemma print_identity:
   forall (A: Type) (printer: A -> unit) (prog: A),
   print printer prog = prog.
 Proof.
-  intros; unfold print. destruct (printer prog); auto. 
+  intros; unfold print. destruct (printer prog); auto.
 Qed.
 
 Lemma compose_print_identity:
-  forall (A: Type) (x: res A) (f: A -> unit), 
+  forall (A: Type) (x: res A) (f: A -> unit),
   x @@ print f = x.
 Proof.
-  intros. destruct x; simpl. rewrite print_identity. auto. auto. 
+  intros. destruct x; simpl. rewrite print_identity. auto. auto.
 Qed.
 
 Remark forward_simulation_identity:
@@ -199,8 +199,8 @@ Proof.
 - auto.
 - exists s1; auto.
 - subst s2; auto.
-- subst s2. exists s1'; auto. 
-Qed. 
+- subst s2. exists s1'; auto.
+Qed.
 
 Lemma total_if_simulation:
   forall (A: Type) (sem: A -> semantics) (flag: unit -> bool) (f: A -> A) (prog: A),
@@ -259,15 +259,15 @@ Proof.
   destruct (partial_if debug Debugvar.transf_program p7) as [p71|] eqn:?; simpl in H; try discriminate.
   destruct (Stacking.transf_program p71) as [p8|] eqn:?; simpl in H; try discriminate.
   apply compose_forward_simulation with (RTL.semantics p1).
-    apply total_if_simulation. apply Tailcallproof.transf_program_correct. 
+    apply total_if_simulation. apply Tailcallproof.transf_program_correct.
   apply compose_forward_simulation with (RTL.semantics p11).
     apply Inliningproof.transf_program_correct; auto.
   apply compose_forward_simulation with (RTL.semantics p12).
-    apply Renumberproof.transf_program_correct. 
+    apply Renumberproof.transf_program_correct.
   apply compose_forward_simulation with (RTL.semantics p2).
     apply total_if_simulation. apply Constpropproof.transf_program_correct.
   apply compose_forward_simulation with (RTL.semantics p21).
-    apply total_if_simulation. apply Renumberproof.transf_program_correct. 
+    apply total_if_simulation. apply Renumberproof.transf_program_correct.
   apply compose_forward_simulation with (RTL.semantics p3).
     eapply partial_if_simulation; eauto.  apply CSEproof.transf_program_correct.
   apply compose_forward_simulation with (RTL.semantics p31).
@@ -281,7 +281,7 @@ Proof.
   apply compose_forward_simulation with (Linear.semantics p6).
     apply Linearizeproof.transf_program_correct; auto.
   apply compose_forward_simulation with (Linear.semantics p7).
-    apply CleanupLabelsproof.transf_program_correct. 
+    apply CleanupLabelsproof.transf_program_correct.
   apply compose_forward_simulation with (Linear.semantics p71).
     eapply partial_if_simulation; eauto. apply Debugvarproof.transf_program_correct.
   apply compose_forward_simulation with (Mach.semantics Asmgenproof0.return_address_offset p8).
@@ -289,8 +289,8 @@ Proof.
     exact Asmgenproof.return_address_exists.
     auto.
   apply Asmgenproof.transf_program_correct; eauto.
-  split. auto. 
-  apply forward_to_backward_simulation. auto. 
+  split. auto.
+  apply forward_to_backward_simulation. auto.
   apply RTL.semantics_receptive.
   apply Asm.semantics_determinate.
 Qed.
@@ -305,15 +305,15 @@ Proof.
   assert (F: forward_simulation (Cminor.semantics p) (Asm.semantics tp)).
   unfold transf_cminor_program, time in H.
   repeat rewrite compose_print_identity in H.
-  simpl in H. 
+  simpl in H.
   destruct (Selection.sel_program p) as [p1|] eqn:?; simpl in H; try discriminate.
   destruct (RTLgen.transl_program p1) as [p2|] eqn:?; simpl in H; try discriminate.
   eapply compose_forward_simulation. apply Selectionproof.transf_program_correct. eauto.
   eapply compose_forward_simulation. apply RTLgenproof.transf_program_correct. eassumption.
   exact (fst (transf_rtl_program_correct _ _ H)).
 
-  split. auto. 
-  apply forward_to_backward_simulation. auto. 
+  split. auto.
+  apply forward_to_backward_simulation. auto.
   apply Cminor.semantics_receptive.
   apply Asm.semantics_determinate.
 Qed.
@@ -324,7 +324,7 @@ Theorem transf_clight_program_correct:
   forward_simulation (Clight.semantics1 p) (Asm.semantics tp)
   * backward_simulation (Clight.semantics1 p) (Asm.semantics tp).
 Proof.
-  intros. 
+  intros.
   assert (F: forward_simulation (Clight.semantics1 p) (Asm.semantics tp)).
   revert H; unfold transf_clight_program, time; simpl.
   rewrite print_identity.
@@ -335,10 +335,10 @@ Proof.
   eapply compose_forward_simulation. apply SimplLocalsproof.transf_program_correct. eauto.
   eapply compose_forward_simulation. apply Cshmgenproof.transl_program_correct. eauto.
   eapply compose_forward_simulation. apply Cminorgenproof.transl_program_correct. eauto.
-  exact (fst (transf_cminor_program_correct _ _ EQ3)). 
+  exact (fst (transf_cminor_program_correct _ _ EQ3)).
 
-  split. auto. 
-  apply forward_to_backward_simulation. auto. 
+  split. auto.
+  apply forward_to_backward_simulation. auto.
   apply Clight.semantics_receptive.
   apply Asm.semantics_determinate.
 Qed.
@@ -355,9 +355,9 @@ Proof.
   caseEq (SimplExpr.transl_program p); simpl; try congruence; intros p0 EQ0.
   intros EQ1.
   eapply compose_forward_simulation. apply SimplExprproof.transl_program_correct. eauto.
-  exact (fst (transf_clight_program_correct _ _ EQ1)). 
+  exact (fst (transf_clight_program_correct _ _ EQ1)).
 
-  split. auto. 
+  split. auto.
   apply forward_to_backward_simulation.
   apply factor_forward_simulation. auto. eapply sd_traces. eapply Asm.semantics_determinate.
   apply atomic_receptive. apply Cstrategy.semantics_strongly_receptive.
@@ -369,10 +369,10 @@ Theorem transf_c_program_correct:
   transf_c_program p = OK tp ->
   backward_simulation (Csem.semantics p) (Asm.semantics tp).
 Proof.
-  intros. 
+  intros.
   apply compose_backward_simulation with (atomic (Cstrategy.semantics p)).
   eapply sd_traces; eapply Asm.semantics_determinate.
-  apply factor_backward_simulation. 
+  apply factor_backward_simulation.
   apply Cstrategy.strategy_simulation.
   apply Csem.semantics_single_events.
   eapply ssr_well_behaved; eapply Cstrategy.semantics_strongly_receptive.
diff --git a/driver/Complements.v b/driver/Complements.v
index 57351a2a..8651f2ff 100644
--- a/driver/Complements.v
+++ b/driver/Complements.v
@@ -44,7 +44,7 @@ Theorem transf_c_program_preservation:
   program_behaves (Asm.semantics tp) beh ->
   exists beh', program_behaves (Csem.semantics p) beh' /\ behavior_improves beh' beh.
 Proof.
-  intros. eapply backward_simulation_behavior_improves; eauto. 
+  intros. eapply backward_simulation_behavior_improves; eauto.
   apply transf_c_program_correct; auto.
 Qed.
 
@@ -81,7 +81,7 @@ Proof.
   assert (WBT: forall p, well_behaved_traces (Cstrategy.semantics p)).
     intros. eapply ssr_well_behaved. apply Cstrategy.semantics_strongly_receptive.
   intros. intuition.
-  eapply forward_simulation_behavior_improves; eauto. 
+  eapply forward_simulation_behavior_improves; eauto.
     apply (fst (transf_cstrategy_program_correct _ _ H)).
   exploit backward_simulation_behavior_improves.
     apply (snd (transf_cstrategy_program_correct _ _ H)).
@@ -92,7 +92,7 @@ Proof.
   exploit backward_simulation_same_safe_behavior.
     apply (snd (transf_cstrategy_program_correct _ _ H)).
     intros. rewrite <- atomic_behaviors in H2; eauto. eauto.
-    intros. rewrite atomic_behaviors; auto. 
+    intros. rewrite atomic_behaviors; auto.
 Qed.
 
 (** We can also use the alternate big-step semantics for [Cstrategy]
@@ -114,7 +114,7 @@ Proof.
   apply behavior_bigstep_terminates with (Cstrategy.bigstep_semantics p); auto.
   apply Cstrategy.bigstep_semantics_sound.
   exploit (behavior_bigstep_diverges (Cstrategy.bigstep_semantics_sound p)). eassumption.
-  intros [A | [t [A B]]]. 
+  intros [A | [t [A B]]].
   left. apply transf_cstrategy_program_preservation with p; auto. red; auto.
   right; exists t; split; auto. apply transf_cstrategy_program_preservation with p; auto. red; auto.
 Qed.
@@ -125,10 +125,10 @@ Qed.
   of the source C program satisfies a given specification
   (a predicate on the observable behavior of the program),
   then all executions of the produced Asm program satisfy
-  this specification as well.  
+  this specification as well.
 
   We first show this result for specifications that are stable
-  under the [behavior_improves] relation. *) 
+  under the [behavior_improves] relation. *)
 
 Section SPECS_PRESERVED.
 
@@ -145,7 +145,7 @@ Theorem transf_c_program_preserves_spec:
 Proof.
   intros.
   exploit transf_c_program_preservation; eauto. intros [beh' [A B]].
-  apply spec_stable with beh'; auto. 
+  apply spec_stable with beh'; auto.
 Qed.
 
 End SPECS_PRESERVED.
@@ -166,9 +166,9 @@ Theorem transf_c_program_preserves_safety_spec:
   (forall beh, program_behaves (Csem.semantics p) beh -> spec beh) ->
   (forall beh, program_behaves (Asm.semantics tp) beh -> spec beh).
 Proof.
-  intros. eapply transf_c_program_preserves_spec; eauto. 
-  intros. destruct H2. congruence. destruct H2 as [t [EQ1 EQ2]]. 
-  subst beh1. elim (spec_safety _ H3). 
+  intros. eapply transf_c_program_preserves_spec; eauto.
+  intros. destruct H2. congruence. destruct H2 as [t [EQ1 EQ2]].
+  subst beh1. elim (spec_safety _ H3).
 Qed.
 
 End SAFETY_PRESERVED.
@@ -196,8 +196,8 @@ Proof.
   destruct H2 as [t [C D]]. subst.
   destruct A as [b1 E]. destruct D as [b2 F].
   destruct b1; simpl in E; inv E.
-  exists t1; split; auto. 
-  exists (behavior_app t0 b2); apply behavior_app_assoc. 
+  exists t1; split; auto.
+  exists (behavior_app t0 b2); apply behavior_app_assoc.
 Qed.
 
 End LIVENESS_PRESERVED.
diff --git a/driver/Configuration.ml b/driver/Configuration.ml
index 41325368..1f05afd8 100644
--- a/driver/Configuration.ml
+++ b/driver/Configuration.ml
@@ -30,7 +30,7 @@ let ini_file_name =
     try
       List.find  Sys.file_exists files
     with Not_found ->
-      begin 
+      begin
         eprintf "Cannot find compcert.ini configuration file.\n";
         exit 2
       end
@@ -73,19 +73,19 @@ let get_config_list key =
 let prepro = get_config_list "prepro"
 let asm = get_config_list "asm"
 let linker = get_config_list "linker"
-let arch = 
+let arch =
   match get_config_string "arch" with
   | "powerpc"|"arm"|"ia32" as a -> a
   | v -> bad_config "arch" [v]
 let model = get_config_string "model"
 let abi = get_config_string "abi"
 let system = get_config_string "system"
-let has_runtime_lib = 
+let has_runtime_lib =
   match get_config_string "has_runtime_lib" with
   | "true" -> true
   | "false" -> false
   | v -> bad_config "has_runtime_lib" [v]
-let has_standard_headers = 
+let has_standard_headers =
   match get_config_string "has_standard_headers" with
   | "true" -> true
   | "false" -> false
@@ -95,7 +95,7 @@ let stdlib_path =
     get_config_string "stdlib_path"
   else
     ""
-let asm_supports_cfi = 
+let asm_supports_cfi =
   match get_config_string "asm_supports_cfi" with
   | "true" -> true
   | "false" -> false
@@ -117,7 +117,7 @@ type struct_return_style =
   | SR_int1248      (* return by content if size is 1, 2, 4 or 8 bytes *)
   | SR_int1to4      (* return by content if size is <= 4 *)
   | SR_int1to8      (* return by content if size is <= 8 *)
-  | SR_ref          (* always return by assignment to a reference 
+  | SR_ref          (* always return by assignment to a reference
                        given as extra argument *)
 
 let struct_passing_style =
diff --git a/driver/Configuration.mli b/driver/Configuration.mli
index f82ce213..1d048ac4 100644
--- a/driver/Configuration.mli
+++ b/driver/Configuration.mli
@@ -46,7 +46,7 @@ type struct_return_style =
   | SR_int1248      (* return by content if size is 1, 2, 4 or 8 bytes *)
   | SR_int1to4      (* return by content if size is <= 4 *)
   | SR_int1to8      (* return by content if size is <= 8 *)
-  | SR_ref          (* always return by assignment to a reference 
+  | SR_ref          (* always return by assignment to a reference
                        given as extra argument *)
 
 val struct_passing_style: struct_passing_style
diff --git a/driver/Driver.ml b/driver/Driver.ml
index c7d9984e..4b58fb4d 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -188,7 +188,7 @@ let compile_c_ast sourcename csyntax ofile debug =
     | Errors.Error msg ->
         eprintf "%s: %a" sourcename print_error msg;
         exit 2 in
-  (* Dump Asm in binary and JSON format *)  
+  (* Dump Asm in binary and JSON format *)
   if !option_sdump then
     begin
       dump_asm asm (output_filename sourcename ".c" ".sdump");
@@ -518,7 +518,7 @@ let unset_all opts = List.iter (fun r -> r := false) opts
 let num_source_files = ref 0
 
 let num_input_files = ref 0
-    
+
 let cmdline_actions =
   let f_opt name ref =
     [Exact("-f" ^ name), Set ref; Exact("-fno-" ^ name), Unset ref] in
@@ -570,8 +570,8 @@ let cmdline_actions =
 (* Linking options *)
   Prefix "-l", Self push_linker_arg;
   Prefix "-L", Self push_linker_arg;
-  Exact "-T", String (fun s -> if Configuration.system = "diab" then 
-    push_linker_arg ("-Wm"^s) 
+  Exact "-T", String (fun s -> if Configuration.system = "diab" then
+    push_linker_arg ("-Wm"^s)
   else begin
       push_linker_arg ("-T");
       push_linker_arg(s)
diff --git a/driver/Interp.ml b/driver/Interp.ml
index 579b936d..fb1c85f0 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -98,7 +98,7 @@ let name_of_function prog fn =
   in find_name prog.prog_defs
 
 let invert_local_variable e b =
-  Maps.PTree.fold 
+  Maps.PTree.fold
     (fun res id (b', _) -> if b = b' then Some id else res)
     e None
 
@@ -176,7 +176,7 @@ let rec compare_cont k1 k2 =
   match k1, k2 with
   | Kstop, Kstop -> 0
   | Kdo k1, Kdo k2 -> compare_cont k1 k2
-  | Kseq(s1, k1), Kseq(s2, k2) ->  
+  | Kseq(s1, k1), Kseq(s2, k2) ->
       let c = compare s1 s2 in if c <> 0 then c else compare_cont k1 k2
   | Kifthenelse(s1, s1', k1), Kifthenelse(s2, s2', k2) ->
       let c = compare (s1,s1') (s2,s2') in
@@ -273,7 +273,7 @@ let extract_string m blk ofs =
         if c = '\000' then begin
           Some(Buffer.contents b)
         end else begin
-          Buffer.add_char b c; 
+          Buffer.add_char b c;
           extract blk (Z.succ ofs)
         end
     | _ ->
@@ -325,7 +325,7 @@ let format_value m flags length conv arg =
   | 'p', "", _ ->
       "<int or pointer argument expected>"
   | _, _, _ ->
-      "<unrecognized format>"      
+      "<unrecognized format>"
 
 let do_printf m fmt args =
 
@@ -374,7 +374,7 @@ let convert_external_arg ge v t =
   | Vfloat f, AST.Tfloat -> Some (EVfloat f)
   | Vsingle f, AST.Tsingle -> Some (EVsingle f)
   | Vlong n, AST.Tlong -> Some (EVlong n)
-  | Vptr(b, ofs), AST.Tint -> 
+  | Vptr(b, ofs), AST.Tint ->
       Senv.invert_symbol ge b >>= fun id -> Some (EVptr_global(id, ofs))
   | _, _ -> None
 
@@ -565,7 +565,7 @@ let rec explore_all p prog ge time states =
     if nextstates <> [] then explore_all p prog ge (time + 1) nextstates
 
 (* The variant of the source program used to build the world for
-   executing events.  
+   executing events.
    Volatile variables are turned into non-volatile ones, so that
      reads and writes can be performed.
    Other variables are turned into empty vars, so that