el diablo está en los detalles, pero esto puede funcionar para usted:
En primer lugar, obtener Frama-C. Si está usando Unix, su distribución puede tener un paquete. El paquete no será la última versión, pero puede ser lo suficientemente bueno y le ahorrará algo de tiempo si lo instala de esta manera.
Digamos que su ejemplo es como abajo, solamente mucho más grande que no es obvio lo que está mal:
int add(int x, int y)
{
static int state;
int result = x + y + state; // I tested it once and it worked.
state++;
return result;
}
ingresa un comando como:
frama-c -lib-entry -main add -deps ugly.c
Opciones -lib-entry -main add significa "mirar a la función add ". La opción -deps calcula dependencias funcionales. Encontrará estos "dependencias funcionales" en el registro:
[from] Function add:
state FROM state; (and default:false)
\result FROM x; y; state; (and default:false)
Esta lista las entradas reales los resultados de add dependen, y los salidas reales calculados a partir de estas entradas, incluyendo las variables estáticas leídos desde y modificado Una variable estática que se inicializó correctamente antes de usarse normalmente no aparecería como entrada, a menos que el analizador no haya podido determinar que siempre se inicializó antes de que se leyera.
El registro muestra state como dependencia de \result. Si esperaba que el resultado devuelto dependiera únicamente de los argumentos (lo que significa que dos llamadas con los mismos argumentos producen el mismo resultado), es una pista de que puede haber algo mal aquí, con la variable state.
Otra sugerencia que se muestra en las líneas anteriores es que la función modifica state.
Esto puede ayudar o no. La opción significa que el analizador no supone que ninguna variable estática no constante haya conservado su valor en el momento en que se llama a la función bajo análisis, por lo que puede ser demasiado impreciso para su código. Hay formas de evitarlo, pero depende de usted si quiere apostar el tiempo necesario para aprender de esta manera.
EDIT: aquí es un ejemplo más complejo:
void initialize_1(int *p)
{
*p = 0;
}
void initialize_2(int *p)
{
*p; // I made a mistake here.
}
int add(int x, int y)
{
static int state1;
static int state2;
initialize_1(&state1);
initialize_2(&state2);
// This is safe because I have initialized state1 and state2:
int result = x + y + state1 + state2;
state1++;
state2++;
return result;
}
En este ejemplo, el mismo comando produce los resultados:
[from] Function initialize_1:
state1 FROM p
[from] Function initialize_2:
[from] Function add:
state1 FROM \nothing
state2 FROM state2
\result FROM x; y; state2
Lo que se ve por initialize_2 es una lista vacía de dependencias, lo que significa que la función no asigna nada. Haré que este caso sea más claro al mostrar un mensaje explícito en lugar de solo una lista vacía. Si sabe lo que debe hacer cualquiera de las funciones initialize_1, initialize_2 o add, puede comparar este conocimiento a priori con los resultados del análisis y ver si algo está mal para initialize_2 y add.
SEGUNDA EDICION: y ahora mi ejemplo muestra algo extraño para initialize_1, así que quizás debería explicar eso. La variable state1 depende de p en el sentido de que p se usa para escribir en state1, y si p hubiera sido diferente, entonces el valor final de state1 hubiera sido diferente. Aquí hay un último ejemplo:
int t[10];
void initialize_index(int i)
{
t[i] = 1;
}
int main(int argc, char **argv)
{
initialize_index(argv[1][0]-'0');
}
Con el comando frama-c -deps t.c, las dependencias computados para initialize_index son:
[from] Function initialize_index:
t[0..9] FROM i (and SELF)
Esto significa que cada una de las células depende de i (puede ser modificado si i es el índice de esa celda en particular). Cada celda también puede mantener su valor (si i indica otra celda): esto se indica con la mención (and SELF) en la última versión, y se indicó con un (and default:true) más oscuro en versiones anteriores.
Pregunta interesante, pero valgrind no tiene conocimiento de "local" o "declarado". Creo que esto debe hacerse por análisis de código, no por análisis ejecutables. – aschepler
usamos PC Lint, pero genera infinidad de advertencias, por lo que encontrar los puntos de acceso real a veces es como pescar en la oscuridad. –