Le soucis avec Frama_C_interval ici c'est que now est un long. Je lance l'analyse avec -machdep x86_64 sur une plateforme ou int est 32bits, donc 109 devrait rentrer dans un int, mais pour un cas plus général, j'ai l'impression qu'il n'y a pas d'équivalent pour les long.
Quand je dis que la fonction ne semble pas fonctionner correctement, c'est parce qu'à la fin de l'analyse, frama-c affiche que "now ∈ {0}" ce qui semble trés trés louche. J'ai ajouté "now = 4" à divers endroits de la fonction rand_initialize_framac, et à chaque fois l'analyse affiche "now ∈ {4}", ce qui montre bien que now n'est pas réinitialisé à 0 par les fonctions appelées. Je suis quasiment certain que en l'état, l'analyse est incorrecte.
[value] Values at end of function rand_initialize_framac:
now ∈ {0}
i ∈ {10}
IBAA_memory[0..255] ∈ [--..--]
IBAA_results[0..255] ∈ [--..--]
IBAA_aa ∈ [--..--]
IBAA_bb ∈ [--..--]
IBAA_counter ∈ [--..--]
IBAA_byte_index ∈ [--..--]
memIndex ∈ [-2147483648..--],0%2
L15_x ∈ [--..--]
L15_y ∈ [--..--]
L15_start_x ∈ {0}
L15_state[0..255] ∈ [--..--]
[^] # Re: courage!
Posté par Enj0lras . En réponse au journal Analyser la génération de nombre aléatoire du noyau. Évalué à 3.
Bonjour, merci pour les remarques !
Le soucis avec Frama_C_interval ici c'est que now est un long. Je lance l'analyse avec -machdep x86_64 sur une plateforme ou int est 32bits, donc 109 devrait rentrer dans un int, mais pour un cas plus général, j'ai l'impression qu'il n'y a pas d'équivalent pour les long.
Quand je dis que la fonction ne semble pas fonctionner correctement, c'est parce qu'à la fin de l'analyse, frama-c affiche que "now ∈ {0}" ce qui semble trés trés louche. J'ai ajouté "now = 4" à divers endroits de la fonction rand_initialize_framac, et à chaque fois l'analyse affiche "now ∈ {4}", ce qui montre bien que now n'est pas réinitialisé à 0 par les fonctions appelées. Je suis quasiment certain que en l'état, l'analyse est incorrecte.