Use `-native-compiler no` to make sure we do not rely on (bugs) in `native_compute`. (!419) · Merge requests · Iris / stdpp

Robbert Krebbers requested to merge robbert/no_native_compiler into master Oct 20, 2022

In std++ and Iris we do not use native_compute, so relying on it needlessly increases the trusted code base. Since recently an unsoundness bug in naive_compute was discovered (which was also fixed immediately), I wonder if it wouldn't make sense to just disable native_compute altogether in std++ and Iris.

Use `-native-compiler no` to make sure we do not rely on (bugs) in `native_compute`.

Merge request reports