diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-03-06 09:53:46 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-03-06 09:53:46 +0100 |
| commit | fe55fe4397636e331fdbe7c2581b00e35bbec734 (patch) | |
| tree | 981e2926d15ba64e38789215968768c167539bc0 /common/Sections.ml | |
| parent | 9dedd1fd62a174be0723b66521e469a4d46c6a18 (diff) | |
| download | compcert-fe55fe4397636e331fdbe7c2581b00e35bbec734.tar.gz compcert-fe55fe4397636e331fdbe7c2581b00e35bbec734.zip | |
AST: extend and adapt to the new linking framework.
- Add "prog_defmap" to compute the ptree name -> global definition corresponding to a program.
- Move "match_program" to Linking.
- Clean up and simplify a bit the transf_* functions for program transformations.
- Add a new kind of external functions, "EF_runtime". Unlike "EF_external", an "EF_runtime" external function cannot be implemented by an internal function definition in another compilation unit. (Linking returns an error in this case.) We will use "EF_runtime" for the "_i64_*" helper functions, which must not be defined by the program, and instead must remain external.
Diffstat (limited to 'common/Sections.ml')
0 files changed, 0 insertions, 0 deletions