1. 26 Nov, 2020 2 commits
    • Julien COHEN's avatar
      [REFACTORING] Clean. · d8b0d7d7
      Julien COHEN authored
      d8b0d7d7
    • Julien COHEN's avatar
      Nouvelle sémantique qui est syntaxiquement identique à celle de... · 78ccd033
      Julien COHEN authored
      Nouvelle sémantique qui est syntaxiquement identique à celle de COMPCERT/cfrontend/Csem.v (identité) et on prouve l'equivalence entre les deux. Ceci a pour objectif de servir d'exemple pour comprendre la bisimilation entre deux sémantiques et aussi de modèle pour construire des variantes de la sémantique originale et prouver leur équivalence avec celle-ci.
      78ccd033
  2. 20 Nov, 2020 2 commits
  3. 18 Aug, 2020 1 commit
  4. 22 Jul, 2020 2 commits
  5. 21 Jul, 2020 1 commit
  6. 03 Jul, 2020 3 commits
  7. 02 Jul, 2020 1 commit
  8. 30 Jun, 2020 2 commits
  9. 25 Jun, 2020 2 commits
  10. 10 Jun, 2020 1 commit
  11. 18 May, 2020 2 commits
  12. 18 Apr, 2020 1 commit
  13. 13 Apr, 2020 1 commit
  14. 11 Apr, 2020 1 commit
    • Julien COHEN's avatar
      Variante de la sémantique de Compcert Csem où on change unqiement la... · b75c4f23
      Julien COHEN authored
      Variante de la sémantique de Compcert Csem où on change unqiement la définition de call_cont pour qu'elle avance sur Kdo. Ce n'est pas nécessaire car les états rencontrés lors des transitions respectent l'invariant no_kdo comme déjà démontré. Toutefois, cela devrait éviter d'avoir à utiliser cet invariant et simplifier certaines preuves (à faire). Il est démontré que la sémantique est équivalente à celle de Compcert.
      b75c4f23
  15. 10 Apr, 2020 1 commit
    • Julien COHEN's avatar
      Nouvelle sémantique basée sur Csem.v mais dans laquelle on retrouve le nom de... · f98c4e8d
      Julien COHEN authored
      Nouvelle sémantique basée sur Csem.v mais dans laquelle on retrouve le nom de la fonction qu'on est en train d'exécuter. Cela permet (j'espère) de pouvoir considérer des refactorings locaux à certaines fonctions désignées par leur nom et ainsi d'éviter de faire l'hypothèse que toutes les fonctions ont un corps différent afin de les identifier.
      f98c4e8d
  16. 19 Mar, 2020 1 commit
  17. 16 Mar, 2020 3 commits
  18. 12 Mar, 2020 2 commits
  19. 11 Mar, 2020 1 commit
  20. 10 Mar, 2020 5 commits
  21. 09 Mar, 2020 1 commit
  22. 03 Mar, 2020 1 commit
  23. 02 Mar, 2020 1 commit
  24. 21 Feb, 2020 2 commits