From 88c46de03f37dd9edb78e68734a9976ab2ccc056 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 22 Mar 2019 10:28:54 +0100 Subject: seems like powerpc runs but the result segfaults --- powerpc/SelectOp.vp | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'powerpc/SelectOp.vp') diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index d2ca408a..478ce251 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -43,6 +43,7 @@ Require Import Integers. Require Import Floats. Require Import Op. Require Import CminorSel. +Require Import OpHelpers. Local Open Scope cminorsel_scope. @@ -552,3 +553,10 @@ Nondetfunction builtin_arg (e: expr) := | Eop Oadd (e1:::e2:::Enil) => BA_addptr (BA e1) (BA e2) | _ => BA e end. + +(* floats *) +Definition divf_base (e1: expr) (e2: expr) := + Eop Odivf (e1 ::: e2 ::: Enil). + +Definition divfs_base (e1: expr) (e2: expr) := + Eop Odivfs (e1 ::: e2 ::: Enil). -- cgit