Hey there, Splint people!
I'm just starting off with Splint and I have a great many questions. They
are as follows:
- When writing code that uses function pointer tables and one of those
functions returns a pointer to storage, how do I specify that the function
pointer itself can be used infinitely and is never released (@shared@?)
but the storage it returns should be considered dependent?
Like... the caller of that method would acquire a reference to some
storage and it's reference is dependent. It's up to the caller to ensure
that it doesn't use that storage after it's released.
Would I need to specify ``inner'' annotations?
- How would I annotate a function, F, that creates an instance of type T and
accepts storage given on parameter P, where the instance of T is to gain
complete ownership (and obligation to release the storage) if the instance
could be successfully allocated. Otherwise, the storage passed into the
function is left as it was on call? I.e. the original owner is still the
owner and still has the obligation to release the storage?
- I'm having a little trouble understanding @abstract@, @observer@ and
@exposed@. If I'm returning a reference to storage which is owned by an
instance of an opaque type (@abstract@?), do I need to specify the
@observer@ annotation? E.g.
@observer@ type *get_bla(opaque_type *);
What about if there are two calls, that both serve the same purpose
(returning a reference to the data) except that one returns a const
reference and the other doesn't?
How would I annotate that precisely?
I have many questions like this and will probably pester you guys a lot.
I'm wondering about this all as I'd love to use Splint to help me write
better code. I'm currently tinkering with class-type stuff in C, tons of
function pointers that act as methods, structs augmented that hold data,
e.t.c. It'd be great if I could document it precisely with Splint.
~Dave Ward
_______________________________________________
splint-discuss mailing list
splint-discuss@mail.cs.virginia.edu
http://www.cs.virginia.edu/mailman/listinfo/splint-discuss
