Στατική ανάλυση προγραμμάτων της C: προβλήματα, μέθοδοι και εργαλεία:
Creators: name: Χατζηελευθερίου, Γεώργιος Νικολάου
Publisher: name: Aristotle University of Thessaloniki
Year: 2009
Subjects: Στατική ανάλυση
Επαλήθευση λογισμικού
Γλώσσα προγραμματισμού C
Static analysis
Program verification
C programming language

description: Η επαλήθευση λογισμικού με τη χρήση της στατικής ανάλυσης είναι η διαδικασία ανίχνευσης σφαλμάτων εκτέλεσης σε προγράμματα σε χρόνο μεταγλώττισης, δηλαδή χωρίς τα προγράμματα να εκτελεστούν. Πολλά εργαλεία στατικής ανάλυσης, ελεύθερα αλλά και εμπορικά, έχουν αναπτυχθεί την τελευταία δεκαετία, πολλά από τα οποία στοχεύουν στην επίλυση προβλημάτων για προγράμματα γραμμένα στη γλώσσα προγραμματισμού C. Στόχος της εργασίας είναι η καταγραφή των προβλημάτων τα οποία μπορούν να εντοπιστούν από τα εργαλεία στατικής ανάλυσης και η αξιολόγηση της αποτελεσματικότητας και της αποδοτικότητας τους με τη χρήση ποιοτικών και ποσοτικών δεδομένων. Η εργασία αποτελείται από έντεκα σαφώς διαχωρισμένες ενότητες. Στην ενότητα 1 γίνεται μια εισαγωγή για τα κίνητρα και τους στόχους της εργασίας. Στην ενότητα 2 παρουσιάζονται οι εγγενείς αδυναμίες της γλώσσας προγραμματισμού και τα λάθη που υπάρχουν συνήθως σε προγράμματα που έχουν γραφεί στη συγκεκριμένη γλώσσα. Στην ενότητα 3 γίνεται η παρουσίαση των μεθόδων στατικής ανάλυσης αλλά κυρίως παρουσιάζονται τα εργαλεία στατικής ανάλυσης τα οποία χρησιμοποιήθηκαν στην εργασία μας. Στην ενότητα 4 παρουσιάζονται τα λάθη τα οποία μπορούν τα εργαλεία στατικής ανάλυσης να εντοπίσουν στα προγράμματα της C με βάση τα αποτελέσματα από την μελέτη μας. Στην ενότητα 5 περιγράφεται η αποτελεσματικότητα των εργαλείων να εντοπίζουν σφάλματα σε τμήματα κώδικα τα οποία απαιτούν ανάλυση με υψηλό επίπεδο ακρίβειας. Η ενότητα 6 περιλαμβάνει τις ποσοτικές μετρήσεις για την αποτελεσματικότητα των εργαλείων στατικής ανάλυσης με βάση γνωστές μετρικές αξιολόγησης. Στην ενότητα 7 παρουσιάζονται αποτελέσματα που αφορούν την αποδοτικότητα των εργαλείων σε ότι αφορά το χρόνο εκτέλεσης και τις απαιτήσεις σε μνήμη. Στην ενότητα 8 περιγράφονται οι δυνατότητες επεκτασιμότητας κάθε εξεταζόμενου εργαλείου στατικής ανάλυσης. Η ενότητα 9 περιέχει τα συμπεράσματα της εργασίας και η ενότητα 10 κάποιες χρήσιμες αναφορές στη βιβλιογραφία και σε άρθρα από επιστημονικά περιοδικά και συνέδρια. Τέλος, στο Παράρτημα επισυνάπτεται όλος ο πηγαίος κώδικας των προγραμμάτων που δημιουργήθηκαν αποκλειστικά και μόνο για τους σκοπούς της συγκεκριμένης εργασίας.
description: Program verification with the use of static analysis is the procedure of the detection of run-time errors in programs at compile time, thus without executing them. A large number of static analysis tools, both commercial and publicly-available, emerged in the last decade and many of them focus on the detection of defects in programs written in C programming language. The main objective of this thesis is the presentation of the defects which static analysis tools are able to detect and the evaluation of their effectiveness and efficiency with the use of qualitative and quantitative data. There exist eleven separate sections in this thesis. In section 1, an introduction is done for the motivation and the objectives of the study. In section 2, we present the unsafe features of C programming language and the defects which usually exist in programs written in this language. In section 3, we present the methods of static analysis and the static analysis tools which have been used in our study. In section 4, we present the errors that the static analysis tools are able to detect in C programs, based on the results of our research. In section 5, we describe the effectiveness of the static analysis tools in the detection of errors in code fragments which require a high level of analysis sensitivity. Section 6 includes the quantitative measurements for the effectiveness of the static analysis tools based on known evaluation metrics. In section 7, we present the results of our research related to the efficiency of static analysis tools, with respect to execution time and memory consumption. In section 8, we describe the extensibility capabilities of each examined static analysis tool. Section 9 includes the conclusions and in section 10 we cite some useful references to books and articles from scientific journals and conferences. Last, in the Appendix we attach the whole source code of the programs developed for the purposes of our study.