Rinspect 是一种建立在流行的 Clang/LLVM 编译器框架之上的工具，用于处理为 Linux/PThreads 平台编写的 C 代码。 它可以支持顺序存储模型、全存储顺序存储模型和部分存储顺序存储模型。
建筑学
Rinspect 基于犹他大学正式验证小组开发的检查项目。 它采用相同的服务器/客户端架构。 基本上，该项目附带了一个经过修改的 LLVM，以编译/指示带有附加组件的待验证源代码。 然后，待验证程序能够通过 Unix 域套接字与称为调度程序的验证程序进行通信。 调度器通过该通信通道控制执行轨迹并收集待测程序的执行历史。 然后使用我们在 PLDI 2015 上开发的算法，调度程序能够报告由宽松内存模型引起的正在验证的源代码的错误。
项目目录结构
源文件
垃圾桶
拍
inspect-0.3（我们的主要源代码）
llvm-3.0.src（修改后的LLVM）
smt_dp
