diff options
| author |  Checkmate50 <dgeisler50@gmail.com> | 2016-03-17 13:01:10 -0600 |
|---|---|---|
| committer | Checkmate50 <dgeisler50@gmail.com> | 2016-03-17 13:01:10 -0600 |
| commit | 51b7e8146f413b83a412572fcc9e3a1a8b302b79 (patch) | |
| tree | 9ef4e6b21037425827b72cff1095398dc299f569 /float_test.bpl | |
| parent | 6ac996211d6f42f0c7f61ea108388d6bb798ecf8 (diff) | |
modified floating point syntax and modified floating point constants to use bitvector values
Diffstat (limited to 'float_test.bpl')
| -rw-r--r-- | float_test.bpl | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/float_test.bpl b/float_test.bpl index fbf8e4e3..e893e098 100644 --- a/float_test.bpl +++ b/float_test.bpl @@ -1,13 +1,13 @@ //Translation from addsub_double_exact.c //Should Verify procedure main() returns () { - var x : float(11 53); - var y : float(11 53); - var z : float(11 53); - var r : float(11 53); - x := fp(10000000 11 53); - y := x + fp(1 11 53); - z := x - fp(1 11 53); + var x : float<11, 53>; + var y : float<11, 53>; + var z : float<11, 53>; + var r : float<11, 53>; + x := fp<11, 53> (10000000bv64); + y := x + fp<11, 53>(1bv64); + z := x - fp<11, 53>(1bv64); r := y - z; - assert r == fp(2 11 53); + assert r == fp<11, 53> (2bv64); }
\ No newline at end of file |