diff options
| author |  Dietrich <dgeisler50@gmail.com> | 2015-04-27 05:37:19 -0600 |
|---|---|---|
| committer | Dietrich <dgeisler50@gmail.com> | 2015-04-27 05:37:19 -0600 |
| commit | 2dae113e5996e050ca6595542de5030747245929 (patch) | |
| tree | 74454d160c292949bedd02ebc1477930a763d2e1 /float_test3.bpl | |
| parent | 94a9542de594ef210d1ede1ff05e12289dfb2dc7 (diff) | |
Began adding the float type to VC expression
Diffstat (limited to 'float_test3.bpl')
| -rw-r--r-- | float_test3.bpl | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/float_test3.bpl b/float_test3.bpl new file mode 100644 index 00000000..cd0ea59e --- /dev/null +++ b/float_test3.bpl @@ -0,0 +1,6 @@ + procedure F() returns () { + var x : float; + var y : float; + y := x - x; + assert y != x; +}
\ No newline at end of file |