Skip to content

Commit

Permalink
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
bidirectional ppc error
Browse files Browse the repository at this point in the history
midnightveil committed Sep 4, 2024

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
1 parent 8d9cda6 commit db066b2
Showing 3 changed files with 34 additions and 0 deletions.
8 changes: 8 additions & 0 deletions tool/microkit/src/sdf.rs
Original file line number Diff line number Diff line change
@@ -860,6 +860,14 @@ impl Channel {
));
};

if end_a.can_ppcall_other && end_b.can_ppcall_other {
return Err(value_error(
xml_sdf,
node,
"cannot ppc bidirectionally".to_string(),
));
}

Ok(Channel {
end_a: end_a.clone(),
end_b: end_b.clone(),
18 changes: 18 additions & 0 deletions tool/microkit/tests/sdf/ch_bidirectional_ppc.xml
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<protection_domain name="test1">
<program_image path="test" />
</protection_domain>
<protection_domain name="test2">
<program_image path="test" />
</protection_domain>
<channel>
<end pd="test1" id="0" pp="true" />
<end pd="test2" id="0" pp="true" />
</channel>
</system>
8 changes: 8 additions & 0 deletions tool/microkit/tests/test.rs
Original file line number Diff line number Diff line change
@@ -368,6 +368,14 @@ mod channel {
"Error: PPCs must be to protection domains of strictly higher priorities; you did from pd test1 (priority: 2) to pd test2 (priority: 1)",
)
}

#[test]
fn test_bidirectional_ppc() {
check_error(
"ch_bidirectional_ppc.xml",
"Error: cannot ppc bidirectionally on element 'channel': ",
)
}
}

#[cfg(test)]

0 comments on commit db066b2

Please sign in to comment.