基于 klee 探索 限制条件下的 c 代码 生成 1. 介绍 本项目目的是编写一个能够用klee驱动执行的sysy代码生成器，用于生成符合sysy语法规范的代码，以便于测试sysy编译器的正确性。 使用klee执行使用符号量作为驱动数据的sysy代码生成器,是希望能够探索到更多合法的生成路径,希望生成在约束条件下(比如深度,循环次数等)的所有可执行路径,以生成符合约束条件的sysy代码. Try # 准备klee环境 docker compose up -d # 进入klee环境 ./enter.sh # 运行生成 ./build.sh