|
From: | Kamin, Volker |
Subject: | [avr-gcc-list] avr-gcc converting c source code into assembler source code for model checking |
Date: | Thu, 16 Jun 2005 11:01:19 +0200 |
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 |
[Prev in Thread] | Current Thread | [Next in Thread] |