tools/verification/rvgen/dot2c
Source file repositories/reference/linux-study-clean/tools/verification/rvgen/dot2c
File Facts
- System
- Linux kernel
- Corpus path
tools/verification/rvgen/dot2c- Extension
[no extension]- Size
- 928 bytes
- Lines
- 26
- Domain
- Support Tooling And Documentation
- Bucket
- tools
- Inferred role
- Support Tooling And Documentation: tools
- Status
- atlas-only
Why This File Exists
Repository support layer: documentation, build tooling, samples, user-space helper tools, generated initramfs support, licenses, and validation utilities.
- Repository support layer: documentation, build tooling, samples, user-space helper tools, generated initramfs support, licenses, and validation utilities.
Dependency Surface
- No C-style include directives detected by the generator.
Detected Declarations
- No top-level syscall, struct, function, initcall, or export declaration detected by the generator.
Annotated Snippet
#!/usr/bin/env python3
# SPDX-License-Identifier: GPL-2.0-only
#
# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org>
#
# dot2c: parse an automata in dot file digraph format into a C
#
# This program was written in the development of this paper:
# de Oliveira, D. B. and Cucinotta, T. and de Oliveira, R. S.
# "Efficient Formal Verification for the Linux Kernel." International
# Conference on Software Engineering and Formal Methods. Springer, Cham, 2019.
#
# For further information, see:
# Documentation/trace/rv/deterministic_automata.rst
if __name__ == '__main__':
from rvgen import dot2c
import argparse
parser = argparse.ArgumentParser(description='dot2c: converts a .dot file into a C structure')
parser.add_argument('dot_file', help='The dot file to be converted')
args = parser.parse_args()
d = dot2c.Dot2c(args.dot_file)
d.print_model_classic()
Annotation
- Atlas domain: Support Tooling And Documentation / tools.
- Implementation status: atlas-only.
Implementation Notes
- This generated page is the file-by-file coverage layer; curated subsystem chapters should link here when they synthesize a multi-file control flow.
- Core OS pages should be promoted from atlas-only to deep-reviewed when they explain data structures, invariants, locking, lifecycle, and C implementation snippets.
- Driver-family pages are intentionally pattern-oriented unless they are part of the selected PCIe/NVMe representative device path.