2016-12-13-Frama-C-Silicon-has-been-released.md

layout: post
author: André Maroneze
date: 2016-12-13 10:00 +0200
categories: Eva gui
image:
title: "Frama-C Silicon has been released!"

Frama-C 14 (Silicon) has just been released. In this post, we present a few additions that should help everyday usage of Value EVA.

Value is now EVA

The Value analysis plug-in has been renamed EVA, for Evolved Value Analysis. It has a new architecture that allows plugging abstract domains, among other features. It is a truly remarkable evolution which this post is too small to contain¹, however, so it will presented in more detail later.

¹ Facetious reference to Fermat's Last Theorem

Automatic built-in matching for libc functions

One of the new user-friendly features is the -val-builtins-auto option, which avoids having to memorize which built-in to use for each libc function that has one, namely malloc, free, and some floating-point and string-related functions (e.g. pow and strlen).

For instance, consider the following toy program, which simply allocates a buffer, copies a string into it, then allocates a buffer of the right size for the string, and stores it there.

// file.c
#include <stdio.h>
#include <stdlib.h>
#include "string.c" // include Frama-C's implementation of string.h

int main() {
  char *buf = malloc(256); // allocate a large buffer
  if (!buf) exit(1);
  char *msg = "silicon";
  strcpy(buf, msg);
  size_t n = strlen(buf);
  char *str = malloc(n + 1); // allocate a buffer with the exact size (plus '\0')
  if (!str) exit(1);
  strncpy(str, buf, n);
  str[n] = 0;
  size_t n2 = strlen(str);
  //@ assert n == n2;
  free(str);
  free(buf);
  return 0;
}

This program uses dynamic allocation and calls functions from string.h.

The following command-line is enough to obtain an interesting result:

frama-c file.c -val -val-builtins-auto -slevel 7

Without -val-builtins-auto one would need to use this overly long argument:

-val-builtin malloc:Frama_C_alloc_by_stack,free:Frama_C_free,strlen:Frama_C_strlen

For more details about Frama_C_alloc_by_stack, check the EVA manual, section 8.1.

The builtins for free and strlen were automatically chosen by EVA. Note however that strcpy and strncpy do not have builtins. In this case, we include "string.c" (which is actually in share/libc/string.c) to use the implementations available with Frama-C.

Analyzing a program using the implementations in share/libc/string.c is less efficient than using a built-in, but more precise than using only a specification. These implementations are designed to minimize the number of alarms when their inputs are imprecise. Also, because they are not optimized for execution, they are conceptually simpler than the actual libc implementations.

Using these functions. -slevel 7 ensures that their loops are fully unrolled in the example. Can you guess why 7 is the right value here?

Inspecting values in the GUI

Another improvement to usability comes in the form of a popup menu in the GUI. To see it, run the following command using the same file as previously: