Extra verifier argument `numberOfErrorsToReport` gets ignored

[Patrick-6]

Adding the option extra_verifier_args = ["--numberOfErrorsToReport=0"] in the Prusti.toml file doesn't seem to do anything, e.g. the following code behaves the same with and without this option (running without overflow checks):

use prusti_contracts::*;

fn test(x: u64) {
    let y = 3 * x;
    assert!(y == 10*x); // Prusti shows error here
    assert!(y == 0); // correct if previous assertion holds
    assert!(false); // no error shown here
}

[fpoli]

It seems that we lost this feature in a refactoring.

In prusti-viper/src/verifier.rs we have

verifier_args.extend(config::extra_verifier_args());

but the new_viper_verifier in prusti-server/src/process_verification.rs doesn't use config::extra_verifier_args.

[Aurel300]

It seems the extra args do get used. In the list of arguments passed to Silicon, the "extra" ones, if any, are at the beginning.

However, neither PRUSTI_EXTRA_VERIFIER_ARGS="--numberOfErrorsToReport 0" nor PRUSTI_EXTRA_VERIFIER_ARGS="--numberOfErrorsToReport=0" has the expected effect. Investigating further, running Silicon manually on the produced Viper file works as expected: there are two assertion failures, corresponding to the first and third assertion in the original program.

Maybe we aren't processing all the errors we get from Silicon?

[Aurel300]

Update: I think the problem is that the previous field of Silicon's VerificationResult is not used when we are converting from the Scala representation to the Rust representation. This code was not updated after viperproject/silicon#575 .

Update 2: this is not the case, Silicon is actually not reporting the errors it should when invoked through the JNI, but it does when the program is verified manually…