Compiling C and C++ Programs for Dynamic White-Box Analysis

BARANOVÁ, Zuzana and Petr ROČKAI. Compiling C and C++ Programs for Dynamic White-Box Analysis. In Nelma Moreira and Emil Sekerinski. Workshop on Practical Formal Verification for Software Dependability (AFFORD 2019). Cham: Springer International Publishing, 2020, p. 30-45. ISBN 978-3-030-54993-0. Available from: https://dx.doi.org/10.1007/978-3-030-54994-7_4.

Basic information

Original name

Compiling C and C++ Programs for Dynamic White-Box Analysis

Authors

BARANOVÁ, Zuzana (703 Slovakia, belonging to the institution) and Petr ROČKAI (703 Slovakia, belonging to the institution)

Edition

Cham, Workshop on Practical Formal Verification for Software Dependability (AFFORD 2019), p. 30-45, 16 pp. 2020

Publisher

Springer International Publishing

---

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Switzerland

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

printed version "print"

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/20:00115150

Organization unit

Faculty of Informatics

ISBN

978-3-030-54993-0

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-54994-7_4

Keywords in English

DIVINE; automated compilation; formal verification; model checking; C; C++

Tags

International impact, Reviewed

---

Abstract

V originále

Building software packages from source is a complex and highly technical process. For this reason, most software comes with build instructions which have both a human-readable and an executable component. The latter in turn requires substantial infrastructure, which helps software authors deal with two major sources of complexity: first, generation and management of various build artefacts and their dependencies, and second, the differences between platforms, compiler toolchains and build environments. This poses a significant problem for white-box analysis tools, which often require that the source code of the program under test is compiled into an intermediate format, like the LLVM IR. In this paper, we present divcc, a drop-in replacement for C and C++ compilation tools which transparently fits into existing build tools and software deployment solutions. Additionally, divcc generates intermediate and native code in a single pass, ensuring that the final executable is built from the intermediate code that is being analysed.