Field-Sensitive Value Analysis of Embedded C Programs with Union Types and Pointer Arithmetics

Details Field-Sensitive Value Analysis of Embedded C Programs with Union Types and Pointer Arithmetics Field-Sensitive Value Analysis of Embedded C Programs with Union Types and Pointer Arithmetics

2007-03-15

arxiv.org/abs/cs/0703074v2

Languages, Compilers, and Tools for Embedded Systems (LCTES) (06/2006) 54-63

Computer Science

Programming Languages

(update: reversed author first and last names)

Scientific paper

We propose a memory abstraction able to lift existing numerical static analyses to C programs containing union types, pointer casts, and arbitrary pointer arithmetics. Our framework is that of a combined points-to and data-value analysis. We abstract the contents of compound variables in a field-sensitive way, whether these fields contain numeric or pointer values, and use stock numerical abstract domains to find an overapproximation of all possible memory states--with the ability to discover relationships between variables. A main novelty of our approach is the dynamic mapping scheme we use to associate a flat collection of abstract cells of scalar type to the set of accessed memory locations, while taking care of byte-level aliases - i.e., C variables with incompatible types allocated in overlapping memory locations. We do not rely on static type information which can be misleading in C programs as it does not account for all the uses a memory zone may be put to. Our work was incorporated within the Astr\'{e}e static analyzer that checks for the absence of run-time-errors in embedded, safety-critical, numerical-intensive software. It replaces the former memory domain limited to well-typed, union-free, pointer-cast free data-structures. Early results demonstrate that this abstraction allows analyzing a larger class of C programs, without much cost overhead.

Affiliated with

Also associated with

No associations

Rating

Field-Sensitive Value Analysis of Embedded C Programs with Union Types and Pointer Arithmetics does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Field-Sensitive Value Analysis of Embedded C Programs with Union Types and Pointer Arithmetics, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Field-Sensitive Value Analysis of Embedded C Programs with Union Types and Pointer Arithmetics will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-363595