From f9df0e2ea8e0b03352f5bbba54f091f2ee25b161 Mon Sep 17 00:00:00 2001 From: Dietrich Date: Tue, 5 May 2015 04:50:47 -0600 Subject: added decimal reading functionality to the float type --- float_test6.bpl | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 float_test6.bpl (limited to 'float_test6.bpl') diff --git a/float_test6.bpl b/float_test6.bpl new file mode 100644 index 00000000..532798d6 --- /dev/null +++ b/float_test6.bpl @@ -0,0 +1,5 @@ + procedure F() returns () { + var x : float; + x := fp (1.5); + assert x == fp (1 0 23 8); +} \ No newline at end of file -- cgit v1.2.3