1.Recently, I am studying how to use Coq to prove the security of the code, and whether I can recommend some documents or materials. thank you very much.
2.Does Coq have a plugin for translating source code into HOL?
for eample。Memory leak security issue。
char p = (char)malloc(100 * sizeof(char));
p = (char*)malloc(50 * sizeof(char));
p = NULL;