Modify prepare.py to apply patch files and modify headers in place.
@@ -28,7 +28,6 @@ import sys
import textwrap
from subprocess import CalledProcessError
-
from make_common_makefile import main as make_common_file
from make_configuration_directories import main as process_configurations
from make_proof_makefiles import main as make_proof_files
@@ -40,13 +39,47 @@ sys.path.append(os.path.normpath(os.path.join(CWD, "..", "patches")))
#from compute_patch import create_patches
#from compute_patch import DirtyGitError
#from compute_patch import PatchCreationError
-#from patches_constants import HEADERS
+from patches_constants import HEADERS
-PROOFS_DIR = os.path.dirname(os.path.abspath(__file__))
+from compute_patch import find_all_defines
+from compute_patch import manipulate_headerfile
+
+import patch
+PROOFS_DIR = os.path.dirname(os.path.abspath(__file__))
LOGGER = logging.getLogger("PrepareLogger")
+################################################################
+
+def patch_headers(headers):
+ """Patch headers so we can define symbols on the command line.
+
+ When building for CBMC, it is convenient to define symbols on the
+ command line and know that these definitions will override the
+ definitions of the same symbols in header files.
+
+ The create_patches function takes a list of header files, searches
+ the Makefile.json files for symbols that will be defined in the
+ Makefiles, and creates patch files that protect the definition of
+ those symbols in header files with #ifndef/#endif. In this way,
+ command line definitions will override header file definitions.
+
+ The create_patches function, however, depends on the fact that all
+ header files being modified are included in the top-level git
+ repository. This assumption is violated if header files live in
+ submodules.
+
+ This function just updates the header files in place without
+ creating patch files. One potential vulnerability of this
+ function is that it could cause preexisting patch files to fail if
+ they patch a file being modified here.
+ """
+ defines = find_all_defines()
+ for header in headers:
+ manipulate_headerfile(defines, header)
+
+################################################################
def build():
process_configurations()
@@ -61,6 +94,10 @@ def build():
""".format(str(e))))
exit(1)
+ # Patch headers directly instead of creating patch files.
+ patch.patch()
+ patch_headers(HEADERS)
+
#try:
# create_patches(HEADERS)
#except (DirtyGitError, PatchCreationError) as e:
@@ -70,6 +107,7 @@ def build():
# """.format(str(e))))
# exit(1)
+################################################################
if __name__ == '__main__':
logging.basicConfig(format="{script}: %(levelname)s %(message)s".format(
