config/cert_exp_33.c

-void set_flag(int number, int *sign_flag) {
-  if (NULL == sign_flag) {
-    return;
-  }
-
-  if (number > 0) {
-    *sign_flag = 1;
-  } else if (number < 0) {
-    *sign_flag = -1;
-  }
-}
-
-int is_negative(int number) {
-  int sign;
-  set_flag(number, &sign);
-  return sign < 0;
-}

tp1/config/cert_exp_33.c

+#include <stddef.h>
+#include <time.h> 
+
+void set_flag(int number, int *sign_flag)
+{
+  if (NULL == sign_flag)
+  {
+    return;
+  }
+
+  if (number > 0)
+  {
+    *sign_flag = 1;
+  }
+  else if (number < 0)
+  {
+    *sign_flag = -1;
+  }
+  else{
+    *sign_flag = 0;
+  }
+  Frama_C_show_each_set_flag(number, *sign_flag);
+}
+
+int is_negative(int number)
+{
+  int sign;
+  set_flag(number, &sign);
+  Frama_C_show_each_is_negative(number, sign);
+  return sign < 0;
+}

tp1/rapport.docx

+J'ai eu quelques soucis liés à l'absence du include en début de code
+
+sign peut être non-initialisé si number = 0
+avec partition history, eva sépare les cas de number en positif, nul et négatif
+red alarm quand partiion-history > 2
+avec interprocedural history, la console spammme, attention à bien avoir le include time
+
+correction de set_flag : remplacer > par >=
+
+**Realloc**
+Point d'entrée choisi : func
+Red Alarm quand -eva-slevel = 10
+
+
+Problème : le code corrigé fait apparaitre de nouvelles erreurs et mêmes de nouvelles alarmes rouges
+Corrigé en ajoutant les return dans la version corrigée du code
+

tp2/Pystan/Rapport.md

+## Calcul de point fixe
+ À quoi
+correspondent les nœuds indiqués comme inatteignables par l'analyse? --> le cas one <> 1 et le noeud final car la loop est infinie
+
+## Propagation de constante
\ No newline at end of file