-
Notifications
You must be signed in to change notification settings - Fork 1
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Report block-level verification progress, port Prusti Assistant changes #57
base: rewrite-2023
Are you sure you want to change the base?
Report block-level verification progress, port Prusti Assistant changes #57
Commits on Jun 3, 2024
-
Fix domain function name garbling when running over prusti-server
Also comment out a line that crashes when not run from the same directory. This was problematic for working with Prusti Assistant.
Configuration menu - View commit details
-
Copy full SHA for 30beba6 - Browse repository at this point
Copy the full SHA 30beba6View commit details
Commits on Jun 8, 2024
-
Use new VerificationResult type
Ported change from PR viperproject#1334
Configuration menu - View commit details
-
Copy full SHA for ec4035e - Browse repository at this point
Copy the full SHA ec4035eView commit details
Commits on Jun 12, 2024
-
Port basic functionality for the new prusti-server work flow according to PR viperproject#1334 .
Configuration menu - View commit details
-
Copy full SHA for 4e6cc8a - Browse repository at this point
Copy the full SHA 4e6cc8aView commit details
Commits on Jun 13, 2024
-
Port
show_ide_info
andskip_verification
flagsQuerying signatures, spans of call contract collection and call finding does not work yet. PR: viperproject#1334
Configuration menu - View commit details
-
Copy full SHA for 0849d35 - Browse repository at this point
Copy the full SHA 0849d35View commit details -
Port
verify_only_defpath
andreport_viper_messages
flagsDefpath only verification does not work since test_entrypoint currently just puts the entire program into the request regardless of the verification tasks at hand. Update the flags in the documentation. PR: viperproject#1334
Configuration menu - View commit details
-
Copy full SHA for 5270e09 - Browse repository at this point
Copy the full SHA 5270e09View commit details
Commits on Jun 14, 2024
-
Add support for block level messaging and bump version
Requires the viperserver backend to support these messages too.
Configuration menu - View commit details
-
Copy full SHA for 39bfc55 - Browse repository at this point
Copy the full SHA 39bfc55View commit details
Commits on Jun 18, 2024
-
Attempt to fix the only defpath flag and fix not emitting fake error
Every body owner function that is not passed to be verified explicitly acts as though it were pure and trusted to skip the encoding of their bodies. Additionally, VERIFY_ONLY_DEFPATH now takes a vector of String instead of just a string.
Configuration menu - View commit details
-
Copy full SHA for 99c3b2c - Browse repository at this point
Copy the full SHA 99c3b2cView commit details -
Configuration menu - View commit details
-
Copy full SHA for e607cc0 - Browse repository at this point
Copy the full SHA e607cc0View commit details -
Configuration menu - View commit details
-
Copy full SHA for d472c60 - Browse repository at this point
Copy the full SHA d472c60View commit details
Commits on Jul 5, 2024
-
Improve contract span emission
`SpanOfCallContracts` now has a vector as it's `call_spans` field so only one object is created per function definition rather than one per call. `CallSpanFinder` now also collects local functions for call contract span emission. Functions that are never called need not be emitted.
Configuration menu - View commit details
-
Copy full SHA for 1443c24 - Browse repository at this point
Copy the full SHA 1443c24View commit details
Commits on Jul 12, 2024
-
Configuration menu - View commit details
-
Copy full SHA for cd45907 - Browse repository at this point
Copy the full SHA cd45907View commit details -
WIP: Restructure how verification requests are handled
A main goal here is that the vir-viper translation happens on the same thread that encodes the program in the local verification case. This should happen so the allocated arena, which is thread local, can be used. Additionally, the JVM reliant bits are a bit more hidden from the general procedure.
Configuration menu - View commit details
-
Copy full SHA for 9f58eef - Browse repository at this point
Copy the full SHA 9f58eefView commit details -
Configuration menu - View commit details
-
Copy full SHA for 1de40ff - Browse repository at this point
Copy the full SHA 1de40ffView commit details
Commits on Jul 15, 2024
-
Configuration menu - View commit details
-
Copy full SHA for aaecb18 - Browse repository at this point
Copy the full SHA aaecb18View commit details -
* Impure generics * Fixed bug due to type parameters not being encoded * Remove fractional perm * mk_bool doesn't need extra typarams
Configuration menu - View commit details
-
Copy full SHA for bc26f7b - Browse repository at this point
Copy the full SHA bc26f7bView commit details -
Support cycles in encoders (Aurel300#47)
* domain fields don't need a full encoding of their type yet * type alias for do_encode_full result * parameterise TaskEncoderDependencies by the owning encoder * remove some dependency unwraps * remove 'tcx lifetime, use 'vir * check for cycles when requesting dependencies or emitting output ref * add try operators for some emit output refs
Configuration menu - View commit details
-
Copy full SHA for ca5edb3 - Browse repository at this point
Copy the full SHA ca5edb3View commit details -
Configuration menu - View commit details
-
Copy full SHA for f8527cc - Browse repository at this point
Copy the full SHA f8527ccView commit details -
Configuration menu - View commit details
-
Copy full SHA for c513772 - Browse repository at this point
Copy the full SHA c513772View commit details -
Configuration menu - View commit details
-
Copy full SHA for e977267 - Browse repository at this point
Copy the full SHA e977267View commit details -
Configuration menu - View commit details
-
Copy full SHA for 0408617 - Browse repository at this point
Copy the full SHA 0408617View commit details -
Configuration menu - View commit details
-
Copy full SHA for 9a99465 - Browse repository at this point
Copy the full SHA 9a99465View commit details -
Configuration menu - View commit details
-
Copy full SHA for f3cf4ef - Browse repository at this point
Copy the full SHA f3cf4efView commit details -
Configuration menu - View commit details
-
Copy full SHA for f53725a - Browse repository at this point
Copy the full SHA f53725aView commit details -
Move backtranslation to where server messages are processed. Move `EncodingInfo` to encoder crate.
Configuration menu - View commit details
-
Copy full SHA for 846c447 - Browse repository at this point
Copy the full SHA 846c447View commit details
Commits on Jul 16, 2024
-
Configuration menu - View commit details
-
Copy full SHA for 14025ce - Browse repository at this point
Copy the full SHA 14025ceView commit details
Commits on Jul 18, 2024
-
Configuration menu - View commit details
-
Copy full SHA for 70b9855 - Browse repository at this point
Copy the full SHA 70b9855View commit details -
Fix viper program passing and factor out cache
- The viper program is now sent using a `GlobalRef`, so it actually compiles. - Cache usage no longer involves the `VerificationRequestProcessing` object. - The cache is now lazy, therefore only loads if the `ENABLE_CACHE` flag is set. - The `VerificationRequestProcessing` object is no longer constructed when all the requests are cache hits. The thread it holds is also not spawned as a result.
Configuration menu - View commit details
-
Copy full SHA for d195424 - Browse repository at this point
Copy the full SHA d195424View commit details
Commits on Jul 19, 2024
-
Configuration menu - View commit details
-
Copy full SHA for 0b30959 - Browse repository at this point
Copy the full SHA 0b30959View commit details -
Configuration menu - View commit details
-
Copy full SHA for 62d2a08 - Browse repository at this point
Copy the full SHA 62d2a08View commit details -
Configuration menu - View commit details
-
Copy full SHA for 9daeac6 - Browse repository at this point
Copy the full SHA 9daeac6View commit details -
Configuration menu - View commit details
-
Copy full SHA for c8a7399 - Browse repository at this point
Copy the full SHA c8a7399View commit details
Commits on Jul 20, 2024
-
Configuration menu - View commit details
-
Copy full SHA for 1b64b36 - Browse repository at this point
Copy the full SHA 1b64b36View commit details
Commits on Jul 22, 2024
-
Configuration menu - View commit details
-
Copy full SHA for a9e5021 - Browse repository at this point
Copy the full SHA a9e5021View commit details
Commits on Jul 25, 2024
-
Configuration menu - View commit details
-
Copy full SHA for b5722f3 - Browse repository at this point
Copy the full SHA b5722f3View commit details -
Configuration menu - View commit details
-
Copy full SHA for 2f8c64f - Browse repository at this point
Copy the full SHA 2f8c64fView commit details
Commits on Aug 1, 2024
-
Configuration menu - View commit details
-
Copy full SHA for f06740f - Browse repository at this point
Copy the full SHA f06740fView commit details -
Configuration menu - View commit details
-
Copy full SHA for 9b2bf78 - Browse repository at this point
Copy the full SHA 9b2bf78View commit details -
Configuration menu - View commit details
-
Copy full SHA for 47591c4 - Browse repository at this point
Copy the full SHA 47591c4View commit details
Commits on Aug 2, 2024
-
Configuration menu - View commit details
-
Copy full SHA for ee1747c - Browse repository at this point
Copy the full SHA ee1747cView commit details -
Configuration menu - View commit details
-
Copy full SHA for 174aef5 - Browse repository at this point
Copy the full SHA 174aef5View commit details -
Configuration menu - View commit details
-
Copy full SHA for b8c37ed - Browse repository at this point
Copy the full SHA b8c37edView commit details
Commits on Aug 8, 2024
-
Report results per method, backtranslate block labels
Also change backtranslation of viper identifiers. Note that caching may not work properly for now if the `GENERATE_VIPER_MESSAGES` flag is set. Fixing this is a WIP.
Configuration menu - View commit details
-
Copy full SHA for 1ebf520 - Browse repository at this point
Copy the full SHA 1ebf520View commit details
Commits on Aug 12, 2024
-
Merge branch 'assistant-features/request-processing-restructure' into…
… rewrite-2023-assistant-features Also clean up some imports.
Configuration menu - View commit details
-
Copy full SHA for 3e78249 - Browse repository at this point
Copy the full SHA 3e78249View commit details
Commits on Aug 15, 2024
-
The same error with different positions used to produce the same hashes (generated using java's `hashCode` function).
Configuration menu - View commit details
-
Copy full SHA for 81230b2 - Browse repository at this point
Copy the full SHA 81230b2View commit details -
Configuration menu - View commit details
-
Copy full SHA for 1063d9d - Browse repository at this point
Copy the full SHA 1063d9dView commit details -
Fix single files not being recognized as primary package
This previously made it impossible to selectively verify in single file programs. It still does not work when running through x.py.
Configuration menu - View commit details
-
Copy full SHA for 110e633 - Browse repository at this point
Copy the full SHA 110e633View commit details -
Configuration menu - View commit details
-
Copy full SHA for 35fc6a1 - Browse repository at this point
Copy the full SHA 35fc6a1View commit details
Commits on Aug 20, 2024
-
Configuration menu - View commit details
-
Copy full SHA for b708b7c - Browse repository at this point
Copy the full SHA b708b7cView commit details -
Configuration menu - View commit details
-
Copy full SHA for fd951ed - Browse repository at this point
Copy the full SHA fd951edView commit details
Commits on Aug 21, 2024
-
Configuration menu - View commit details
-
Copy full SHA for 19de80e - Browse repository at this point
Copy the full SHA 19de80eView commit details -
Configuration menu - View commit details
-
Copy full SHA for da102cc - Browse repository at this point
Copy the full SHA da102ccView commit details
Commits on Aug 29, 2024
-
Configuration menu - View commit details
-
Copy full SHA for e5a323b - Browse repository at this point
Copy the full SHA e5a323bView commit details
Commits on Aug 30, 2024
-
Configuration menu - View commit details
-
Copy full SHA for ef98dc6 - Browse repository at this point
Copy the full SHA ef98dc6View commit details
Commits on Sep 2, 2024
-
Configuration menu - View commit details
-
Copy full SHA for a614769 - Browse repository at this point
Copy the full SHA a614769View commit details