Inicio Explorar Ayuda
Registro Iniciar sesión
liyuezong
/
SmartPDCode
Seguir 2
Destacar 0
Fork 0
Archivos Incidencias 0 Pull Requests 0 Wiki
Árbol: ef7d8de18d
Ramas Etiquetas
SmartPDCode
/
GD32F427
/
rtos
/
coreJSON
/
test
/
cbmc
/
proofs
/
objectSearch
liyi f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hace 4 días
..
Makefile f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hace 4 días
README.md f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hace 4 días
cbmc-proof.txt f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hace 4 días
cbmc-viewer.json f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hace 4 días
objectSearch_harness.c f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hace 4 días

README.md

objectSearch proof

This directory contains a memory safety proof for objectSearch. The proof runs in a few seconds and provides 100% coverage.

For this proof, the following functions are replaced with function contracts. These functions have separate proofs.

  • skipAnyScalar;
  • skipCollection;
  • skipSpace;
  • skipString.

To run the proof.

  • Add cbmc, goto-cc, goto-instrument, goto-analyzer, and cbmc-viewer to your path;
  • Run make;
  • Open html/index.html in a web browser.