Federico Poli
Federico Poli
The program ```rust use prusti_contracts::*; struct Node { sibling: Option, key: u32, } #[pure] #[requires(val > 0)] fn less_than_seg(curr: &Box, val: u32) -> bool { curr.key >= val && match...
Prusti reports an internal error ("generating fold-unfold Viper statements failed") when verifying the following program. The reason is that a postcondition tries to use `self` while it's blocked by a...
Prusti panics if its binaries are placed in a folder from which it's not possible to move to `../..`. The cause is these unwraps: https://github.com/viperproject/prusti-dev/blob/e1e8c9b45181663ba2a788e8c211e5dec27b6827/prusti-utils/src/launch/mod.rs#L36-L48 When the `parent()` calls fail...
Prusti fails to parse the following contract. ```rust use prusti_contracts::*; #[requires( true && if let Some(_) = x { //
The `./docs/dependency-graph/dependency_graph.py` does *not* generate the dependency edge `prusti-interface --> prusti-specs`.
Viper (the underlaying verification language) has [termination checks](https://viper.ethz.ch/tutorial/#termination) but Prusti doesn't use them yet. - [x] The user documentation should at least make it clear that at the moment one...
The tests fail on Python 3.8 : ``` $ nosetests EF ====================================================================== ERROR: test_export_json (export_test.TestExportJson) ---------------------------------------------------------------------- Traceback (most recent call last): File "/home/travis/build/fpoli/python-astexport/tests/export_test.py", line 16, in test_export_json result = json.loads(export_json(test.input))...
- Renames 'hepdataparent' field to 'datasource' - Associates 'author' field with tag '786__w' - Associates 'exactauthor' field with tag '786__w' - Adds tags '400__a' and '880__a' to 'exactauthor' field
- Associates the `address` field to a single `371__%` tag instead of many `371__a`, `371__b`, `371__c`, ... tags - Keeps other tags associated with the `address` field: `110__a`, `110__b`, `110__t`,...