SmartRocket DDC工具，是专为C/C++设计的动静态代码分析工具，采用形式化验证技术提前识别除零、移位、空指针解引用、数组越界、数据溢出、未赋值使用、共享变量冲突、不可达代码等多类型的动态缺陷，支持MISRA等国际编码规范进行代码合规扫描，提供精准错误定位和修复建议，显著缩短修复周期，降低风险成本。工具推出的运行时缺陷检测功能模块标志着国内代码质量保障从“被动检测”转向“主动预防”，为高可靠性软件开发与测试提供形式化验证领域有效的工业级解决方案。
客户试用申请
聚焦代码中所有算术与浮点运算，通过区间抽象与约束求解，穷举变量在全部合法取值范围内的运算结果，系统化排除因数据极端值引发的计算异常。
全面接管内存访问与多线程交互的校验工作，将指针、数组、堆栈变量及共享资源纳入统一的形式化分析模型，杜绝内存污染与线程失控。
内建主流行业编码规范引擎，在检测缺陷的同时对代码的可读性、可维护性与逻辑合理性进行自动化评审，辅助团队建立统一的代码审美与安全基线。
在单元测试执行前，即可系统化识别90%以上的运行时缺陷，将错误发现节点大幅前移;有效降低后期调试与返工成本，综合节省50%以上的缺陷修复开销。真正实现质量保障从“被动响应式测试”向“主动证明式预防”的范式转变，契合DevOps与功能安全标准中“安全左移”的先进理念。
基于抽象解释与定理证明的数学严谨性，工具输出的每一条缺陷报告均对应一条真实可触发的执行路径，并:提供具体输入样例以供复现。彻底规避传统静态工具常见的“误报海啸"问题，帮助团队将有限人力聚焦于真实风险，杜绝无效排查带来的时间损耗。
支持深度集成于SmartRocketTestGrid嵌入式软件自动化测试平台，实现从静态规则扫描一运行时缺陷检测一单元测试一集成测试一目标机测试的全流程闭环验证。一套工具链覆盖代码合规度量、错误路径穷举、并发竞态分析、控制流/数据流审计等多个维度，减少多工具切换带来的集成成本与学习负担。
支持根据项目实际需求，定制化生成多格式、多维度报告(Word/PDF/HTML/Excel)，满足不同评审场景（代码审查、适航取证、客户交付）。提供开放规则配置接口，允许用户启用/关闭特定缺陷类型检测、调整告警严重性分级，精细适配企业既有编码规范体系。
