Inicio Explorar Axuda
Rexistro Iniciar sesión
liyuezong
/
SmartPDCode
Seguir 2
Destacar 0
Fork 0
Ficheiros Incidencias 0 Pull Requests 0 Wiki
Árbore: f162b98f4f
Ramas Etiquetas
SmartPDCode
/
GD32F427
/
rtos
/
coreHTTP
/
test
/
cbmc
/
proofs
liyi f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hai 4 días
..
HTTPClient_AddHeader f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hai 4 días
HTTPClient_AddRangeHeader f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hai 4 días
HTTPClient_InitializeRequestHeaders f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hai 4 días
HTTPClient_ReadHeader f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hai 4 días
HTTPClient_Send f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hai 4 días
HTTPClient_strerror f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hai 4 días
findHeaderFieldParserCallback f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hai 4 días
findHeaderOnHeaderCompleteCallback f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hai 4 días
findHeaderValueParserCallback f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hai 4 días
httpParserOnBodyCallback f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hai 4 días
httpParserOnHeaderFieldCallback f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hai 4 días
httpParserOnHeaderValueCallback f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hai 4 días
httpParserOnHeadersCompleteCallback f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hai 4 días
httpParserOnMessageBeginCallback f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hai 4 días
httpParserOnMessageCompleteCallback f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hai 4 días
httpParserOnStatusCallback f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hai 4 días
httpParserOnStatusCompleteCallback f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hai 4 días
lib f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hai 4 días
Makefile-project-defines f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hai 4 días
Makefile-project-targets f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hai 4 días
Makefile-project-testing f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hai 4 días
Makefile-template-defines f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hai 4 días
Makefile.common f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hai 4 días
README.md f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hai 4 días
run-cbmc-proofs.py f162b98f4f GD32F427 更换系统由RT_thread 替换为FreeRTOS 。解决北向串口100ms通信延迟问题。 hai 4 días

README.md

CBMC proofs

This directory contains the CBMC proofs. Each proof is in its own directory.

This directory includes four Makefiles.

One Makefile describes the basic workflow for building and running proofs:

  • Makefile.common:
    • make: builds the goto binary, does the cbmc property checking and coverage checking, and builds the final report.
    • make goto: builds the goto binary
    • make result: does cbmc property checking
    • make coverage: does cbmc coverage checking
    • make report: builds the final report

Three included Makefiles describe project-specific settings and can override definitions in Makefile.common:

  • Makefile-project-defines: definitions like compiler flags required to build the goto binaries, and definitions to override definitions in Makefile.common.
  • Makefile-project-targets: other make targets needed for the project
  • Makefile-project-testing: other definitions and targets needed for unit testing or continuous integration.