diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-20 12:25:02 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-20 12:25:02 +0100 |
| commit | 3718f2f520fc9a4dec2e9c1ac6eaf71f36f4f8a1 (patch) | |
| tree | fe4fafcb0d72473e7159662bacee7fa7fc13afaa /mppa_k1c/SelectOp.vp | |
| parent | e80af0edafe49ec2576b7fa3a24d4596083698b6 (diff) | |
| download | compcert-kvx-3718f2f520fc9a4dec2e9c1ac6eaf71f36f4f8a1.tar.gz compcert-kvx-3718f2f520fc9a4dec2e9c1ac6eaf71f36f4f8a1.zip | |
begin float division
Diffstat (limited to 'mppa_k1c/SelectOp.vp')
| -rw-r--r-- | mppa_k1c/SelectOp.vp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index b2ce1fef..80eb641c 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -535,4 +535,8 @@ Nondetfunction builtin_arg (e: expr) := | _ => BA e end. +(* float division *) + +Definition divfbase (e1: expr) (e2: expr) := + Eop Odivf (e1 ::: e2 ::: Enil). End SELECT. |