Value analysis plug-in
The Value analysis plug-in automatically computes variation domains for the variables of the program.
The results of the value analysis can be exploited directly in two ways.
- They can be used to infer the absence of run-time errors. The results are displayed in reverse, that is, alarms are emitted for all the operations that could lead to a run-time error. If an alarm is not emitted for an operation in the source code, then this operation is guaranteed not to cause a run-time error.
- The Frama-C graphical user interface displays the inferred sets for possible values of a variable in each point of the analyzed program.
The plug-in can be used both with the graphical user interface and in batch mode. In batch mode, the command line may look like:
frama-c -val file1.c file2.c
A list of alarms (corresponding to possible run-time errors as computed by the analysis) is produced on the standard output.
The results of the value analysis are used by many other plug-ins. In this cases, the analysis is initiated automatically by the exploiting plug-in, but it is still possible to configure it for the case at hand (e.g. through the same command-line options that would be used in conjunction with -val)
The options to configure the analysis as well as the syntax of the results are described in the full user documentation.
Only the simplest uses of dynamic allocation are handled precisely.
Only sequential code can be analysed at this time.