TOPICS is a tool dedicated to the verification of C-like programs. The particularity of this tool lies in the fact that it can deal with programs manipulating dynamic data structures. In this first version, TOPICS can treat programs working over singly linked lists, but this feature will be extended to more complex data structures. The main feature of TOPICS is the translation of C-like programs into a bisimilar counter system, where counter systems correspond to finite automata extended with (unbounded) integer variables. This translation allows to use tools which verifies counter systems in order to check that the given program do not realize errors as memory violation, memory leakage or out of bound error.
The translation implemented in TOPICS corresponds to the one presented in the article From Pointer Systems to Counter Systems Using Shape Analysis. The programs given in input of TOPICS are written in a syntaxic fragment of the C programming language. These programs can manipulate integer variables, singly linked lists and arrays of integers and of lists. Whereas there is no restriction on the size of the manipulating lists, the arrays have to be of finite size. The user has also the possibility to give an initial configuration to TOPICS, in which he will characterize the initial state of the memory he wants the programs to begin with.
The following table gives some files produced by TOPICS for different programs.
In the first two colums, there are the program given in input and the description of the initial configuration. The third column contains a representation of the control flow graph produced by TOPICS. The fourth column contains a description of the counter system produced by TOPICS. The two last columns contain the files produced for the tools FAST and ASPIC.
| Program | Initial configuration | Control Flow Graph | Counter automaton | FAST file | ASPIC files |
|---|---|---|---|---|---|
| create.c | create_automaton.pdf | createCA.pdf | create.fst | create_MemL_aspic.fst | |
| insert.c | conf.init | insert_automaton.pdf | insertCA.pdf | insert.fst | insert_MemL_aspic.fst |
| reverse.c | conf.init | reverse_automaton.pdf | reverseCA.pdf | reverse.fst | reverse_MemL_aspic.fst |
| deleteAll.c | conf.init | deleteAll_automaton.pdf | deleteAllCA.pdf | deleteAll.fst | deleteAll_MemL_aspic.fst |
| merge.c | conf.init | merge_automaton.pdf | The counter automaton is too big | merge.fst |
merge_MemL_aspic.fst merge_SegF_aspic.fst |
| mainReverse.c | main_automaton.pdf | mainCA.pdf | main.fst |
main_MemL_aspic.fst main_Undef_aspic.fst |
|
| doubleFree.c | conf.init | doubleFree_automaton.pdf | doubleFreeCA.pdf | doubleFree.fst |
doubleFree_SegF_aspic.fst doubleFree_MemL_aspic.fst |
| doubleFree.c |
conf.init with list of even length |
doubleFree_automaton.pdf | doubleFreeCA.pdf | doubleFree.fst |
doubleFree_SegF_aspic.fst doubleFree_MemL_aspic.fst |