Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://github.com/model-checking/kani/issues/316 below:

Global ASM is not supported · Issue #316 · model-checking/kani · GitHub

Following LLVM, Rust allows global ASM in a module. This means that crates can have arbitrary code that we cannot analyze.

We know of crates that use this feature

We could fail any crate that uses this feature, but this would block any use of those crates, even if they did not use any of the risky features. Even worse, this would block all consumers of such crates, from even compiling, again even if they do not use any of the dangerous features.

Unlike for inline ASM in a function, where we can insert assert(0) as a mechanism to guarantee soundness, there is no obvious way to only fail code paths that use the injected ASM.

• Raise a warning if global asm appears
• Incorporate that warning into viewer

• Support ASM in CBMC

https://rust-lang.github.io/rfcs/1548-global-asm.html

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4