alteration of user-defined assigns clauses
ID0000468: This issue was created automatically from Mantis Issue 468. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000468 | Frama-C | Kernel | public | 2010-05-03 | 2011-10-21 |
| Reporter | ddelmas | Assigned To | virgile | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Boron-20100401 | Target Version | - | Fixed in Version | - |
Description :
The builtin.* source files distributed together with Frama-C define the below prototypes :
builtin.c :
//@ assigns Frama_C_entropy_source \from Frama_C_entropy_source; void Frama_C_update_entropy(void);
builtin.h :
/*@ assigns \result \from a, b, Frama_C_entropy_source; assigns Frama_C_entropy_source \from Frama_C_entropy_source; */ int Frama_C_nondet(int a, int b);
[...]
/*@ assigns \result \from min, max, Frama_C_entropy_source; assigns Frama_C_entropy_source \from Frama_C_entropy_source; */ int Frama_C_interval(int min, int max);
Let us prompt the below commands on the attached assigns.c source file :
SHARE=frama-c -print-path
export CPP="gcc -C -E -I$SHARE"
frama-c assigns.c $SHARE/builtin.c -print -ocode print_assigns.c
The generated print_assigns.c source file defines the following behaviors :
/*@ behavior default: assigns Frama_C_entropy_source; assigns Frama_C_entropy_source \from Frama_C_entropy_source; / extern void Frama_C_update_entropy(void) ; /@ behavior default: assigns Frama_C_entropy_source; assigns \result \from a, b, Frama_C_entropy_source; assigns Frama_C_entropy_source \from Frama_C_entropy_source; */ int Frama_C_nondet(int a , int b ) { [...] }
/*@ behavior default: assigns Frama_C_entropy_source; assigns \result \from min, max, Frama_C_entropy_source; assigns Frama_C_entropy_source \from Frama_C_entropy_source; */ int Frama_C_interval(int min , int max ) { [...] }
Theses clauses are correct, but they spoil the precision of the value analysis plug-in on the interpretation of \from clauses. See the "Additional Information" field for a detailed explanation by Pascal Cuoq.
Additional Information :
Message from Pascal Cuoq :
J'ai dû transformer ton fichier ainsi :
int Frama_C_entropy_source ; /*@ behavior default: // assigns Frama_C_entropy_source; assigns Frama_C_entropy_source \from Frama_C_entropy_source;
/ extern void Frama_C_update_entropy(void) ; /@ behavior default: // assigns Frama_C_entropy_source; assigns \result \from a, b, Frama_C_entropy_source; assigns Frama_C_entropy_source \from Frama_C_entropy_source;
*/ int Frama_C_nondet(int a , int b ) { int tmp ; Frama_C_update_entropy(); ...
et ce pour chaque ligne d'assigns qui était ainsi redondante.
En effet chaque ligne d'assigns est sensée être vérifiée indépendamment des autres, donc cela ne change pas le sens d'écrire les choses en double comme c'était dans le fichier, mais l'analyse de valeurs ne cherche pas à être trop maline sur les assigns qui ont une intersection non vide. Quand elle voit
assigns Frama_C_entropy_source ;elle note que cette variable est calculée à partir de toutes les variables accessibles, et comme les inputs d'une fonction incluent les inputs des appelées, c'est toutes les fonctions appelant directement ou indirectement celles qui sont sur-spécifiées qui semblent lire toute la mémoire.
Si ces assigns ont été générés par une transformation de Frama-C à partir d'assigns non redondants, alors ce n'est pas vraiment ta faute et c'est un bug qu'il convient de rapporter.