diff options
author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2015-04-01 18:27:15 +0200 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2015-04-01 18:27:15 +0200 |
commit | 68e2ce02f8d69b26c9cea6e0d338f855cbea3ace (patch) | |
tree | 98acb09c398112bff31ce34c0857aa0f4e9b8e23 /cfrontend/Initializers.v | |
parent | 5d6febecb8c0f90a627033744f6f62164645a1a4 (diff) | |
parent | daccc2928e6410c4e8c886ea7d019fd9a071b931 (diff) | |
download | compcert-68e2ce02f8d69b26c9cea6e0d338f855cbea3ace.tar.gz compcert-68e2ce02f8d69b26c9cea6e0d338f855cbea3ace.zip |
Merge pull request #31 from AbsInt/null-ptr-cmp
Revised semantics of comparisons between a pointer and 0.
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") |