Sākums Izpētīt Palīdzība
Reģistrēties Pierakstīties
liyuezong
/
SmartPDCode
Vērot 2
Pievienot zvaigznīti 0
Atdalīts 0
Faili Problēmas 0 Izmaiņu pieprasījumi 0 Vikivietne
Koks: ef7d8de18d
Atzari Tagi
SmartPDCode
/
GD32F427
/
rtos
/
coreJSON
/
test
/
cbmc
/
proofs
/
multiSearch
liyi f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 4 dienas atpakaļ
..
Makefile f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 4 dienas atpakaļ
README.md f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 4 dienas atpakaļ
cbmc-proof.txt f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 4 dienas atpakaļ
cbmc-viewer.json f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 4 dienas atpakaļ
multiSearch_harness.c f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 4 dienas atpakaļ

README.md

multiSearch proof

This directory contains a memory safety proof for multiSearch. 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.

  • arraySearch;
  • objectSearch;
  • skipDigits.

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.