diff options
| author | Alasdair Armstrong | 2019-04-09 18:30:37 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-04-09 20:35:50 +0100 |
| commit | 271a8aba3041e4f712f3331fd1610cdf31fbb4c9 (patch) | |
| tree | 1644d1916b76e8e75606a63cf3d92b71358b26de /src/value2.lem | |
| parent | 97cc026337ea5cfc33586b6725c312c1a507f922 (diff) | |
SMT: Refactor Jib values to make inlining work
Had to change the hundreds and hundreds of places such values were
used. However this now lets us automatically prove cheri-concentrate
properties. Such as showing
function prop_cap_round_trip(cap: bits(128)) -> bool = {
let cap_rt = capToBits(capBitsToCapability(true, cap));
cap == cap_rt
}
is always true.
Diffstat (limited to 'src/value2.lem')
| -rw-r--r-- | src/value2.lem | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/value2.lem b/src/value2.lem index caf355b7..0e65e91f 100644 --- a/src/value2.lem +++ b/src/value2.lem @@ -53,10 +53,10 @@ open import Pervasives open import Sail2_values type vl = - | V_bits of list bitU - | V_bit of bitU - | V_bool of bool - | V_unit - | V_int of integer - | V_string of string - | V_null (* Used for unitialized values and null pointers in C compilation *) + | VL_bits of list bitU * bool + | VL_bit of bitU + | VL_bool of bool + | VL_unit + | VL_int of integer + | VL_string of string + | VL_null (* Used for unitialized values and null pointers in C compilation *) |