Commit 03c5649b authored by Rodolphe Lepigre's avatar Rodolphe Lepigre Committed by Paul
Browse files

Used type abbreviation in BFF example.

parent 233665f9
......@@ -39,6 +39,8 @@ typedef u64 pte_t;
//@ pte_leaf_attr_hi: integer[51..63]
//@rc::end
//@rc::typedef pte_t ≔ bitfield<Pte>
#define PTE_TYPE_BLOCK 0
#define PTE_TYPE_PAGE 1
#define PTE_TYPE_TABLE 1
......@@ -55,7 +57,7 @@ typedef u64 pte_t;
//@rc::end
[[rc::parameters("pte : Pte")]]
[[rc::args("pte @ bitfield<Pte>")]]
[[rc::args("pte @ pte_t")]]
[[rc::requires("{bitfield_wf pte}")]] // FIXME not necessary.
[[rc::returns("{pte_valid pte} @ boolean<bool_it>")]]
static bool pte_valid(pte_t pte) {
......@@ -78,7 +80,7 @@ static bool pte_valid(pte_t pte) {
[[rc::requires("{bitfield_wf old}", "{bitfield_wf pa}", "{bitfield_wf attr}")]] // FIXME not necessary.
[[rc::parameters("p : loc", "old : Pte", "pa : Pte", "attr : Pte", "level : Z")]]
[[rc::args("p @ &own<old @ bitfield<Pte>>", "pa @ bitfield<Pte>", "attr @ bitfield<Pte>", "level @ int<u32>")]]
[[rc::args("p @ &own<old @ pte_t>", "pa @ pte_t", "attr @ pte_t", "level @ int<u32>")]]
[[rc::requires("{old.(pte_valid) = false}")]]
[[rc::returns("{true} @ boolean<bool_it>")]]
[[rc::ensures("own p : {svl_pte pa level attr} @ bitfield<Pte>")]]
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment