1. 9

  2. 2

    This seems to be like dialyzer for c? Also has anyone used this and can contrast it with valgrind?

    1. 1

      I don’t have any experience with Frama-C, but valgrind is, as far as I know, a runtime analyzer. It requires hitting code paths to validate them according to whatever metrics it has. Frama-C is a source could analyzer, which doens’t require running the source code.

      1. 2

        To extend on this, to the best of my knowledge, Frama-C is largely trying to reason about value properties in the program, for example deducing that “on line 5 the variable x >= 5.” Such a statement holds on all paths for all program inputs (i.e., it is always true in the program). This allows for the user to check if the program satisfies some specification. In contrast, valgrind can only generate information about the runtime paths which it observed. Generally, something like Frama-C is used to verify safety properties (something bad never happens) in a program whereas Valgrind is used to find bugs but not prove their absence.

        Specifically, creating an algorithm to automatically deduce information which holds over all paths and over all inputs is intractable since the search space is huge. So, approximations to the program’s behaviour are used so that the calculated information contains at least all the behaviour in the program and perhaps some additional, spurious information. As a result, the analysis may produce false alarms, e.g., the analysis may say that “x >= 5” when in fact in all feasible executions of the program “x >= 10”.

        However, when attempting to reason about a specification in this way, the analysis usually attempts to always find all the errors in the program. In other words, if there exists an error in the program it will be detected (along with some false alarms). In the previous example, notice how “x >= 5” implies that “x >= 10”; the analysis deduced an over-approximated fact which included all the valid program behaviour. If “x >= 5” is not sufficient enough to prove the program satisfies its specification then either the analysis or the program needs to be modified.

        To make a long story short, a runtime (dynamic) analyses typically are used for bug hunting (e.g., trying to find a path through the program which causes an error) whereas a static analysis in the style of Frama-C attempts to prove the absence of errors. (Though, there are dynamic analyses which try to predict additional behaviour of the program given a dynamic trace).