From be0b1872bf2ad36df9b0c7a0ffa63b9e77fa769b Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 18 Feb 2020 16:57:17 +0100 Subject: Refine the type of function results in AST.signature Before it was "option typ". Now it is a proper inductive type that can also express small integer types (8/16-bit unsigned/signed integers). One benefit is that external functions get more precise types that control better their return values. As a consequence, the CompCert C type preservation property now holds unconditionally, without extra typing hypotheses on external functions. --- powerpc/Asmexpand.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'powerpc/Asmexpand.ml') diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 704b0aba..ce88778c 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -852,7 +852,7 @@ let expand_instruction instr = if variadic then begin emit (Pmflr GPR0); emit (Pbl(intern_string "__compcert_va_saveregs", - {sig_args = []; sig_res = None; sig_cc = cc_default})); + {sig_args = []; sig_res = Tvoid; sig_cc = cc_default})); emit (Pmtlr GPR0) end; current_function_stacksize := sz; -- cgit