Игнорировать ассемблерный код в анализе значений и резервный код

Question

Я попытаюсь использовать анализ стоимости проекта в C, но этот проект содержит некоторые .c файл, где мы можем найти код ассемблера. Когда я пытаюсь запустить frama-C для этих файлов, я получаю сообщение об ошибке в коде сборки.

Код ассемблера разработан для Motorola 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

Answer 1

Frama-C не обрабатывает ассемблерный код. Может разбирать некоторые встроенные сборки (gcc"s asm(...) инструкция), но не целый файл. Вы должны попытаться выяснить, что PERMUTE Процедура выполняет и обеспечивает замену, либо с простым определением C, либо в виде прототипа + спецификации ACSL (первое предпочтительнее, если вы собираетесь использовать Value Analysis).

-machdep не позволит Frama-C интерпретировать любой ассемблерный код. Этот параметр в основном фиксирует размер стандартных целочисленных типов (например, 32-битный для int) и их представление (big или little endian). Если вам нужна поддержка конкретной архитектуры, которая не включена в поддерживаемую в настоящее время (как показано на frama-c -machdep help), вам действительно следует обратиться в службу поддержки Frama-C, чтобы узнать, при каких условиях это можно добавить.

В графическом пользовательском интерфейсе Value Analysis покажет вам код, который недоступен с точки входа анализа, как выделенный и на красном фоне. Также возможно написать скрипт / плагин, который бы программно извлекал эту информацию, но в дистрибутиве нет ничего для этого.