diff options
author | Yann Herklotz <git@yannherklotz.com> | 2023-04-27 16:32:13 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2023-04-27 16:32:13 +0100 |
commit | ab617cf8e6e60e8de3eb8de220f71dd05c18209f (patch) | |
tree | 1e2da8e3edbf48d02f536a21f2cafb6167045c51 /verilog/ConstpropOp.v | |
parent | f0867a37e28a1f3670362e7935f9ef30988ddb92 (diff) | |
download | compcert-master.tar.gz compcert-master.zip |
Diffstat (limited to 'verilog/ConstpropOp.v')
-rw-r--r-- | verilog/ConstpropOp.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/verilog/ConstpropOp.v b/verilog/ConstpropOp.v index 9b9c9711..c525c9c2 100644 --- a/verilog/ConstpropOp.v +++ b/verilog/ConstpropOp.v @@ -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)) |