@article{YANG Ping:17, author = {YANG Ping, WANG Sheng-yuan}, title = {Analysis of Target Code Generation Mechanism of CompCert Compiler}, publisher = {Computer Science}, year = {2020}, journal = {Computer Science}, volume = {47}, number = {9}, eid = {17}, numpages = {6}, pages = {17}, keywords = {CompCert;Formally Verified compilers;Target code generation;Compiler retargeting}, url = {https://www.jsjkx.com/EN/abstract/article_19337.shtml}, doi = {10.11896/jsjkx.200400018} }