[avr-gcc-list] avr-gcc converting c source code into assembler source code for model checking

[Kamin, Volker]

Hi everyone.

 

Summary:

I am looking for a formal description of the transformation process from c source code into assembler source code.

 

Intro:

I am currently working on a project creating a model checker for ATMEL AVR. The goal is to release a working program that can detect flaws in programs like possible deadlocks, unreachable code, stack overflow, etc. We found out, that none of the model checkers we considered (CBMC, BLAST, and many, many more) could be easily modified to suit our goal. Now we are planning our own model checker, specialized for ATMEL AVR.

 

Problem:

I have an exhaustive description of the ATMEL assembler, but weren’t able to find a formal description of the assembler subset that is used to produce the output of “avr-gcc main.s”.

 

Any help is appreciated and helps us to proceed towards our goal.

 

Regards,

 

Volker Kamin

Department of Computer Science XI

University of Technology Aachen, Germany