@@ -539,6 +539,7 @@ fn main() {
539
539
miri_config. borrow_tracker = None ;
540
540
} else if arg == "-Zmiri-tree-borrows" {
541
541
miri_config. borrow_tracker = Some ( BorrowTrackerMethod :: TreeBorrows ) ;
542
+ miri_config. provenance_mode = ProvenanceMode :: Strict ;
542
543
} else if arg == "-Zmiri-unique-is-unique" {
543
544
miri_config. unique_is_unique = true ;
544
545
} else if arg == "-Zmiri-disable-data-race-detector" {
@@ -728,13 +729,20 @@ fn main() {
728
729
"-Zmiri-unique-is-unique only has an effect when -Zmiri-tree-borrows is also used"
729
730
) ;
730
731
}
731
- // Tree Borrows + permissive provenance does not work.
732
- if miri_config. provenance_mode == ProvenanceMode :: Permissive
733
- && matches ! ( miri_config. borrow_tracker, Some ( BorrowTrackerMethod :: TreeBorrows ) )
734
- {
735
- show_error ! (
736
- "Tree Borrows does not support integer-to-pointer casts, and is hence not compatible with permissive provenance"
737
- ) ;
732
+ // Tree Borrows implies strict provenance, and is not compatible with native calls.
733
+ if matches ! ( miri_config. borrow_tracker, Some ( BorrowTrackerMethod :: TreeBorrows ) ) {
734
+ if miri_config. provenance_mode != ProvenanceMode :: Strict {
735
+ show_error ! (
736
+ "Tree Borrows does not support integer-to-pointer casts, and hence requires strict provenance"
737
+ ) ;
738
+ }
739
+ if miri_config. native_lib . is_some ( ) {
740
+ show_error ! ( "Tree Borrows is not compatible with calling native functions" ) ;
741
+ }
742
+ }
743
+ // Native calls and strict provenance are not compatible.
744
+ if miri_config. native_lib . is_some ( ) && miri_config. provenance_mode == ProvenanceMode :: Strict {
745
+ show_error ! ( "strict provenance is not compatible with calling native functions" ) ;
738
746
}
739
747
// You can set either one seed or many.
740
748
if many_seeds. is_some ( ) && miri_config. seed . is_some ( ) {
0 commit comments