We present a refined segmentation abstract domain for the analysis of strings in the C programming language, properly extending the parametric segmentation approach to array representation introduced by P. Cousot et al. to the case of text values. In particular, we capture the so-called string of interest of an array of char, in order to distinguish well-formed string arrays. A concrete and abstract semantics of the main C header file string.h functions are worked out in full detail.

M-String Segmentation: A Refined Abstract Domain for String Analysis in C Programs

Agostino Cortesi;OLLIARO, MARTINA
2018

Abstract

We present a refined segmentation abstract domain for the analysis of strings in the C programming language, properly extending the parametric segmentation approach to array representation introduced by P. Cousot et al. to the case of text values. In particular, we capture the so-called string of interest of an array of char, in order to distinguish well-formed string arrays. A concrete and abstract semantics of the main C header file string.h functions are worked out in full detail.
Proceedings of the IEEE 12th International Symposium on Theoretical Aspects of Software Engineering TASE 2018
File in questo prodotto:
File Dimensione Formato  
Tase2018_Olliaro.pdf

non disponibili

Descrizione: preprint TASE
Tipologia: Documento in Pre-print
Licenza: Accesso gratuito (solo visione)
Dimensione 204.74 kB
Formato Adobe PDF
204.74 kB Adobe PDF   Visualizza/Apri

I documenti in ARCA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/10278/3708312
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 9
  • ???jsp.display-item.citation.isi??? 3
social impact