Skip to content

Commit 3db55ce

Browse files
tjhancetjhance
authored
fix some Never handling (#2043)
1 parent 0e5bbfe commit 3db55ce

3 files changed

Lines changed: 525 additions & 232 deletions

File tree

‎source/rust_verify_test/tests/mut_refs.rs‎

Lines changed: 245 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2763,3 +2763,248 @@ test_verify_one_file_with_options! {
27632763
}
27642764
} => Err(err) => assert_fails(err, 1)
27652765
}
2766+
2767+
test_verify_one_file_with_options! {
2768+
#[test] place_that_doesnt_return ["new-mut-ref"] => verus_code! {
2769+
use vstd::prelude::*;
2770+
2771+
#[allow(unreachable_code)]
2772+
#[verifier::exec_allows_no_decreases_clause]
2773+
fn test1() {
2774+
let mut a = 4;
2775+
*({ loop {}; &mut a }) = 5;
2776+
assert(false);
2777+
}
2778+
2779+
#[allow(unreachable_code)]
2780+
#[verifier::exec_allows_no_decreases_clause]
2781+
fn test2() {
2782+
let mut a = 4;
2783+
*({ loop {}; &mut a }) = ({ assert(false); 5 });
2784+
assert(false);
2785+
}
2786+
2787+
#[allow(unreachable_code)]
2788+
#[verifier::exec_allows_no_decreases_clause]
2789+
fn test2_fails() {
2790+
let mut a = 4;
2791+
*({
2792+
assert(false); // FAILS
2793+
&mut a }) = ({ loop {} 5 });
2794+
}
2795+
2796+
#[allow(unreachable_code)]
2797+
#[verifier::exec_allows_no_decreases_clause]
2798+
fn test3() {
2799+
let mut a = 4;
2800+
let mut a_ref: &mut u64 = loop { };
2801+
assert(false);
2802+
}
2803+
2804+
#[allow(unreachable_code)]
2805+
#[verifier::exec_allows_no_decreases_clause]
2806+
fn test4() {
2807+
let y: [[u64; 2]; 2] = [[0,1],[2,3]];
2808+
let x = y[({ loop{}; 0 })][({ assert(false); 1 })];
2809+
}
2810+
2811+
#[allow(unreachable_code)]
2812+
#[verifier::exec_allows_no_decreases_clause]
2813+
fn test5() {
2814+
let y: [[u64; 2]; 2] = [[0,1],[2,3]];
2815+
let x = y[({
2816+
assert(false); // FAILS
2817+
1})][({ loop{}; 0 })];
2818+
}
2819+
2820+
#[allow(unreachable_code)]
2821+
#[verifier::exec_allows_no_decreases_clause]
2822+
fn test6(y: [&mut (u64, u64); 2]) {
2823+
let mut y = y;
2824+
(*y[({ loop{} 0 })]).0 = 20;
2825+
assert(false);
2826+
}
2827+
} => Err(e) => assert_fails(e, 2)
2828+
}
2829+
2830+
test_verify_one_file_with_options! {
2831+
#[test] compound_op_that_doesnt_return ["new-mut-ref"] => verus_code! {
2832+
#[allow(unreachable_code)]
2833+
#[verifier::exec_allows_no_decreases_clause]
2834+
fn test1(y: [&mut (u64, u64); 2]) {
2835+
let mut y = y;
2836+
(*y[({ loop{} 0 })]).0 += 20;
2837+
}
2838+
2839+
#[allow(unreachable_code)]
2840+
#[verifier::exec_allows_no_decreases_clause]
2841+
fn test2(y: [&mut (u64, u64); 2]) {
2842+
let mut y = y;
2843+
(*y[({
2844+
assert(false); // FAILS
2845+
0 })]).0 += ({ loop{} 20 });
2846+
}
2847+
2848+
#[allow(unreachable_code)]
2849+
#[verifier::exec_allows_no_decreases_clause]
2850+
fn test3(y: [&mut (u64, u64); 2]) {
2851+
let mut y = y;
2852+
(*y[0]).0 += ({ loop{} 20 });
2853+
}
2854+
2855+
#[allow(unreachable_code)]
2856+
#[verifier::exec_allows_no_decreases_clause]
2857+
fn test4(y: &mut [&mut (u64, u64); 2])
2858+
ensures mut_ref_current(y) == mut_ref_future(y)
2859+
{
2860+
let mut y = y;
2861+
(*y[0]).0 += ({ return; 20 });
2862+
}
2863+
2864+
#[allow(unreachable_code)]
2865+
#[verifier::exec_allows_no_decreases_clause]
2866+
fn test4_fails(y: &mut [&mut (u64, u64); 2])
2867+
ensures false
2868+
{
2869+
let mut y = y;
2870+
(*y[0]).0 += ({
2871+
return; // FAILS
2872+
0
2873+
});
2874+
}
2875+
} => Err(e) => assert_fails(e, 2)
2876+
}
2877+
2878+
test_verify_one_file_with_options! {
2879+
#[test] call_with_args_that_dont_return ["new-mut-ref"] => verus_code! {
2880+
fn call(a: &mut u64, b: &mut u64, c: &mut u64) { }
2881+
2882+
fn call_requires_false(a: &mut u64, b: &mut u64, c: &mut u64)
2883+
requires false
2884+
{ }
2885+
2886+
#[verifier::exec_allows_no_decreases_clause]
2887+
#[allow(unreachable_code)]
2888+
fn test1() {
2889+
let mut a = 20;
2890+
let mut b = 30;
2891+
let mut c = 40;
2892+
call_requires_false(&mut a, ({ loop {} &mut b }), &mut c);
2893+
}
2894+
2895+
#[verifier::exec_allows_no_decreases_clause]
2896+
#[allow(unreachable_code)]
2897+
fn test2() {
2898+
let mut a = 20;
2899+
let mut b = 30;
2900+
let mut c = 40;
2901+
call_requires_false(&mut a, (loop {}), &mut c);
2902+
}
2903+
2904+
#[verifier::exec_allows_no_decreases_clause]
2905+
#[allow(unreachable_code)]
2906+
fn test3(a_ref: &mut u64, c_ref: &mut u64)
2907+
ensures
2908+
mut_ref_future(a_ref) == mut_ref_current(a_ref),
2909+
mut_ref_future(c_ref) == mut_ref_current(c_ref),
2910+
{
2911+
call_requires_false(a_ref, (return), c_ref);
2912+
}
2913+
2914+
#[verifier::exec_allows_no_decreases_clause]
2915+
#[allow(unreachable_code)]
2916+
fn test3_fails(a_ref: &mut u64, c_ref: &mut u64)
2917+
ensures
2918+
false
2919+
{
2920+
call_requires_false(a_ref, (
2921+
return // FAILS
2922+
), c_ref);
2923+
}
2924+
2925+
#[verifier::exec_allows_no_decreases_clause]
2926+
#[allow(unreachable_code)]
2927+
fn test4() {
2928+
let mut a = 20;
2929+
let mut b = 30;
2930+
let mut c = 40;
2931+
call_requires_false(&mut a, (loop {}), ({ assert(false); &mut c }));
2932+
}
2933+
2934+
#[verifier::exec_allows_no_decreases_clause]
2935+
#[allow(unreachable_code)]
2936+
fn test5() {
2937+
let mut a = 20;
2938+
let mut b = 30;
2939+
let mut c = 40;
2940+
call(({
2941+
assert(false); // FAILS
2942+
&mut a }), (loop {}), &mut c);
2943+
}
2944+
} => Err(e) => assert_fails(e, 2)
2945+
}
2946+
2947+
test_verify_one_file_with_options! {
2948+
#[test] ctor_with_args_that_dont_return ["new-mut-ref"] => verus_code! {
2949+
struct Ctor<'a, 'b, 'c>(&'a mut u64, &'b mut u64, &'c mut u64);
2950+
2951+
#[verifier::exec_allows_no_decreases_clause]
2952+
#[allow(unreachable_code)]
2953+
fn test1() {
2954+
let mut a = 20;
2955+
let mut b = 30;
2956+
let mut c = 40;
2957+
let ct = Ctor(&mut a, ({ loop {} &mut b }), &mut c);
2958+
}
2959+
2960+
#[verifier::exec_allows_no_decreases_clause]
2961+
#[allow(unreachable_code)]
2962+
fn test2() {
2963+
let mut a = 20;
2964+
let mut b = 30;
2965+
let mut c = 40;
2966+
let ct = Ctor(&mut a, (loop {}), &mut c);
2967+
}
2968+
2969+
#[verifier::exec_allows_no_decreases_clause]
2970+
#[allow(unreachable_code)]
2971+
fn test3(a_ref: &mut u64, c_ref: &mut u64)
2972+
ensures
2973+
mut_ref_future(a_ref) == mut_ref_current(a_ref),
2974+
mut_ref_future(c_ref) == mut_ref_current(c_ref),
2975+
{
2976+
let ct = Ctor(a_ref, (return), c_ref);
2977+
}
2978+
2979+
#[verifier::exec_allows_no_decreases_clause]
2980+
#[allow(unreachable_code)]
2981+
fn test3_fails(a_ref: &mut u64, c_ref: &mut u64)
2982+
ensures
2983+
false
2984+
{
2985+
let ct = Ctor(a_ref, (
2986+
return // FAILS
2987+
), c_ref);
2988+
}
2989+
2990+
#[verifier::exec_allows_no_decreases_clause]
2991+
#[allow(unreachable_code)]
2992+
fn test4() {
2993+
let mut a = 20;
2994+
let mut b = 30;
2995+
let mut c = 40;
2996+
let ct = Ctor(&mut a, (loop {}), ({ assert(false); &mut c }));
2997+
}
2998+
2999+
#[verifier::exec_allows_no_decreases_clause]
3000+
#[allow(unreachable_code)]
3001+
fn test5() {
3002+
let mut a = 20;
3003+
let mut b = 30;
3004+
let mut c = 40;
3005+
let ct = Ctor(({
3006+
assert(false); // FAILS
3007+
&mut a }), (loop {}), &mut c);
3008+
}
3009+
} => Err(e) => assert_fails(e, 2)
3010+
}

0 commit comments

Comments
 (0)