diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-04-02 16:25:25 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-04-02 16:25:25 +0200 |
commit | 170284b51766112e29d6bbfe519bad9f6da95269 (patch) | |
tree | 13a163ccee48cee0512a8af484b394623cdce030 /cfrontend/Initializers.v | |
parent | 2e30ad9698a6f24a8a746f68b30c235913006392 (diff) | |
parent | 959432fa13a899290db5236f93575a8bfdc13bb5 (diff) | |
download | compcert-kvx-170284b51766112e29d6bbfe519bad9f6da95269.tar.gz compcert-kvx-170284b51766112e29d6bbfe519bad9f6da95269.zip |
Merge branch 'master' into dwarf
Diffstat (limited to 'cfrontend/Initializers.v')
-rw-r--r-- | cfrontend/Initializers.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index 025960d7..7af4792a 100644 --- a/cfrontend/Initializers.v +++ b/cfrontend/Initializers.v @@ -74,7 +74,7 @@ Fixpoint constval (ce: composite_env) (a: expr) : res val := constval ce l | Eunop op r1 ty => do v1 <- constval ce r1; - match sem_unary_operation op v1 (typeof r1) with + match sem_unary_operation op v1 (typeof r1) Mem.empty with | Some v => OK v | None => Error(msg "undefined unary operation") end @@ -94,7 +94,7 @@ Fixpoint constval (ce: composite_env) (a: expr) : res val := | Eseqand r1 r2 ty => do v1 <- constval ce r1; do v2 <- constval ce r2; - match bool_val v1 (typeof r1) with + match bool_val v1 (typeof r1) Mem.empty with | Some true => do_cast v2 (typeof r2) type_bool | Some false => OK (Vint Int.zero) | None => Error(msg "undefined && operation") @@ -102,7 +102,7 @@ Fixpoint constval (ce: composite_env) (a: expr) : res val := | Eseqor r1 r2 ty => do v1 <- constval ce r1; do v2 <- constval ce r2; - match bool_val v1 (typeof r1) with + match bool_val v1 (typeof r1) Mem.empty with | Some false => do_cast v2 (typeof r2) type_bool | Some true => OK (Vint Int.one) | None => Error(msg "undefined || operation") @@ -111,7 +111,7 @@ Fixpoint constval (ce: composite_env) (a: expr) : res val := do v1 <- constval ce r1; do v2 <- constval ce r2; do v3 <- constval ce r3; - match bool_val v1 (typeof r1) with + match bool_val v1 (typeof r1) Mem.empty with | Some true => do_cast v2 (typeof r2) ty | Some false => do_cast v3 (typeof r3) ty | None => Error(msg "condition is undefined") |