roptat @roptat@framapiaf.org

merci de m'avoir écouté :)

\_o<

ou alors je ne fais aucun pré-calcul et j'espère que la comparaison directe ne prenne pas trop longtemps... Dans tous les cas, il faut que je trouve si je peux indiquer à klee qu'une fonction ne doit pas être interprétée, et si les fonctions de la bibliothèque changent souvent entre les versions.

En plus je veux obtenir quelque chose de rapide (sans compter un éventuel pré-calcul, comme l'analyse que je fais actuellement avec klee). Donc il faudrait précalculer chaque paire. Soit un nombre exponentiel de précalculs plus ou moins linéaires, soit un nombre linéaire de précalculs exponentiels... le choix est compliqué ^^'

je peux aussi faire une analyse en parallèle, et là les fonctions non interprétées ont plus de sens, parce que je construis le même état (abstrait) des deux côtés, tant que la fonction est la même des deux côtés. le problème, c'est que là j'ai besoin de faire une analyse par *paire* de versions.

mais en même temps, entre deux versions les changements sont faibles. Si je sais quelles versions je veux comparer avant de lancer klee je peux déjà réduire le nombre de fonctions à analyser (avec un diff je repère celles qui n'ont pas changées).

or justement je ne sais pas à l'avance quelles versions je veux comparer, c'est pour ça que j'analyse les versions séparément : j'en analyse un tas et ensuite je peux facilement comparer les résultats deux à deux.

il y a un papier, ucklee, qui propose un truc comme ça, mais impossible de mettre la main sur le code. Une autre possibilité que j'ai vu, c'est d'abstraire l'appel de fonction, et de se retrouver avec une fonction non interprétée dans l'état du programme. Pratique si la fonction est la même entre les deux versions qui m'intéressent, mais sinon sans grand intérêt.

j'ai l'impression qu'il passe beaucoup de temps dans le fonctions de la bibliothèque, plutôt que dans la fonction qui m'intéresse vraiment, et qu'il y repasse plusieurs fois et recommence toute l'analyse de la fonction. Je me demande si je peux pas plutôt lui fournir un résummé de ce que fait la fonction et le laisser résoudre une grosse formule pour trouver les états possibles à la fin

j'ai un programme dont je veux analyser les changements au cours du temps, au niveau sémantique. L'idée c'est de lancer klee (qui trouve tous les chemins d'exécution possibles) séparément sur les deux versions qui m'intéressent, puis de comparer les traces. Sauf qu'à ce rythme là, klee il aura fini dans deux ans.

Bon là je crois que je saisis mieux la différence entre interprétation abstraite et exécution symbolique. Le premier est peu précis mais termine rapidement, le deuxième est exact mais, c'est super leeeeeent...

Je vais voir si je peux reformuler mon problème pour permettre un peu d'imprécision, ça devrait accélérer un peu les choses...