Ignore the assembler code in value analysis and sparecode

I will try to use the value analysis on a project in C, but this project contains some .c file where we can find assembler code. When I try to launch frama-C on these files, I get an error on the assembly code.

The assembler code is desgned for Motorola 68040, I have seen in the documentation, that I need to use the option -machdep to change the analysis platform for the module, but this platform isn't defined, so do I need to contact the support or can I configure the module to ignore the assembler code?

And a second question, on SpareCode module. Can we configure the module, to just see the dead code and conserve the spare code (in the case of a procedure)?

The code of otherfile.c (without comment) :

#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

Solution

Frama-C does not handle assembly code. It can parse some inline assembly (gcc's asm(...) instruction), but not a whole file. You should try to figure out what the PERMUTE procedure is doing and provide a replacement, either with a plain C definition or as a prototype + ACSL specification (the former being preferable if you intend to use Value Analysis).

-machdep will not let Frama-C interpret any assembly code. This option mainly fixes the size of standard integer types (e.g. 32 bit for int) and their representation (big or little endian). If you need support for a specific architecture that is not included in the ones that are currently supported (as shown with frama-c -machdep help), you should indeed contact Frama-C's support to see under which condition this can be added.

In the graphical user interface, Value Analysis will show you the code that is unreachable from the entry point of the analysis as stroken out and on a red background. It is also possible to write a script/plug-in that would extract this information programmatically, but there's nothing in the distribution for exactly that.