Gate Synthesis for C Programs with Heap
- Byron Cook ,
- Ashutosh Gupta ,
- Satnam Singh ,
- Viktor Vafeiadis
Draft under submission. |
Published by IEEE Computer Society
Current C to gates synthesis tools do not support programs that make non-trivial use of dynamically-allocated heap (e.g. linked-list C programs that call malloc and free). The problem is that its difficult to determine an a priori bound on the amount of heap used during the program’s execution, if a bound even exists. In this paper we develop a new method of synthesizing symbolic bounds expressed over generic parameters, thus leading to a C to gates synthesis fow for programs using dynamic allocation and deallocation.
Copyright © 2007 IEEE. Reprinted from IEEE Computer Society.This material is posted here with permission of the IEEE. Internal or personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution must be obtained from the IEEE by writing to pubs-permissions@ieee.org.By choosing to view this document, you agree to all provisions of the copyright laws protecting it.