使用机器检查进行 AVR 微控制器机器代码验证

本 Crate 中的可执行文件允许通过 machine-check 对 AVR ATmega328P 微控制器的机器代码程序进行形式验证。

除了常见的 machine-check 可执行文件参数外，该可执行文件还接受一对参数，用于指定包含 ATmega328P 程序代码的 Intel HEX 文件的路径：--hex-file abc.hex。

有关验证规范的详细信息，请参阅 machine-check。

请注意，machine-check 和本 Crate 目前均为实验性质，正在等待进一步的改进和稳定。

已知系统问题

• 一些较少使用的指令尚未实现。
• 仅支持通用 I/O 外设。
• 程序计数器不总是检查溢出。

固有恐慌

• 程序内存外的跳转和调用。
• 执行保留或非法指令。
• 非法或不推荐的读写操作。
• 在数据内存外读取或写入时推送、弹出、调用和返回。
• 未实现指令、读取和写入。

使用的资源

该系统使用官方的 AVR 指令集手册 和 非汽车 ATmega328P 数据手册 编写。

许可证

根据您的选择，受 Apache License 2.0 或 MIT 许可证的许可。除非您明确声明，否则您有意提交给本 Crate 的任何贡献，根据 Apache-2.0 许可证定义，应按照上述方式双重许可，不附加任何额外的条款或条件。