diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-02-06 13:19:59 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-02-06 13:19:59 +0100 |
| commit | 47a77e398dd3815a20622934cdeeb4f0e076f42b (patch) | |
| tree | 6e531b417c17aeac2508225651afc7aa8d989c6a /backend/PrintAsmaux.ml | |
| parent | 20ee821830467d091984ccf9ed646de7975866a7 (diff) | |
| download | compcert-47a77e398dd3815a20622934cdeeb4f0e076f42b.tar.gz compcert-47a77e398dd3815a20622934cdeeb4f0e076f42b.zip | |
Changed the ia32 backend to the new Printer.
Diffstat (limited to 'backend/PrintAsmaux.ml')
| -rw-r--r-- | backend/PrintAsmaux.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 381ef5df..8812d320 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -69,6 +69,11 @@ let float64_literals : (int * int64) list ref = ref [] let float32_literals : (int * int32) list ref = ref [] let jumptables : (int * label list) list ref = ref [] +let reset_constants () = + float64_literals := []; + float32_literals := []; + jumptables := [] + (* Variables used for the handling of varargs *) let current_function_stacksize = ref 0l |