How does strptr_is_null Implemented?

Google Group
1

Hi,

I noticed that there are two functions in ATS sources

fun strptr_is_null
{l:addr} (x: !strptr l):<> bool (l==null) = "#atspre_ptr_is_null"fun strptr_isnot_null
{l:addr} (x: !strptr l):<> bool (l > null) = “#atspre_ptr_isnot_null”

I am not familiar with those two highlighted part. What are these? And how
to use them?

Thank you!

2

I believe you would say these are dependent Boolean types; the second function would be necessary to call before a function requiring a non null string pointer.

3

Actually, in this case, if I recall correctly, the implementations are c functions (the part in quotes), so no proof is given, making these more similar to a “praxi” as far as the proof system is concerned.

4

Thank you very much! That helps a lot.

5

You can also implement it in ATS:

implement strptr_is_null (str) = (strptr2ptr (str) = 0)

6

So essentially it is up to those two functions, specifically their implementations, to prove l is (or is not) null.

7

Yes, it is implemented in C. And it depends on the programmer to implement
it correctly to match the interface in ATS.