diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-08-23 12:32:50 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-08-23 12:32:50 +0200 |
| commit | b55d63d2917b384fa0f5da76d7d16036ad263847 (patch) | |
| tree | 5b6e45bcd99437e5d2866f0a2603674c80ecf5e0 /cfrontend/PrintCsyntax.ml | |
| parent | c3c0aba2ed285bc33208cfc67667f47d6d1b0762 (diff) | |
| download | compcert-kvx-b55d63d2917b384fa0f5da76d7d16036ad263847.tar.gz compcert-kvx-b55d63d2917b384fa0f5da76d7d16036ad263847.zip | |
Print prototypes for malloc and free.
The declarations of malloc and free should also be printed for
CompCert C.
Bug 19616.
Diffstat (limited to 'cfrontend/PrintCsyntax.ml')
| -rw-r--r-- | cfrontend/PrintCsyntax.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 7b2fc108..e3e259f7 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -426,7 +426,7 @@ let print_function p id f = let print_fundef p id fd = match fd with - | Ctypes.External((EF_external _ | EF_runtime _), args, res, cconv) -> + | Ctypes.External((EF_external _ | EF_runtime _| EF_malloc | EF_free), args, res, cconv) -> fprintf p "extern %s;@ @ " (name_cdecl (extern_atom id) (Tfunction(args, res, cconv))) | Ctypes.External(_, _, _, _) -> |