Skip to content

Tags: runtimeverification/mir-semantics

Tags

v0.4.17

Set Version: 0.4.17

release-0.4.17

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
Update dependency: deps/k_release (#633)

Co-authored-by: devops <devops@runtimeverification.com>

v0.4.16

Set Version: 0.4.16

release-0.4.16

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
Update dependency: deps/k_release (#618)

Co-authored-by: devops <devops@runtimeverification.com>

v0.4.15

Set Version: 0.4.15

release-0.4.15

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
529 pointer cast corrections (#632)

This became a rather large and pervasive change, adding metadata to the
`Reference` value (not just to pointers).

* `Reference`s now carry metadata which gives the size of the pointee in
case of an array or slice.
* The size of slices (and arrays) is important when dereferencing the
references (or pointers, which is much less common).
* Statically-determined sizes are also carried around to avoid looking
up the size from the `TypeInfo` each time
* when dereferencing arrays, only the expected size is copied. If the
expected size is larger than the actual array, the execution gets stuck.
A new test has been added which is expected to fail on undefined
behaviour (`rustc`-compiled code will instead happily copy random data
into the array, as can be observed by activating the `println`s in the
new test).

v0.4.14

Set Version: 0.4.14

release-0.4.14

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
624 include and offset spans in linked smir (#630)

All spans are now included in the linker output, with the respective
crate offset applied to each occurrence.

FIxes #624

v0.4.13

Set Version: 0.4.13

release-0.4.13

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
Assign Ty IDs to all function items (#628)

The function table in SMIR JSON currently only contains functions which
are called from other functions within the crate. For library crates,
there can be many functions in the crate that aren't iun the table, and
for binary crates, `main` is usually missing.

Previously, only `main`'s symbol was added to the table.

This change assigns negative `Ty` IDs to every item which is not present
in the function table.

As a result, then dead-item pruning code now works on all functions
without crash.

The previous hack to expose start symbol functions was removed from the
crate tests.

Fixes #619