Skip to content

Commit

Permalink
update expect
Browse files Browse the repository at this point in the history
  • Loading branch information
@nikomatsakis
nikomatsakis committed Feb 6, 2025
1 parent d25ae43 commit 8218458
Show file tree
Hide file tree
Showing 9 changed files with 558 additions and 436 deletions.
40 changes: 12 additions & 28 deletions src/type_system/tests/assignment.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -115,20 +115,12 @@ fn forall_shared_P_assign_to_field_of_P_pair() {
judgment `type_statements_with_final_ty { statements: [pair . d1 = data . give ;, () ;], ty: (), env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: my Data, pair: !perm_0 Pair}, assumptions: {copy(!perm_0), relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
the rule "cons" failed at step #1 (src/file.rs:LL:CC) because
judgment `type_statement { statement: pair . d1 = data . give ;, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: my Data, pair: !perm_0 Pair}, assumptions: {copy(!perm_0), relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
the rule "reassign" failed at step #1 (src/file.rs:LL:CC) because
judgment `type_expr_as { expr: data . give, as_ty: Data, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: my Data, pair: !perm_0 Pair}, assumptions: {copy(!perm_0), relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {pair} } }` failed at the following rule(s):
the rule "type_expr_as" failed at step #0 (src/file.rs:LL:CC) because
judgment `type_expr { expr: data . give, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: my Data, pair: !perm_0 Pair}, assumptions: {copy(!perm_0), relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {pair} } }` failed at the following rule(s):
the rule "give place" failed at step #0 (src/file.rs:LL:CC) because
judgment `access_permitted { access: give, place: data, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: my Data, pair: !perm_0 Pair}, assumptions: {copy(!perm_0), relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {pair} } }` failed at the following rule(s):
the rule "access_permitted" failed at step #0 (src/file.rs:LL:CC) because
judgment `env_permits_access { access: give, place: data, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: my Data, pair: !perm_0 Pair}, assumptions: {copy(!perm_0), relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {pair} } }` failed at the following rule(s):
the rule "env_permits_access" failed at step #1 (src/file.rs:LL:CC) because
judgment `parameters_permit_access { parameters: [!perm_0 Pair], access: give, place: data, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: my Data, pair: !perm_0 Pair}, assumptions: {copy(!perm_0), relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
the rule "cons" failed at step #0 (src/file.rs:LL:CC) because
judgment `parameter_permits_access { parameter: !perm_0 Pair, access: give, place: data, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: my Data, pair: !perm_0 Pair}, assumptions: {copy(!perm_0), relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
the rule "parameter" failed at step #1 (src/file.rs:LL:CC) because
judgment had no applicable rules: `lien_permit_access { lien: Variable(!perm_0), access: give, accessed_place: data, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: my Data, pair: !perm_0 Pair}, assumptions: {copy(!perm_0), relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }`"#]]);
the rule "reassign" failed at step #3 (src/file.rs:LL:CC) because
judgment `prove_is_moved { a: !perm_0 Pair, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, @ fresh(0): Data, data: my Data, pair: !perm_0 Pair}, assumptions: {copy(!perm_0), relative(!perm_0), atomic(!perm_0)}, fresh: 1 } }` failed at the following rule(s):
the rule "is-moved" failed at step #0 (src/file.rs:LL:CC) because
judgment `prove_predicate { predicate: move(!perm_0 Pair), env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, @ fresh(0): Data, data: my Data, pair: !perm_0 Pair}, assumptions: {copy(!perm_0), relative(!perm_0), atomic(!perm_0)}, fresh: 1 } }` failed at the following rule(s):
the rule "moved" failed at step #1 (src/file.rs:LL:CC) because
condition evaluted to false: `is_moved`"#]]);
}

/// Test that field is not assignable when using a perm var that is not shared.
Expand Down Expand Up @@ -165,18 +157,10 @@ fn forall_P_assign_to_field_of_P_pair() {
judgment `type_statements_with_final_ty { statements: [pair . d1 = data . give ;, () ;], ty: (), env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: my Data, pair: !perm_0 Pair}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
the rule "cons" failed at step #1 (src/file.rs:LL:CC) because
judgment `type_statement { statement: pair . d1 = data . give ;, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: my Data, pair: !perm_0 Pair}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
the rule "reassign" failed at step #1 (src/file.rs:LL:CC) because
judgment `type_expr_as { expr: data . give, as_ty: Data, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: my Data, pair: !perm_0 Pair}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {pair} } }` failed at the following rule(s):
the rule "type_expr_as" failed at step #0 (src/file.rs:LL:CC) because
judgment `type_expr { expr: data . give, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: my Data, pair: !perm_0 Pair}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {pair} } }` failed at the following rule(s):
the rule "give place" failed at step #0 (src/file.rs:LL:CC) because
judgment `access_permitted { access: give, place: data, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: my Data, pair: !perm_0 Pair}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {pair} } }` failed at the following rule(s):
the rule "access_permitted" failed at step #0 (src/file.rs:LL:CC) because
judgment `env_permits_access { access: give, place: data, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: my Data, pair: !perm_0 Pair}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {pair} } }` failed at the following rule(s):
the rule "env_permits_access" failed at step #1 (src/file.rs:LL:CC) because
judgment `parameters_permit_access { parameters: [!perm_0 Pair], access: give, place: data, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: my Data, pair: !perm_0 Pair}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
the rule "cons" failed at step #0 (src/file.rs:LL:CC) because
judgment `parameter_permits_access { parameter: !perm_0 Pair, access: give, place: data, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: my Data, pair: !perm_0 Pair}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
the rule "parameter" failed at step #1 (src/file.rs:LL:CC) because
judgment had no applicable rules: `lien_permit_access { lien: Variable(!perm_0), access: give, accessed_place: data, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: my Data, pair: !perm_0 Pair}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }`"#]]);
the rule "reassign" failed at step #3 (src/file.rs:LL:CC) because
judgment `prove_is_moved { a: !perm_0 Pair, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, @ fresh(0): Data, data: my Data, pair: !perm_0 Pair}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 1 } }` failed at the following rule(s):
the rule "is-moved" failed at step #0 (src/file.rs:LL:CC) because
judgment `prove_predicate { predicate: move(!perm_0 Pair), env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, @ fresh(0): Data, data: my Data, pair: !perm_0 Pair}, assumptions: {relative(!perm_0), atomic(!perm_0)}, fresh: 1 } }` failed at the following rule(s):
the rule "moved" failed at step #1 (src/file.rs:LL:CC) because
condition evaluted to false: `is_moved`"#]]);
}
12 changes: 6 additions & 6 deletions src/type_system/tests/cancellation.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -101,9 +101,9 @@ fn shared_live_leased_to_our_leased() {
live_after = LivePlaces { accessed: {p}, traversed: {} }
&place_a = p
the rule "shared-vs-our-leased" failed at step #2 (src/file.rs:LL:CC) because
condition evaluted to false: `place_a.is_prefix_of(&place_b)`
place_a = p
&place_b = d"#]]);
condition evaluted to false: `place_b.is_prefix_of(&place_a)`
place_b = d
&place_a = p"#]]);
}

#[test]
Expand Down Expand Up @@ -196,9 +196,9 @@ fn leased_live_leased_to_leased() {
live_after = LivePlaces { accessed: {p}, traversed: {} }
&place_a = p
the rule "leased-vs-leased" failed at step #2 (src/file.rs:LL:CC) because
condition evaluted to false: `place_a.is_prefix_of(&place_b)`
place_a = p
&place_b = d
condition evaluted to false: `place_b.is_prefix_of(&place_a)`
place_b = d
&place_a = p
the rule "my-sub-copy" failed at step #0 (src/file.rs:LL:CC) because
condition evaluted to false: `chain_a.is_owned(&env)`
chain_a = Chain { liens: [Leased(p), Leased(d)] }
Expand Down
Loading

0 comments on commit 8218458

Please sign in to comment.