Hello,
I'm a developer of the tool named "api-sanity-autotest" that uses the
splint annotations from the library header files. The tool itself is an
automatic generator of basic runtime unit tests for C/C++ libraries. The
tool uses the following annotations with the aim of improving the tests
quality: @returned@, @out@, @notnull@, @requires@, @ensures@, @abstr...@.
And I have some suggestions for the splint evolution:
1) Add an ability to dump all annotations from the header file to the
XML file. The option --dump-annotations will be very helpful for me. The
format of dump may be the following:
<annotation>
<interface>
name of the interface annotated
</interface>
<target>
retval
param1
param2
...
</target>
<body>
ensures ...
...
</body>
</annotation>
2) Add a @private@ annotation to the interface. It will tell the splint
that this interface should not be verified.
3) Annotating the C++ code.
Thanks!
--
Andrey Ponomarenko
Linux Verification Center, ISPRAS
web: http://www.linuxtesting.org
mail: [email protected]
_______________________________________________
splint-discuss mailing list
[email protected]
http://www.cs.virginia.edu/mailman/listinfo/splint-discuss
