From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- cfrontend/SimplExpr.v | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) (limited to 'cfrontend/SimplExpr.v') diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index 097dc589..4fe8105d 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -10,7 +10,7 @@ (* *) (* *********************************************************************) -(** Translation from Compcert C to Clight. +(** Translation from Compcert C to Clight. Side effects are pulled out of Compcert C expressions. *) Require Import Coqlib. @@ -82,11 +82,11 @@ Local Open Scope gensym_monad_scope. Parameter first_unused_ident: unit -> ident. -Definition initial_generator (x: unit) : generator := +Definition initial_generator (x: unit) : generator := mkgenerator (first_unused_ident x) nil. Definition gensym (ty: type): mon ident := - fun (g: generator) => + fun (g: generator) => Res (gen_next g) (mkgenerator (Psucc (gen_next g)) ((gen_next g, ty) :: gen_trail g)) (Ple_succ (gen_next g)). @@ -119,7 +119,7 @@ Function eval_simpl_expr (a: expr) : option val := | Econst_float n _ => Some(Vfloat n) | Econst_single n _ => Some(Vsingle n) | Econst_long n _ => Some(Vlong n) - | Ecast b ty => + | Ecast b ty => match eval_simpl_expr b with | None => None | Some v => sem_cast v (typeof b) ty @@ -149,7 +149,7 @@ Definition transl_incrdecr (id: incr_or_decr) (a: expr) (ty: type) : expr := to dereference a l-value [l] and store its result in temporary variable [id]. *) Definition chunk_for_volatile_type (ty: type) : option memory_chunk := - if type_is_volatile ty + if type_is_volatile ty then match access_mode ty with By_value chunk => Some chunk | _ => None end else None. @@ -201,7 +201,7 @@ Inductive set_destination : Type := | SDbase (tycast ty: type) (tmp: ident) | SDcons (tycast ty: type) (tmp: ident) (sd: set_destination). -Inductive destination : Type := +Inductive destination : Type := | For_val | For_effects | For_set (sd: set_destination). @@ -277,7 +277,7 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement | For_val => do t <- gensym ty; do (sl2, a2) <- transl_expr (For_set (sd_seqbool_val t ty)) r2; - ret (sl1 ++ + ret (sl1 ++ makeif a1 (makeseq sl2) (Sset t (Econst_int Int.zero ty)) :: nil, Etempvar t ty) | For_effects => @@ -285,7 +285,7 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement ret (sl1 ++ makeif a1 (makeseq sl2) Sskip :: nil, dummy_expr) | For_set sd => do (sl2, a2) <- transl_expr (For_set (sd_seqbool_set ty sd)) r2; - ret (sl1 ++ + ret (sl1 ++ makeif a1 (makeseq sl2) (makeseq (do_set sd (Econst_int Int.zero ty))) :: nil, dummy_expr) end @@ -295,7 +295,7 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement | For_val => do t <- gensym ty; do (sl2, a2) <- transl_expr (For_set (sd_seqbool_val t ty)) r2; - ret (sl1 ++ + ret (sl1 ++ makeif a1 (Sset t (Econst_int Int.one ty)) (makeseq sl2) :: nil, Etempvar t ty) | For_effects => @@ -303,7 +303,7 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement ret (sl1 ++ makeif a1 Sskip (makeseq sl2) :: nil, dummy_expr) | For_set sd => do (sl2, a2) <- transl_expr (For_set (sd_seqbool_set ty sd)) r2; - ret (sl1 ++ + ret (sl1 ++ makeif a1 (makeseq (do_set sd (Econst_int Int.one ty))) (makeseq sl2) :: nil, dummy_expr) end @@ -336,7 +336,7 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement match dst with | For_val | For_set _ => do t <- gensym ty2; - ret (finish dst + ret (finish dst (sl1 ++ sl2 ++ Sset t a2 :: make_assign a1 (Etempvar t ty2) :: nil) (Ecast (Etempvar t ty2) ty1)) | For_effects => -- cgit