diff options
| author | Alasdair Armstrong | 2019-05-08 18:14:51 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-05-08 18:23:08 +0100 |
| commit | ff4b53fba32ebdb6cb587fac0bc5f4a523304a55 (patch) | |
| tree | f6f1ce39709836e6ad3d988e96ab69327f897f8d /src/value2.lem | |
| parent | 611748f32de5269eb3d56bb3098cf07c9a89a0ba (diff) | |
SMT: Add reals and strings to SMT backend
Jib_compile now has an option that lets it generate real value
literals (VL_real), which we don't want for backends (i.e. C), which
don't support them. Reals are encoded as actual reals in SMT, as there
isn't really any nice way to encode them as bitvectors. Currently we
just have the pure real functions, functions between integers and
reals (i.e. floor, to_real, etc) are not supported for now.
Strings are likewise encoded as SMTLIB strings, for similar reasons.
Jib_smt has ctx.use_real and ctx.use_string which are set when we
generate anything real or string related, so we can keep the logic as
Arrays+Bitvectors for most Sail that doesn't require either.
Diffstat (limited to 'src/value2.lem')
| -rw-r--r-- | src/value2.lem | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/value2.lem b/src/value2.lem index 0e65e91f..0afaa2d1 100644 --- a/src/value2.lem +++ b/src/value2.lem @@ -59,4 +59,5 @@ type vl = | VL_unit | VL_int of integer | VL_string of string + | VL_real of string | VL_null (* Used for unitialized values and null pointers in C compilation *) |