Kani's assert macro implementation bypasses some compile-time checks #803
Description
With PR #797, Kani's implementation of the assert macro's second form that accepts a custom message bypasses several compile-time checks.
For example, while rustc errors out on the following program:
fn main() {
assert!(1 + 1 == 3, "Bad arithmetic: {}", foo);
}output:
error[E0425]: cannot find value `foo` in this scope
--> no_display.rs:2:47
|
2 | assert!(1 + 1 == 3, "Bad arithmetic: {}", foo);
| ^^^ not found in this scope
kani does not complain about the non-existence of the variable foo:
CBMC version 5.48.0 (cbmc-5.48.0) 64-bit x86_64 linux
Reading GOTO program from file no_display.goto
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 16 object bits, 48 offset bits (user-specified)
Starting Bounded Model Checking
Runtime Symex: 0.00102581s
size of program expression: 75 steps
simple slicing removed 3 assignments
Generated 3 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 7.25e-06s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.000213004s
Running propositional reduction
Post-processing
Runtime Post-process: 2.594e-05s
Solving with MiniSAT 2.2.1 with simplifier
100 variables, 33 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 9.1981e-05s
Runtime decision procedure: 0.000343287s
** Results:
[assertion.1] Code generation sanity check: Correct CBMC vtable size for StructTag("tag-_4317141983261250885") (MIR type Closure(DefId(2:9147 ~ std[2f3c]::rt::lang_start::{closure#0}), [(), i8, extern "rust-call" fn(()) -> i32, (fn(),)])). Please report failures:
https://github.com/model-checking/kani/issues/new?template=bug_report.md: SUCCESS
[pointer_primitives.1] dead object in OBJECT_SIZE(&temp_0): SUCCESS
/home/ubuntu/examples/no_display.rs function main
[main.assertion.1] line 2 assertion: "Bad arithmetic: {}", foo: FAILURE
** 1 of 3 failed (2 iterations)
VERIFICATION FAILED
Other checks that would be skipped by kani's assert macro are that the argument must implement the Display trait.