Skip to content

PRUSTI_CHECK_PANICS=false causes a compiler panic for a called pure arithmetic function #1554

Description

@lynae99

Prusti 0.2.2 reports a normal verification error with its default configuration,
but panics when panic checking is disabled.

Reproducer

Save the following as PureCallCheckPanics.rs:

use prusti_contracts::*;

#[pure]
fn negate(value: i32) -> i32 {
    -value
}

fn main() {
    negate(0);
}

Reproduction commands

PRUSTI=/path/to/prusti-rustc
PRUSTI_HOME=/path/to/prusti
DEFAULT_OUT=$(mktemp -d)
TARGET_OUT=$(mktemp -d)

RUSTUP_TOOLCHAIN=nightly-2023-09-15 \
  "$PRUSTI" PureCallCheckPanics.rs --crate-name pure_call_check_panics \
  --edition=2021 -L "$PRUSTI_HOME" -L "$PRUSTI_HOME/deps" \
  --out-dir "$DEFAULT_OUT"

PRUSTI_CHECK_PANICS=false RUSTUP_TOOLCHAIN=nightly-2023-09-15 \
  "$PRUSTI" PureCallCheckPanics.rs --crate-name pure_call_check_panics \
  --edition=2021 -L "$PRUSTI_HOME" -L "$PRUSTI_HOME/deps" \
  --out-dir "$TARGET_OUT"

Actual result

The default configuration reports a normal verification error:

assertion might fail with "attempt to negate with overflow"

With PRUSTI_CHECK_PANICS=false, the compiler exits with status 101:

thread 'rustc' panicked at prusti/src/verifier.rs:76:17
assertion failed: env.diagnostic.has_errors() || ...

The result was reproduced in three independent runs.

Expected result

Disabling panic checking should not cause the compiler to panic. Prusti should
finish normally or report a regular diagnostic.

Version

Prusti 0.2.2, commit 0d4a8d4
rustc 1.74.0-nightly

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions