diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-10-05 15:52:58 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-10-05 15:52:58 +0200 |
| commit | 26ddb90280b45e92d90eead89edb237f2922824a (patch) | |
| tree | ff18b31abdbb97133f9708ca085467f25758e507 /x86/ConstpropOp.vp | |
| parent | e9c738e3bd156f68905968e25c70ec796d3119c4 (diff) | |
| download | compcert-26ddb90280b45e92d90eead89edb237f2922824a.tar.gz compcert-26ddb90280b45e92d90eead89edb237f2922824a.zip | |
Support Cygwin 64 bits
- Add support for the Win64 ABI to the x86_64 port
- Update vararg support to handle Win64 conventions
- Configure support for x86_64-cygwin64
Diffstat (limited to 'x86/ConstpropOp.vp')
| -rw-r--r-- | x86/ConstpropOp.vp | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/x86/ConstpropOp.vp b/x86/ConstpropOp.vp index ada8d54a..dd4b839a 100644 --- a/x86/ConstpropOp.vp +++ b/x86/ConstpropOp.vp @@ -17,11 +17,10 @@ Require Import Coqlib Compopts. Require Import AST Integers Floats. Require Import Op Registers. Require Import ValueDomain ValueAOp. +Require SelectOp. (** * Converting known values to constants *) -Parameter symbol_is_external: ident -> bool. (**r See [SelectOp] *) - Definition Olea_ptr (a: addressing) := if Archi.ptr64 then Oleal a else Olea a. Definition const_for_result (a: aval) : option operation := @@ -31,7 +30,7 @@ Definition const_for_result (a: aval) : option operation := | F n => if Compopts.generate_float_constants tt then Some(Ofloatconst n) else None | FS n => if Compopts.generate_float_constants tt then Some(Osingleconst n) else None | Ptr(Gl id ofs) => - if symbol_is_external id then + if SelectOp.symbol_is_external id then if Ptrofs.eq ofs Ptrofs.zero then Some (Oindirectsymbol id) else None else Some (Olea_ptr (Aglobal id ofs)) |