RV-Match now supports execution of applications containing x86_64 inline assembly. If you have a program that contains inline assembly, you can compile it with kcc like any other C program and we will compile the functions containing inline assembly with gcc and execute them directly the same way we handle any other native code which we do not have C source for. As a result of this, the ability to detect undefined behavior in that function is eliminated, but it allows you to analyze complex applications which contain some code in inline assembly which you do not want to translate into C source.
Runtime Verification seeking a Senior Verification Engineer and a Full Stack Software Engineer
Runtime Verification, Inc is looking for two new software engineers to work on our family of products. We are a start-up based in Urbana, Illinois, less than 15 walk minutes away from the Computer Science Department at the University of Illinois in Urbana-Champaign (UIUC), which is in the top 5 schools in Computer Science in the United States and the top 1-2 schools in the domains of software engineering, formal methods and programming languages. Continue reading
Experienced C Developers Can Still Misunderstand Simple Language Concepts
Not long ago, one of our customers came to us confused about an analysis report on a simple program their company used internally to assess knowledge of C. Among the code they sent us was something like the following three lines:
int32_t var = 0xffeeddcc; int32_t var2 = 0x7f000000; var2 <<= 8;
They assumed that this code should be free from defects, and thought that possibly the two defects we reported were incorrect. Let's take a look at the error reports that result when we insert these lines into a simple program and execute them:
Continue reading
Runtime Verification seeking a Software Development Engineer
Runtime Verification, Inc is looking for a software engineer to work on our family of products. We are a start-up based in Urbana, Illinois, less than 15 walk minutes away from the Computer Science Department at the University of Illinois in Urbana-Champaign (UIUC), which is in the top 5 schools in Computer Science in the United States and the top 1-2 schools in the domains of software engineering, formal methods and programming languages. Continue reading
Using RV-Predict to track down race conditions
We've all had it happen: you write some multithreaded code, but when you run it, it crashes with some kind of error every second or third or hundredth run. The traditional way of trying to debug this problem is very tedious and involves attempting to reproduce the error (difficult) and then tracing the inconsistent state backwards to find the source of the race condition (even more difficult).
Enter RV-Predict. Today I was developing code for RV-Match when I ran into an intermittently occurring NullPointerException in its parser. Instead of trying to reproduce the bug and tracking its behavior backwards, I assumed going in that it was caused by a race condition, and ran RV-Predict on the program. After it crashed, it spat out the following error report: Continue reading
“restrict” keyword in header files
It would appear that Mac OS X's copy of string.h is invalid.
It declares strcpy as
char *strcpy(char *, const char *);
But the C standard declares it as
char *strcpy(char * restrict, const char * restrict);
These two types are actually incompatible with each other according to the C standard, and a function that is declared more than once in different translation units with different declarations is considered undefined behavior. Thus, any correctly conforming C library will cause any code that includes string.h to be undefined.
Oops!
Undefined C: Common mistakes
This blog post is the beginning of an intended series of blog posts detailing undefined and unspecified behavior in the ISO C standard, and its impact on development. To start with, we will summarize the domain and provide information about some of the undefined behaviors which we have found to be most widespread in production-deployed C code of the open source projects we have tested.