Christoph M. Wintersteiger
|
7e705a2d32
|
Bug fixes for underspecified FP operations.
|
2016-10-15 18:35:39 +02:00 |
|
Christoph M. Wintersteiger
|
bc257211d6
|
Whitespace
|
2016-10-15 18:35:39 +02:00 |
|
Christoph M. Wintersteiger
|
617e941015
|
fp2bv refactoring
|
2016-05-23 18:10:17 +01:00 |
|
Christoph M. Wintersteiger
|
b6d90a64da
|
fpa rewriter tidy up
|
2016-05-21 18:07:37 +01:00 |
|
Christoph M. Wintersteiger
|
1cc8146aba
|
Bugfixes for FP UFs and arrays.
|
2016-05-20 19:53:57 +01:00 |
|
Christoph M. Wintersteiger
|
df81ab72f5
|
Bug and performance fixes for FP UFs.
|
2016-05-17 16:35:45 +01:00 |
|
Christoph M. Wintersteiger
|
6b2d84b2be
|
Fixed model evaluation/simplification for to_ieee_bv.
|
2016-03-16 17:46:52 +00:00 |
|
Christoph M. Wintersteiger
|
7ec70c1686
|
bug fixes for unspecified FP results
|
2016-03-16 16:57:20 +00:00 |
|
Christoph M. Wintersteiger
|
db6b9faabc
|
Bugfix for FPA rewriter.
|
2016-03-16 16:35:45 +00:00 |
|
Christoph M. Wintersteiger
|
cdc8e1303a
|
Bugfix for fp.to_*_unspecified.
Fixes #507
|
2016-03-16 16:16:29 +00:00 |
|
Christoph M. Wintersteiger
|
99d7a47f82
|
Bugfixes for unspecified results from fp.to_* (models are still incomplete).
Relates to #507
|
2016-03-15 21:45:54 +00:00 |
|
Christoph M. Wintersteiger
|
371573cbff
|
More implementation of fp.to_ieee_bv for unspecified input/output
Relates to #507
|
2016-03-15 15:11:37 +00:00 |
|
Christoph M. Wintersteiger
|
176782d62b
|
Bugfix for fp.to_ieee_bv for unspecified input/output.
|
2016-03-15 14:38:11 +00:00 |
|
Christoph M. Wintersteiger
|
b5279d1da8
|
Bugfix for fp.to_ieee_bv.
Fixes #507.
|
2016-03-11 12:35:41 +00:00 |
|
Christoph M. Wintersteiger
|
de3cb7e5dc
|
More FPA exponent/siginficand order consistency
|
2016-01-05 18:05:21 +00:00 |
|
Christoph M. Wintersteiger
|
05b29df2cb
|
Bugfix for FP API
|
2016-01-04 21:01:01 +00:00 |
|
Christoph M. Wintersteiger
|
677ff221f8
|
Internal consistency: FP exponents are always passed before significands.
|
2016-01-04 18:57:15 +00:00 |
|
Christoph M. Wintersteiger
|
077e801590
|
Assertion fix. Relates to #383.
|
2015-12-23 13:41:52 +01:00 |
|
Christoph M. Wintersteiger
|
92152b16ca
|
Bugfixes for model verification of unspecified values of fp.min/fp.max
|
2015-11-02 19:25:44 +00:00 |
|
Christoph M. Wintersteiger
|
8fffa9f188
|
Removed trailing whitespace.
|
2015-10-30 12:20:41 +00:00 |
|
Christoph M. Wintersteiger
|
9b5abcd55a
|
Improved support for FPA unspecified min/max values, model validation, and proof generation.
|
2015-10-25 13:10:40 +00:00 |
|
Christoph M. Wintersteiger
|
ca496f20cb
|
Partial refactoring of fpa2bv conversion to support proofs.
|
2015-10-25 13:10:40 +00:00 |
|
Christoph M. Wintersteiger
|
099775947e
|
Partial fix for fp,min/fp.max models
|
2015-10-25 13:10:40 +00:00 |
|
Christoph M. Wintersteiger
|
de39173f6f
|
Corrected unspecified behavior of fp.min/fp.max corner cases in fpa2bv_converter and in theory_fpa.
Fixes #68
|
2015-10-07 20:44:08 +01:00 |
|
Christoph M. Wintersteiger
|
8a026c355f
|
Corrected unspecified behavior of corner cases in fp.min/fp.max.
Partially addresses #68.
|
2015-10-07 20:39:36 +01:00 |
|
Christoph M. Wintersteiger
|
79d69cd5f0
|
Added FP to_ieee_bv to fpa_rewriter to enable model evaluation.
|
2015-09-16 12:57:05 +01:00 |
|
Christoph M. Wintersteiger
|
a1073206f9
|
Bugfix for FP rewriter.
|
2015-09-15 16:23:24 +01:00 |
|
Christoph M. Wintersteiger
|
25f75b60fe
|
Bugfix for fp.mul and fp.fma for small numbers of e/s bits.
Fixes #215.
|
2015-09-10 11:37:06 +01:00 |
|
Christoph M. Wintersteiger
|
9428acd578
|
Bugfix for FPA rewriter.
|
2015-05-29 13:58:33 +01:00 |
|
Christoph M. Wintersteiger
|
7619d609f9
|
FPA min/max -+0.0 special cases changed to +0.0 instead of second argument.
Fixes #68
|
2015-05-28 12:20:48 +01:00 |
|
Christoph M. Wintersteiger
|
eee076b9f8
|
Bugfixes for fp.min, fp.max.
Fixes the fix for #68
|
2015-05-21 18:16:02 +01:00 |
|
Christoph M. Wintersteiger
|
73eb7cbf5c
|
Bugfix for mpf roundToIntegral.
Partially fixes #69
|
2015-05-05 23:53:33 +01:00 |
|
Christoph M. Wintersteiger
|
57af3a4c6e
|
FPA min/max refactoring and fixes.
Fixes #68
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-05-04 13:47:04 +01:00 |
|
Christoph M. Wintersteiger
|
359c7e4da9
|
Removed unnecessary variables and added initialization to others to silence warnings.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-02-07 14:47:26 +00:00 |
|
Christoph M. Wintersteiger
|
941d1063dd
|
FPA rewriter and MPF bugfixes
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-02-06 18:48:14 +00:00 |
|
Christoph M. Wintersteiger
|
5e60bcd920
|
FPA: fixes for the fpa_rewriter to enable model extraction and validation.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-02-06 16:53:31 +00:00 |
|
Christoph M. Wintersteiger
|
95300e801d
|
fixed build errors and warnings
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-21 18:24:36 +00:00 |
|
Christoph M. Wintersteiger
|
5344d6f3c0
|
various bugfixes and extensions for FPA
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-15 19:25:49 +00:00 |
|
Christoph M. Wintersteiger
|
c0bc2518b0
|
Renaming for consistency mk_value -> mk_numeral
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-08 14:22:44 +00:00 |
|
Christoph M. Wintersteiger
|
c0a027fc80
|
FPA: Elminated nzero/pzero AST kinds
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-08 14:07:47 +00:00 |
|
Christoph M. Wintersteiger
|
dd17f3c7d6
|
Renaming floats, float, Floats, Float -> FPA, fpa
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-08 13:18:56 +00:00 |
|