Federico Poli comments

Results 208 comments of


                                            Federico Poli

Wrong optimization of signed integer divisions

(I also wonder why those optimizations are not always used by Viper. Are they slower on average than feeding the unoptimized expressions to Z3? Has anyone ever tried measuring this?)

Trigger inference infers invalid triggers

Why is a `forall` with a single quantified variable rewritten to a forall with *two* quantified variables? Does Silicon do it frequently?

Trigger inference infers invalid triggers

I see, thanks! Just to be sure, the extra quantified variable can only be introduced when the user does *not* specify the triggers, right? Otherwise it'd be really hard to...

Error for missing model lifetime specifier recommends invalid syntax, has unclear fix

Hi @csgordon! Thank you for reporting this. The high-level reason of the weird lifetime error is that specifications are implemented as a macro that desugars attributes into Rust code (we...

ghost seq not implemented

@Aurel300

JNI_GetCreatedJavaVMs

Could you add a complete minimal example? `JNI_GetCreatedJavaVMs` works fine when used in [duchess](https://github.com/duchess-rs/duchess) with OpenJDK 20.0.1.

Cargo time machine (generate lock files based on old registry state)

Is the publication date of a package stored somewhere? With that, it would be possible to filter package versions from `ret` just before the `sort_unstable_by`:

Cargo time machine (generate lock files based on old registry state)

Alternatively, to use a specific git hash one could modify this `git fetch`: