Doxygen for test gen support

.gitignore

@@ -12,6 +12,8 @@ src/goto-analyzer/taint_driver_scripts/.idea/*
 /*.files
 /*.includes
 
+*.pyc
+
 # compilation files
 *.lo
 *.od
@@ -68,6 +70,10 @@ src/xmllang/xml_lex.yy.cpp
 src/xmllang/xml_y.output
 src/xmllang/xml_y.tab.cpp
 src/xmllang/xml_y.tab.h
+src/memory-models/mm_lex.yy.cpp
+src/memory-models/mm_y.output
+src/memory-models/mm_y.tab.cpp
+src/memory-models/mm_y.tab.h
 
 # binaries
 src/cbmc/cbmc

scripts/compare_postprocessor_output.py

@@ -0,0 +1,99 @@
+import difflib, argparse, subprocess, sys, os, multiprocessing, itertools
+
+
+def preprocess(compiler, file_contents):
+    """ Get output from the preprocessing pass on a file.  """
+    output = subprocess.Popen(
+            [compiler, '-E', '-'],
+            stdout=subprocess.PIPE,
+            stderr=subprocess.PIPE,
+            stdin=subprocess.PIPE).communicate(input=file_contents)[0]
+
+    def should_keep(line):
+        return str.strip(line) and line[0] != '#'
+
+    return filter(should_keep, output.splitlines())
+
+
+def preprocess_file(compiler, filename):
+    """ Open a file and get the preprocessor output.  """
+    with open(filename, 'rb') as f:
+        return preprocess(compiler, f.read())
+
+
+def file_contents_from_branch(filename, branch):
+    """ Get a copy of a file from another branch and return its contents.  """
+    return subprocess.check_output(
+            ['git', 'show', '%s:%s' % (branch, filename)])
+
+
+def equal_to_file_on_branch(filename, branch, compiler):
+    """
+    Open a file on this branch and preprocess it.  Preprocess the same file
+    from another branch, and return a diff.
+    """
+    with open(filename, 'rb') as f:
+        def p(text):
+            return preprocess(compiler, text)
+        return difflib.unified_diff(p(f.read()),
+                p(file_contents_from_branch(filename, branch)),
+                fromfile=filename,
+                tofile=filename,
+                lineterm='')
+
+
+def is_source(filename):
+    """ Return whether the file appears to be a C++ source file.  """
+    _, ext = os.path.splitext(filename)
+    return ext == '.h' or ext == '.cpp'
+
+
+def process(tup):
+    """
+    Check a single file, and return its name if the check fails, otherwise
+    return None.
+    """
+    filename, branch, compiler = tup
+    failed = '\n'.join(equal_to_file_on_branch(filename, branch, compiler))
+    return failed if failed else None
+
+
+def main():
+    """
+    Open a file and compare its preprocessor output to the output from the same
+    file on a different branch.  Return 0 if the outputs match, or 1 otherwise.
+    """
+    parser = argparse.ArgumentParser()
+    parser.add_argument(
+            '--branch', type=str, default='upstream/master',
+            help='The branch to compare')
+    parser.add_argument(
+            '--compiler', type=str, default='g++',
+            help='The compiler to use')
+    args = parser.parse_args()
+
+    all_files = [os.path.join(root, file)
+            for root, _, files in os.walk('.') for file in files]
+    source_files = filter(is_source, all_files)
+
+    zipped = zip(
+            source_files,
+            itertools.cycle([args.branch]),
+            itertools.cycle([args.compiler]))
+
+    pool = multiprocessing.Pool(10)
+
+    results = filter(None, pool.map(process, zipped))
+
+    pool.close()
+    pool.join()
+
+    if results:
+        print('\n\n'.join(results))
+        return 1
+
+    return 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())

scripts/do_doc_convert.py

@@ -0,0 +1,40 @@
+from reformat_docs import convert_file
+from os import walk
+from os.path import join
+from sys import exit
+from re import match
+
+"""
+Run this from CBMC's top-level directory.
+"""
+
+def main():
+    IGNORE_LIST = [
+            r'src/big-int/.*',
+            r'src/miniz/.*',
+            r'src/ansi-c/arm_builtin_headers.h',
+            r'src/ansi-c/clang_builtin_headers.h',
+            r'src/ansi-c/cw_builtin_headers.h',
+            r'src/ansi-c/gcc_builtin_headers_alpha.h',
+            r'src/ansi-c/gcc_builtin_headers_arm.h',
+            r'src/ansi-c/gcc_builtin_headers_generic.h',
+            r'src/ansi-c/gcc_builtin_headers_ia32-2.h',
+            r'src/ansi-c/gcc_builtin_headers_ia32.h',
+            r'src/ansi-c/gcc_builtin_headers_mips.h',
+            r'src/ansi-c/gcc_builtin_headers_power.h',
+            r'src/ansi-c/library/cprover.h']
+
+    MATCH_EXPR = r'.*\.(h|cpp)'
+
+    for root, dirs, files in walk('src'):
+        for file in files:
+            path = join(root, file)
+            if any(map(lambda x: match(x, path), IGNORE_LIST)):
+                print 'ignoring', path
+                continue
+            if not match(MATCH_EXPR, path):
+                continue
+            convert_file(path, True)
+
+if __name__ == '__main__':
+    exit(main())