diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-11-12 13:42:22 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-11-12 13:42:22 +0000 |
commit | ce4951549999f403446415c135ad1403a16a15c3 (patch) | |
tree | cac9bbb2fea29fce331916b277c38ed8fe29e471 /backend/CMtypecheck.ml | |
parent | dcb9f48f51cec5e864565862a700c27df2a1a7e6 (diff) | |
download | compcert-ce4951549999f403446415c135ad1403a16a15c3.tar.gz compcert-ce4951549999f403446415c135ad1403a16a15c3.zip |
Globalenvs: allocate one-byte block with permissions Nonempty for each
function definition, so that comparisons between function pointers
are correctly defined.
AST, Globalenvs, and many other files:
represent programs as a list of (function or variable) definitions
instead of two lists, one for functions and the other for variables.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2067 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/CMtypecheck.ml')
-rw-r--r-- | backend/CMtypecheck.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml index 40707854..408e9ec1 100644 --- a/backend/CMtypecheck.ml +++ b/backend/CMtypecheck.ml @@ -349,10 +349,11 @@ let type_function id f = with Error s -> raise (Error (sprintf "In function %s:\n%s" (extern_atom id) s)) -let type_fundef (id, fd) = - match fd with - | Internal f -> type_function id f - | External ef -> () +let type_globdef (id, gd) = + match gd with + | Gfun(Internal f) -> type_function id f + | Gfun(External ef) -> () + | Gvar v -> () let type_program p = - List.iter type_fundef p.prog_funct; p + List.iter type_globdef p.prog_defs; p |