prusti-dev
prusti-dev copied to clipboard
viperproject
Consistency error: identifier with `::`
I was trying out Prusti in https://github.com/arxanas/git-branchless/pull/777/commits/d087a311f7f7b1d1f83de1d47c2d809c01fd4857 via the VS Code extension, but got some errors. I was directed to report them here.
VS Code error output
[{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti internal error] Prusti encountered an unexpected internal error",
"startLineNumber": 1,
"startColumn": 1,
"endLineNumber": 1,
"endColumn": 1,
"relatedInformation": [
{
"startLineNumber": 1,
"startColumn": 1,
"endLineNumber": 1,
"endColumn": 1,
"message": "We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new",
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs"
},
{
"startLineNumber": 1,
"startColumn": 1,
"endLineNumber": 1,
"endColumn": 1,
"message": "Details: consistency error in scm_bisect::Search::<G>::new: Consistency error: __TYPARAM__$_impl_IntoIterator_lt_Item__eq__G::Node_gt_$1$__ is not a valid identifier. (<no position>)",
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs"
}
]
},{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti internal error] Prusti encountered an unexpected internal error",
"startLineNumber": 1,
"startColumn": 1,
"endLineNumber": 1,
"endColumn": 1,
"relatedInformation": [
{
"startLineNumber": 1,
"startColumn": 1,
"endLineNumber": 1,
"endColumn": 1,
"message": "We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new",
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs"
},
{
"startLineNumber": 1,
"startColumn": 1,
"endLineNumber": 1,
"endColumn": 1,
"message": "Details: consistency error in scm_bisect::Search::<G>::new: Consistency error: m_std$$iter$$IntoIterator$$IntoIter$__TYPARAM__$_impl_IntoIterator_lt_Item__eq__G::Node_gt_$1$__ is not a valid identifier. (<no position>)",
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs"
}
]
},{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti internal error] Prusti encountered an unexpected internal error",
"startLineNumber": 1,
"startColumn": 1,
"endLineNumber": 1,
"endColumn": 1,
"relatedInformation": [
{
"startLineNumber": 1,
"startColumn": 1,
"endLineNumber": 1,
"endColumn": 1,
"message": "We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new",
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs"
},
{
"startLineNumber": 1,
"startColumn": 1,
"endLineNumber": 1,
"endColumn": 1,
"message": "Details: consistency error in scm_bisect::Search::<G>::new: Consistency error: struct$m_std$$iter$$Map$m_std$$iter$$IntoIterator$$IntoIter$__TYPARAM__$_impl_IntoIterator_lt_Item__eq__G::Node_gt_$1$__$closure$m_Search$$$openang$G$closeang$$$new$$$opencur$closure$sharp$0$closecur$ is not a valid identifier. (<no position>)",
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs"
}
]
},{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti: unsupported feature] iterators are not fully supported yet",
"startLineNumber": 40,
"startColumn": 21,
"endLineNumber": 40,
"endColumn": 26
},{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti internal error] Prusti encountered an unexpected internal error",
"startLineNumber": 54,
"startColumn": 18,
"endLineNumber": 54,
"endColumn": 74,
"relatedInformation": [
{
"startLineNumber": 54,
"startColumn": 18,
"endLineNumber": 54,
"endColumn": 74,
"message": "We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new",
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs"
},
{
"startLineNumber": 54,
"startColumn": 18,
"endLineNumber": 54,
"endColumn": 74,
"message": "Details: cannot generate fold-unfold Viper statements. Failed to subtract fractional permissions: invalid substraction: read - write.\n",
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs"
}
]
},{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti: unsupported feature] higher-ranked lifetimes and types are not supported",
"startLineNumber": 56,
"startColumn": 42,
"endLineNumber": 69,
"endColumn": 15
},{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti internal error] Prusti encountered an unexpected internal error",
"startLineNumber": 58,
"startColumn": 21,
"endLineNumber": 69,
"endColumn": 14,
"relatedInformation": [
{
"startLineNumber": 58,
"startColumn": 21,
"endLineNumber": 69,
"endColumn": 14,
"message": "We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new",
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs"
},
{
"startLineNumber": 58,
"startColumn": 21,
"endLineNumber": 69,
"endColumn": 14,
"message": "Details: cannot generate fold-unfold Viper statements. Failed to subtract fractional permissions: invalid substraction: read - write.\n",
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs"
}
]
},{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti: unsupported feature] access to reference-typed fields is not supported",
"startLineNumber": 67,
"startColumn": 22,
"endLineNumber": 67,
"endColumn": 22
},{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti: unsupported feature] iterators are not fully supported yet",
"startLineNumber": 87,
"startColumn": 21,
"endLineNumber": 87,
"endColumn": 26
},{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti internal error] Prusti encountered an unexpected internal error",
"startLineNumber": 101,
"startColumn": 18,
"endLineNumber": 101,
"endColumn": 76,
"relatedInformation": [
{
"startLineNumber": 101,
"startColumn": 18,
"endLineNumber": 101,
"endColumn": 76,
"message": "We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new",
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs"
},
{
"startLineNumber": 101,
"startColumn": 18,
"endLineNumber": 101,
"endColumn": 76,
"message": "Details: cannot generate fold-unfold Viper statements. Failed to subtract fractional permissions: invalid substraction: read - write.\n",
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs"
}
]
},{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti: unsupported feature] higher-ranked lifetimes and types are not supported",
"startLineNumber": 103,
"startColumn": 42,
"endLineNumber": 116,
"endColumn": 15
},{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti internal error] Prusti encountered an unexpected internal error",
"startLineNumber": 105,
"startColumn": 21,
"endLineNumber": 116,
"endColumn": 14,
"relatedInformation": [
{
"startLineNumber": 105,
"startColumn": 21,
"endLineNumber": 116,
"endColumn": 14,
"message": "We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new",
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs"
},
{
"startLineNumber": 105,
"startColumn": 21,
"endLineNumber": 116,
"endColumn": 14,
"message": "Details: cannot generate fold-unfold Viper statements. Failed to subtract fractional permissions: invalid substraction: read - write.\n",
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs"
}
]
},{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti: unsupported feature] access to reference-typed fields is not supported",
"startLineNumber": 114,
"startColumn": 22,
"endLineNumber": 114,
"endColumn": 22
},{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti: unsupported feature] cast statements that create loans are not supported",
"startLineNumber": 169,
"startColumn": 10,
"endLineNumber": 169,
"endColumn": 15
},{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti: unsupported feature] cast statements that create loans are not supported",
"startLineNumber": 228,
"startColumn": 10,
"endLineNumber": 228,
"endColumn": 15
},{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti: unsupported feature] unsupported constant type Ref('_#68r, [&str; 2], Not)",
"startLineNumber": 238,
"startColumn": 13,
"endLineNumber": 238,
"endColumn": 59
},{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti: unsupported feature] cast statements that create loans are not supported",
"startLineNumber": 251,
"startColumn": 17,
"endLineNumber": 251,
"endColumn": 22
},{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti internal error] Prusti encountered an unexpected internal error",
"startLineNumber": 270,
"startColumn": 5,
"endLineNumber": 284,
"endColumn": 6,
"relatedInformation": [
{
"startLineNumber": 270,
"startColumn": 5,
"endLineNumber": 284,
"endColumn": 6,
"message": "We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new",
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs"
},
{
"startLineNumber": 270,
"startColumn": 5,
"endLineNumber": 284,
"endColumn": 6,
"message": "Details: cannot generate fold-unfold Viper statements. The required permission Acc(_6.closure_0.tuple_0.val_ref, read) cannot be obtained.\n",
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs"
}
]
},{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti internal error] Prusti encountered an unexpected internal error",
"startLineNumber": 274,
"startColumn": 25,
"endLineNumber": 277,
"endColumn": 14,
"relatedInformation": [
{
"startLineNumber": 274,
"startColumn": 25,
"endLineNumber": 277,
"endColumn": 14,
"message": "We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new",
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs"
},
{
"startLineNumber": 274,
"startColumn": 25,
"endLineNumber": 277,
"endColumn": 14,
"message": "Details: cannot generate fold-unfold Viper statements. The required permission Pred(old[pre]((unfolding acc(Ref(tuple2$ref$m_SearchGraph$$Node$__TYPARAM__$_G$0$__$ref$m_Status$_beg_$_end_)(_2), write) in (unfolding acc(Ref(ref$m_Status$_beg_$_end_)(_2.tuple_1), write) in _2.tuple_1.val_ref))), read) cannot be obtained.\n",
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs"
}
]
},{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti: unsupported feature] unsizing a std::boxed::Box<<G as SearchGraph>::Error> into a std::boxed::Box<dyn std::error::Error> is not supported",
"startLineNumber": 282,
"startColumn": 46,
"endLineNumber": 282,
"endColumn": 59
},{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti internal error] Prusti encountered an unexpected internal error",
"startLineNumber": 289,
"startColumn": 5,
"endLineNumber": 303,
"endColumn": 6,
"relatedInformation": [
{
"startLineNumber": 289,
"startColumn": 5,
"endLineNumber": 303,
"endColumn": 6,
"message": "We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new",
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs"
},
{
"startLineNumber": 289,
"startColumn": 5,
"endLineNumber": 303,
"endColumn": 6,
"message": "Details: cannot generate fold-unfold Viper statements. The required permission Acc(_6.closure_0.tuple_0.val_ref, read) cannot be obtained.\n",
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs"
}
]
},{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti internal error] Prusti encountered an unexpected internal error",
"startLineNumber": 293,
"startColumn": 25,
"endLineNumber": 296,
"endColumn": 14,
"relatedInformation": [
{
"startLineNumber": 293,
"startColumn": 25,
"endLineNumber": 296,
"endColumn": 14,
"message": "We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new",
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs"
},
{
"startLineNumber": 293,
"startColumn": 25,
"endLineNumber": 296,
"endColumn": 14,
"message": "Details: cannot generate fold-unfold Viper statements. The required permission Pred(old[pre]((unfolding acc(Ref(tuple2$ref$m_SearchGraph$$Node$__TYPARAM__$_G$0$__$ref$m_Status$_beg_$_end_)(_2), write) in (unfolding acc(Ref(ref$m_Status$_beg_$_end_)(_2.tuple_1), write) in _2.tuple_1.val_ref))), read) cannot be obtained.\n",
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs"
}
]
},{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti: unsupported feature] unsizing a std::boxed::Box<<G as SearchGraph>::Error> into a std::boxed::Box<dyn std::error::Error> is not supported",
"startLineNumber": 301,
"startColumn": 46,
"endLineNumber": 301,
"endColumn": 59
},{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti: unsupported feature] unsizing a std::boxed::Box<<G as SearchGraph>::Error> into a std::boxed::Box<dyn std::error::Error> is not supported",
"startLineNumber": 314,
"startColumn": 50,
"endLineNumber": 314,
"endColumn": 63
},{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti: unsupported feature] unsizing a std::boxed::Box<<G as SearchGraph>::Error> into a std::boxed::Box<dyn std::error::Error> is not supported",
"startLineNumber": 318,
"startColumn": 50,
"endLineNumber": 318,
"endColumn": 63
},{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti: unsupported feature] higher-ranked lifetimes and types are not supported",
"startLineNumber": 319,
"startColumn": 13,
"endLineNumber": 327,
"endColumn": 19
},{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti internal error] Prusti encountered an unexpected internal error",
"startLineNumber": 321,
"startColumn": 29,
"endLineNumber": 324,
"endColumn": 18,
"relatedInformation": [
{
"startLineNumber": 321,
"startColumn": 29,
"endLineNumber": 324,
"endColumn": 18,
"message": "We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new",
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs"
},
{
"startLineNumber": 321,
"startColumn": 29,
"endLineNumber": 324,
"endColumn": 18,
"message": "Details: cannot generate fold-unfold Viper statements. The required permission Pred(old[pre]((unfolding acc(Ref(tuple2$ref$m_SearchGraph$$Node$__TYPARAM__$_G$0$__$ref$m_Status$_beg_$_end_)(_2), write) in (unfolding acc(Ref(ref$m_Status$_beg_$_end_)(_2.tuple_1), write) in _2.tuple_1.val_ref))), read) cannot be obtained.\n",
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs"
}
]
},{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti internal error] Prusti encountered an unexpected internal error",
"startLineNumber": 325,
"startColumn": 25,
"endLineNumber": 327,
"endColumn": 18,
"relatedInformation": [
{
"startLineNumber": 325,
"startColumn": 25,
"endLineNumber": 327,
"endColumn": 18,
"message": "We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new",
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs"
},
{
"startLineNumber": 325,
"startColumn": 25,
"endLineNumber": 327,
"endColumn": 18,
"message": "Details: cannot generate fold-unfold Viper statements. Failed to subtract fractional permissions: invalid substraction: read - write.\n",
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs"
}
]
},{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti: unsupported feature] access to reference-typed fields is not supported",
"startLineNumber": 345,
"startColumn": 15,
"endLineNumber": 345,
"endColumn": 36
},{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti: unsupported feature] unsizing a std::boxed::Box<<G as SearchGraph>::Error> into a std::boxed::Box<dyn std::error::Error> is not supported",
"startLineNumber": 366,
"startColumn": 58,
"endLineNumber": 366,
"endColumn": 71
},{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti: unsupported feature] unsizing a std::boxed::Box<<G as SearchGraph>::Error> into a std::boxed::Box<dyn std::error::Error> is not supported",
"startLineNumber": 383,
"startColumn": 58,
"endLineNumber": 383,
"endColumn": 71
},{
"resource": "/Users/waleed/Workspace/git-branchless/scm-bisect/scm-bisect/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti: unsupported feature] unsupported type Alias(Opaque, AliasTy { substs: [G, ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrNamed(DefId(0:63 ~ scm_bisect[bb37]::{impl#2}::make_binary_search_iter::'a), 'a) })], def_id: DefId(0:175 ~ scm_bisect[bb37]::{impl#2}::make_binary_search_iter::{opaque#0}), _use_mk_alias_ty_instead: () })",
"startLineNumber": 400,
"startColumn": 5,
"endLineNumber": 424,
"endColumn": 6
}]
Thank you for the report! One identifier generated by Prusti incorrectly contains a ::.
The detailed error from the log:
consistency error in scm_bisect::Search::<G>::new: Consistency error: struct$m_std$$iter$$Map$m_std$$iter$$IntoIterator$$IntoIter$__TYPARAM__$_impl_IntoIterator_lt_Item__eq__G::Node_gt_$1$__$closure$m_Search$$$openang$G$closeang$$$new$$$opencur$closure$sharp$0$closecur$ is not a valid identifier.
