diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2014-11-26 14:46:07 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2014-11-26 14:46:07 +0100 |
| commit | b279716c76c387c6c5eec96388c0c35629858b4c (patch) | |
| tree | a71079afbe6eebc1162391546aeaebe56dbd56d2 /driver/Interp.ml | |
| parent | 1ccc058794381d7d7c2ff704786009019489001d (diff) | |
| download | compcert-kvx-b279716c76c387c6c5eec96388c0c35629858b4c.tar.gz compcert-kvx-b279716c76c387c6c5eec96388c0c35629858b4c.zip | |
Introduce symbol environments (type Senv.t) as a restricted view on global environments (type Genv.t). Use symbol environments instead of global environments for external functions (module Events).
Diffstat (limited to 'driver/Interp.ml')
| -rw-r--r-- | driver/Interp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/driver/Interp.ml b/driver/Interp.ml index 9bb9d237..8dd32ff4 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -389,7 +389,7 @@ let convert_external_arg ge v t = | Vsingle f, AST.Tsingle -> Some (EVsingle f) | Vlong n, AST.Tlong -> Some (EVlong n) | Vptr(b, ofs), AST.Tint -> - Genv.invert_symbol ge b >>= fun id -> Some (EVptr_global(id, ofs)) + Senv.invert_symbol ge b >>= fun id -> Some (EVptr_global(id, ofs)) | _, _ -> None let rec convert_external_args ge vl tl = |