diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-16 13:51:33 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-16 13:51:33 +0100 |
| commit | 1e08d4adb241e076a96f9525fdb8359cf8845527 (patch) | |
| tree | 0ef2e4239e970c9904a94a5675ce0f73dc0f1fb4 /ia32 | |
| parent | 9d95c2ce76bffe4be06697ac99936c7703c18a07 (diff) | |
| download | compcert-1e08d4adb241e076a96f9525fdb8359cf8845527.tar.gz compcert-1e08d4adb241e076a96f9525fdb8359cf8845527.zip | |
Added interface for the Asmexpansion.
Hide the reference used internally behind the interface and added
some functions to access the needed values.
Bug 18394
Diffstat (limited to 'ia32')
| -rw-r--r-- | ia32/Asmexpand.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ia32/Asmexpand.ml b/ia32/Asmexpand.ml index 3a3548f9..4f2bb937 100644 --- a/ia32/Asmexpand.ml +++ b/ia32/Asmexpand.ml @@ -200,12 +200,12 @@ let expand_builtin_vstore chunk args = (* Handling of varargs *) let expand_builtin_va_start r = - if not !current_function.fn_sig.sig_cc.cc_vararg then + if not (is_current_function_variadic ()) then invalid_arg "Fatal error: va_start used in non-vararg function"; let ofs = coqint_of_camlint Int32.(add (add !PrintAsmaux.current_function_stacksize 4l) (mul 4l (Z.to_int32 (Conventions1.size_arguments - !current_function.fn_sig)))) in + (get_current_function_sig ()))))) in emit (Pmov_mr (linear_addr r _0, ESP)); emit (Padd_mi (linear_addr r _0, ofs)) |