On the Use of Underspecified Data-Type Semantics for Type Safety in Low-Level Code
| Autor: | Tjark Weber, Marcus Völp, Hendrik Tews |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2012 |
| Předmět: | |
| Zdroj: | Electronic Proceedings in Theoretical Computer Science, Vol 102, Iss Proc. SSV 2012, Pp 73-87 (2012) |
| Druh dokumentu: | article |
| ISSN: | 2075-2180 67047653 |
| DOI: | 10.4204/EPTCS.102.8 |
| Popis: | In recent projects on operating-system verification, C and C++ data types are often formalized using a semantics that does not fully specify the precise byte encoding of objects. It is well-known that such an underspecified data-type semantics can be used to detect certain kinds of type errors. In general, however, underspecified data-type semantics are unsound: they assign well-defined meaning to programs that have undefined behavior according to the C and C++ language standards. A precise characterization of the type-correctness properties that can be enforced with underspecified data-type semantics is still missing. In this paper, we identify strengths and weaknesses of underspecified data-type semantics for ensuring type safety of low-level systems code. We prove sufficient conditions to detect certain classes of type errors and, finally, identify a trade-off between the complexity of underspecified data-type semantics and their type-checking capabilities. |
| Databáze: | Directory of Open Access Journals |
| Externí odkaz: |
|