RV-Match now supports inline assembly

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.

Continue reading

K Framework Seeking Professional Developers

5104335The K Framework provides extensive support for writing and validating formal semantics of programming languages, and using these semantics to execute, analyze, and even verify programs. We are part of a new joint effort to advance the implementation of the K framework – and we are now hiring for this project. The organizations involved are

Positions for professional developers are available at RV, IOHK, and ADSC. The K website has full details on the projects and the available positions.

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

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