These are annotations that track values that do not exist in the actual C program. The compiler ignores them and they have no effect on execution, but they help us in the proof to keep track of what is going on.

The first AUXUP in your email below, for instance, says that the memory starting at pointer `regionBase` for 2 to the power of `userSize` bytes, should now be tracked under the type `cte*`. Roughly speaking, this will usually lead us to prove that there are currently no other pointers to this area under another type and that the memory there is consistent with known cte values (usually just 0), and afterwards we know that pointers into this region are valid cte pointers. This often happens in memory allocation code, e.g. something like the `retype` operation in the kernel.

The updates can have conditions/guards on then, but they are usually just “True”, i.e. the empty condition.

Cheers, Gerwin

On 14 Jul 2015, at 7:07 pm, Pei.XiLong(裴喜龙) pei.xilong@kortide.com wrote:

Hi, In recent seL4 commit https://github.com/seL4/seL4/commit/67d8d041de0c435a1cc59ef8c237be6e39beb1c6 , A lot of comments like these: /** AUXUPD: "(True, ptr_retyps (2 ^ (unat <acute>userSize)) (Ptr (ptr_val <acute>regionBase) :: cte_C ptr))" */ /** GHOSTUPD: "(True, gs_new_cnodes (unat <acute>userSize) (ptr_val <acute>regionBase) (4 + unat <acute>userSize))" */ have been added into source code, What is their meaning? I don't know isablle, and just know a little about haskell.

  thanks!


  Xilong Pei
  Tongji University
  2015/7/14

---

Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.