Support for C++ in GMC
| Thesis title in Czech: | Support for C++ in GMC |
|---|---|
| Thesis title in English: | Support for C++ in GMC |
| Key words: | formální verifikace, C++, GMC |
| English key words: | formal verification, C++, GMC |
| Academic year of topic announcement: | 2011/2012 |
| Thesis type: | diploma thesis |
| Thesis language: | angličtina |
| Department: | Department of Distributed and Dependable Systems (32-KDSS) |
| Supervisor: | doc. RNDr. Jan Kofroň, Ph.D. |
| Author: | hidden - assigned and confirmed by the Study Dept. |
| Date of registration: | 07.11.2011 |
| Date of assignment: | 07.11.2011 |
| Confirmed by Study dept. on: | 07.12.2011 |
| Date and time of defence: | 09.09.2013 00:00 |
| Date of electronic submission: | 29.07.2013 |
| Date of submission of printed version: | 02.08.2013 |
| Date of proceeded defence: | 09.09.2013 |
| Opponents: | doc. RNDr. Petr Hnětynka, Ph.D. |
| Guidelines |
| GMC is a software model checker for the C language. It is based on GIMPLE, which is used as the intermediate representation of C programs in GCC. The goal of the thesis is to extend GMC with a basic support for the C++ language, in particular including handling of classes (constructors, destructors, inheritance and virtual methods) and, if it will turn out to be necessary for it, also exceptions. As an optional task, also support for other C++ features, such as templates, will be a welcome contribution. As a part of the thesis, the student should also demonstrate the achieved results on a set of examples showing usability of the solution. |
| References |
| [1] GIMPLE, http://gcc.gnu.org/onlinedocs/gccint/GIMPLE.html
[2] GCC, http://gcc.gnu.org/ [3] GMC, http://d3s.mff.cuni.cz/~sery/gmc/ [4] Jan Kouba: Memory Representation for Model Checker of C/C++, MSc. thesis, Charles University in Prague, 2010 [5] Ondrej Krc-Jediny: GIMPLE Model Checker, MSc. thesis, Charles University in Prague, 2011 |