0

我将尝试在 C 中的一个项目上使用值分析，但该项目包含一些.c文件，我们可以在其中找到汇编代码。当我尝试在这些文件上启动 frama-C 时，汇编代码出现错误。

汇编代码是为摩托罗拉68040设计的，我在文档中看到，我需要使用选项-machdep来更改模块的分析平台，但是这个平台没有定义，所以我需要联系支持还是可以我将模块配置为忽略汇编代码？

第二个问题，关于 SpareCode 模块。我们可以配置模块，只查看死代码并保留备用代码（在过程的情况下）吗？

otherfile.c 的代码（无注释）：

#pragma asm

     XDEF _CONVERSION_INTEL

MESSAGE     SET 20
NB_CARAC    SET 26

     SECTION mc3_sys_code

_CONVERSION_INTEL
    movem.l d1-d3/a0,-(sp)
    move.l  MESSAGE(sp),a0
    moveq   #0,d1 
    move.w  NB_CARAC(sp),d1
    moveq   #0,d3

 PERMUTE:
    move.w  (a0),d2
    rol.w   #8,d2
    move.w  d2,(a0)
    addq.l  #2,a0
    addq.l  #2,d3
    cmp.l   d3,d1
    bgt PERMUTE test
    movem.l (sp)+,d1-d3/a0
    rts

#pragma endasm
4

1 回答 1

4

Frama-C 不处理汇编代码。它可以解析一些内联汇编（gcc'sasm(...)指令），但不能解析整个文件。您应该尝试弄清楚该PERMUTE过程在做什么并提供替换，无论是使用普通 C 定义还是作为原型 + ACSL 规范（如果您打算使用价值分析，前者更可取）。

-machdep不会让 Frama-C 解释任何汇编代码。此选项主要修复标准整数类型的大小（例如 32 位int）及其表示形式（大端或小端）。如果您需要对当前支持的架构中未包含的特定架构的支持（如 所示frama-c -machdep help），您确实应该联系 Frama-C 的支持人员，看看在什么条件下可以添加。

在图形用户界面中，价值分析将向您显示从分析的入口点无法访问的代码，并在红色背景上划掉。也可以编写一个脚本/插件以编程方式提取此信息，但分发中没有任何内容。

于 2014-05-26T15:30:00.163 回答