--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on January 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Support for RISCV



On 01/21/2017 01:08 PM, Paulo Matos wrote:
> My guess is that you need to know datatypes sizes for a specific
> arch for proper static analysis of C code.

Sizes, alignments, builtin functions, ..., and many other
implementation-defined behaviors, several of which can be influenced
by toolchain options.  Indeed, for proper static analysis of C code
you need a rather precise model of the toolchain, one that includes
the effect of each option that may influence the program semantics.
Kind regards,

   Roberto

-- 
     Prof. Roberto Bagnara

Applied Formal Methods Laboratory - University of Parma, Italy
mailto:bagnara at cs.unipr.it
                              BUGSENG srl - http://bugseng.com
                              mailto:roberto.bagnara at bugseng.com


> On 21 January 2017 12:06:14 CET, "Gerlach, Jens" <jens.gerlach at fokus.fraunhofer.de> wrote:
> 
>     Hello,
> 
>     do you mean https://en.wikipedia.org/wiki/RISC-V ?
> 
>     I don’t understand what this has to do with static analysis of C(!)-code.
> 
>     Regards
> 
>     Jens
>         
>     ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
> 
>         
>         Message: 1
>         Date: Fri, 20 Jan 2017 12:33:49 +0100
>         From: Paulo Matos <pmatos at linki.tools>
>         To: frama-c-discuss at lists.gforge.inria.fr
>         Subject: [Frama-c-discuss] Support for RISCV
>         Message-ID: <9732e061-bac9-7205-b3da-9682f67abe87 at linki.tools>
>         Content-Type: text/plain; charset=utf-8
>         
>         Hello,
>         
>         What's the best place to start if I want to add support for RISCV?
>         
>         Is there any documentation on adding a new backend to Frama-C?
>         
>      
> 
>     ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
> 
>     Frama-c-discuss mailing list
>     Frama-c-discuss at lists.gforge.inria.fr
>     http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
> 
> 
> -- 
> Sent from my Android device with K-9 Mail. Please excuse my brevity.
> 
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
>