diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-02-20 09:52:30 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-02-20 09:52:30 +0000 |
| commit | 842190a7a7c85b15f663fdf299a1f015a774f416 (patch) | |
| tree | 70c467bf21255737f3b28b10972478896599c740 /cfrontend/Clight.v | |
| parent | 3ec022950ec233a2af418aacd1755fce4d701724 (diff) | |
| download | compcert-kvx-842190a7a7c85b15f663fdf299a1f015a774f416.tar.gz compcert-kvx-842190a7a7c85b15f663fdf299a1f015a774f416.zip | |
Remove useless checks on type_of_global in dynamic semantics
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2411 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/Clight.v')
| -rw-r--r-- | cfrontend/Clight.v | 14 |
1 files changed, 0 insertions, 14 deletions
diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v index 59c056d6..f2ba2405 100644 --- a/cfrontend/Clight.v +++ b/cfrontend/Clight.v @@ -335,19 +335,6 @@ Section SEMANTICS. Variable ge: genv. -(** [type_of_global b] returns the type of the global variable or function - at address [b]. *) - -Definition type_of_global (b: block) : option type := - match Genv.find_var_info ge b with - | Some gv => Some gv.(gvar_info) - | None => - match Genv.find_funct_ptr ge b with - | Some fd => Some(type_of_fundef fd) - | None => None - end - end. - (** ** Evaluation of expressions *) Section EXPR. @@ -402,7 +389,6 @@ with eval_lvalue: expr -> block -> int -> Prop := | eval_Evar_global: forall id l ty, e!id = None -> Genv.find_symbol ge id = Some l -> - type_of_global l = Some ty -> eval_lvalue (Evar id ty) l Int.zero | eval_Ederef: forall a ty l ofs, eval_expr a (Vptr l ofs) -> |