Skip to content

Commit d63559b

Browse files
committed
cite cerberus
1 parent d871de6 commit d63559b

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

wip/value-domain.md

+2
Original file line numberDiff line numberDiff line change
@@ -112,6 +112,8 @@ trait TypedMemory: Memory {
112112
```
113113

114114
Here, `Type` is some representation of the Rust type system (akin to [`Ty`](https://doc.rust-lang.org/nightly/nightly-rustc/rustc/ty/type.Ty.html) in the compiler).
115+
This interface is inspired by [Cerberus](https://www.cl.cam.ac.uk/~pes20/cerberus/).
116+
115117
We can implement `TypedMemory` for any `Memory` as follows:
116118
* For `typed_write`, pick any representation of `val` for `ty`, and call `Memory::write`. If no representation exists, we have UB.
117119
* For `typed_read`, read `ty.size()` many bytes from memory, and then determine which value this list of bytes represents. If it does not represent any value, we have UB.

0 commit comments

Comments
 (0)