def check_uid_uniqueness()

in template-for-repository/proofs/run-cbmc-proofs.py [0:0]

• 19 lines of code
• 4 McCabe index (conditional complexity)

def check_uid_uniqueness(proof_dir, proof_uids):
    with (pathlib.Path(proof_dir) / "Makefile").open() as handle:
        for line in handle:
            m = re.match(r"^PROOF_UID\s*=\s*(?P<uid>\w+)", line)
            if not m:
                continue
            if m["uid"] not in proof_uids:
                proof_uids[m["uid"]] = proof_dir
                return

            logging.critical(
                "The Makefile in directory '%s' should have a different "
                "PROOF_UID than the Makefile in directory '%s'",
                proof_dir, proof_uids[m["uid"]])
            sys.exit(1)

    logging.critical(
        "The Makefile in directory '%s' should contain a line like", proof_dir)
    logging.critical("PROOF_UID = ...")
    logging.critical("with a unique identifier for the proof.")
    sys.exit(1)