1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
|
diff --git a/acl2.lisp b/acl2.lisp
index 036657d902..c2b7e4fad9 100644
--- a/acl2.lisp
+++ b/acl2.lisp
@@ -1963,11 +1963,7 @@ ACL2 from scratch.")
(* *my-most-positive-double-float*
*my-most-positive-double-float*)
(error () 0.0d0))
- 'double-float))
- #+sbcl
- (member :overflow
- (cadr (member :traps
- (sb-int:get-floating-point-modes)))))
+ 'double-float)))
(error "This Lisp is unsuitable for ACL2, because it failed ~%a check that ~
floating-point overflow causes an error."))
diff --git a/float-raw.lisp b/float-raw.lisp
index 1364491fdf..e6d0417971 100644
--- a/float-raw.lisp
+++ b/float-raw.lisp
@@ -46,13 +46,13 @@
; #.*infinity-double* and #.*negative-infinity-double*), so we do so, but we
; don't bother testing for Nan in LispWorks.
-; We return form unchanged in other than Allegro CL and LispWorks, because we
+; We return form unchanged in other than Allegro CL, LispWorks, and SBCL, because we
; already know that an error is signalled on overflow for other Lisps that host
; ACL2; see break-on-overflow-and-nan.
- #-(or allegro lispworks)
+ #-(or allegro lispworks sbcl)
(declare (ignore op))
- #-(or allegro lispworks)
+ #-(or allegro lispworks sbcl)
form
#+allegro
`(let ((result ,form))
@@ -65,6 +65,14 @@
(when (or (= result +1D++0) (= result -1D++0))
(error "Floating-point overflow for a call of ~s"
',op))
+ result)
+ #+sbcl
+ `(let ((result ,form))
+ (when (or (sb-ext:float-nan-p result)
+ (= result sb-ext:double-float-positive-infinity)
+ (= result sb-ext:double-float-negative-infinity))
+ (error "Floating-point exception for a call of ~s"
+ ',op))
result))
(defmacro defun-df-binary (name op)
|
