@@ -539,6 +539,7 @@ fn main() {
539539 miri_config. borrow_tracker = None ;
540540 } else if arg == "-Zmiri-tree-borrows" {
541541 miri_config. borrow_tracker = Some ( BorrowTrackerMethod :: TreeBorrows ) ;
542+ miri_config. provenance_mode = ProvenanceMode :: Strict ;
542543 } else if arg == "-Zmiri-unique-is-unique" {
543544 miri_config. unique_is_unique = true ;
544545 } else if arg == "-Zmiri-disable-data-race-detector" {
@@ -728,13 +729,20 @@ fn main() {
728729 "-Zmiri-unique-is-unique only has an effect when -Zmiri-tree-borrows is also used"
729730 ) ;
730731 }
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" ) ;
738746 }
739747 // You can set either one seed or many.
740748 if many_seeds. is_some ( ) && miri_config. seed . is_some ( ) {
0 commit comments