文件名称:verker:Linux内核库功能已正式验证
文件大小:199KB
文件格式:ZIP
更新时间:2024-06-11 08:37:00
linux-kernel verification formal-verification acsl frama-c
威客 要以俄语查看此文件,请点击。 该存储库包含Linux内核功能的ACSL规范。 该项目的目的是对Linux内核库功能进行形式验证。 文件 [ ] 证明状态 ID 功能 地位 逻辑功能 libfuzzer 评论 1个 check_bytes8 证明了 证明了 是的 2个 match_string 证明了 不需要 3 记忆力 证明了 是的 4 记忆体 证明了 是的 5 记忆扫描 证明了 不需要 是的 6 skip_spaces 证明了 证明了 是的 要求太严格了(删除strlen) 7 strcasecmp 证明了 是的 8 strcat 证明了 不需要 usr strcmp确保 9 strchr 证明了 证明了 是的 10 Strchrnul 证明了 证明了 是的 11 strcmp 证明了 证明了 是的 12 strcpy