• Nessuna parola chiave trovata

Nella presente tesi di laurea viene proposto un approccio per la generazione
automatica di test per programmi C/C++ che si basa sulla programmazione logica
con vincoli, integrato nell'analizzatore di programmi ECLAIR. In prima istanza,
viene chiarito il ruolo dei comportamenti indefinti nei linguaggi di
programmazione. Successivamente vengono descritti i principali criteri di
copertura definiti in letteratura. Infine, si descrive il processo di
generazione automatica di test. Si chiarisce il ruolo della forma SSA e come
questa venga calcolata dinamicamente. Si passa poi alla valutazione delle
espressioni e alla relativa gestione dei comportamenti indefiniti. Viene poi
trattata la gestione degli operatori bitwise e la successiva integrazione del
generatore di test nell'analizzatore ECLAIR. Infine si illustrano le principali
tecniche per risolvere i problemi CLP(FD): oltre alla propagazione ed al
labeling, viene descritta la tecnica della Dynamic Linear Relaxation,
proposta da Arnaud Gotlieb.