diff --git a/Makefile b/Makefile index 6856c2b..8637127 100644 --- a/Makefile +++ b/Makefile @@ -32,7 +32,7 @@ all: $(PDFS) watch: while inotifywait -e close_write "src/étude/OCamlPro_PPAQSE-COTS_rapport.typ" || true; do make; done -$(BUILD_DIR)/%.pdf: src/%.typ $$(call deps,src/%.typ) $$(dir src/%)/bibliography.yml Makefile | $$(@D)/. +$(BUILD_DIR)/%.pdf: src/%.typ src/base.typ $$(call deps,src/%.typ) $$(dir src/%)/bibliography.yml Makefile | $$(@D)/. $(TYPST) c $(TYPST_ARGS) $< # force moving file for typst seems to always try building locally oO mv -f src/$*.pdf $@ diff --git a/src/base.typ b/src/base.typ index 65307f0..0e4f1ef 100644 --- a/src/base.typ +++ b/src/base.typ @@ -66,6 +66,7 @@ dir: ttb, spacing: 2pt, line(length: 100%), + v(5pt), align( center + horizon, [ @@ -89,7 +90,9 @@ text(size: 40pt, [*#title*]), text(size: 30pt, [*#subtitle*]), authors, - body + body, + v(1fr), + image("imgs/by.png") ) ) ] @@ -240,8 +243,8 @@ ) } ), - v(10%), - + v(1fr), + image("imgs/by.png") ) ) diff --git a/src/imgs/by.png b/src/imgs/by.png new file mode 100644 index 0000000..c8473a2 Binary files /dev/null and b/src/imgs/by.png differ diff --git "a/src/pr\303\251sentation/OCamlPro_PPAQSE-COTS_pr\303\251sentation.typ" "b/src/pr\303\251sentation/OCamlPro_PPAQSE-COTS_pr\303\251sentation.typ" index e69de29..1c0ddf7 100644 --- "a/src/pr\303\251sentation/OCamlPro_PPAQSE-COTS_pr\303\251sentation.typ" +++ "b/src/pr\303\251sentation/OCamlPro_PPAQSE-COTS_pr\303\251sentation.typ" @@ -0,0 +1,652 @@ + +#import "../base.typ": * +#import "../étude/links.typ": * + + +#show: presentation + +#title-slide( + title: [ + Écosystèmes COTS de développement et de vérification des logiciels + critiques et temps réel + ], + subtitle: "", + authors: [Julien Blond (julien.blond\@ocaml.pro)], +) + +#slide[ + = OCamlPro + + - PME française créée en 2011 + - ADN recherche et liens étroits avec la recherche académique. + - OCaml : core team, opam & optimisations + - R&D langages (DSL) & dette technique (Cobol) + - Méthodes formelles (Alt-Ergo) + - Certification Sécurité (CC EAL6+) + - Formations (OCaml, Rust, Coq) + + Jane street, Inria, DGFiP, Samsung, Mitsubishi, Thales, CEA, Adacore, + TrustInSoft +] + +#slide[ + = Objectif + + Tour d'horizon des langages de programmation dans la sûreté: + - C + - C++ + - Ada + - Scade + - OCaml + - Rust + + Donner suffisamment d'informations pour faire un choix éclairé +] + +#slide[ + = C + + - Créé en 1972 par Dennis Ritchie + - Programmation système (Unix) + - Langage bas niveau + - Standardisé : C89, C99, C11, C18, C23 (draft)... + - ... mais une sémantique indéterministe. + + +] + +#slide[ + = C++ + + - Créé en 1979 par Bjarne Stroustrup + - C++ = C + classes + templates + exceptions + ... + - Mêmes usages que le C mais censé être plus efficace/productif + - Standardisé : C++98, C++03, C++11, C++14, C++17, C++20, C++23... + - ... mais sémantique indéterministe. +] + +#slide[ + = Ada + + - Initié par le DoD dans les années 1970 + - Langage de programmation de haut niveau pour la sûreté + - Standardisé : Ada83, Ada95, Ada2005, Ada2012, Ada2023 + - Sémantique claire +] + +#slide[ + = Scade + + - Créé dans les années 1990 par VERIMAG/VERILOG + - Repris par Esterel Technologies/Ansys + - Langage de programmation graphique basé sur Lustre + - Propriétaire + - Sémantique déterministe +] + +#slide[ + = OCaml + + - Créé en 1996 par l'INRIA + - Lignée des langages ML + - Lien étroit avec Coq + - Centré sur l'algorithmique et la simplicité + - Sémantique mathématique issue du $lambda$-calcul +] + +#slide[ + = Rust + + - Créé dans les années 2000 chez Mozilla + - Première version en 2015 + - C++ amélioré + - Qualifications/standarisation en cours +] + +#slide[ + = Paradigmes + + #align( + center, + table( + columns: (auto, auto, auto, auto, auto), + align: left, + align(center)[*Langage*], + align(center)[*Impératif*], + align(center)[*Fonctionnel*], + align(center)[*Objet*], + align(center)[*Déclaratif*], + [C], [✓], [\~], [], [], + [C++], [✓], [\~], [✓], [], + [Ada], [✓], [], [\~], [], + [Scade], [], [], [], [_dataflow_, graphique], + [OCaml], [✓], [✓], [✓], [], + [Rust], [✓], [✓], [\~], [], + ) + ) +] + +#slide[ + = Mécanismes de protection intrinsèques + + #align( + center, + table( + columns: (auto, auto, auto, auto, auto), + align: left, + align(center)[*Langage*], + align(center)[*Typage*], + align(center)[*Pointeurs*], + align(center)[*Mémoire*], + align(center)[*Contrôles*], + [C], [😕], [😨], [😨], [😕], + [C++], [😕], [😨], [😨], [😐], + [Ada], [😊], [😌], [😨], [😊], + [Scade], [😊], [😊], [😊], [😊], + [OCaml], [😃], [😊], [😃], [😊], + [Rust], [😊], [😕], [😌], [😊], + ) + ) +] + +#slide[ + = Compilateurs + + #align( + center, + table( + columns: (auto, auto), + align: (left, left), + align(center)[*Langage*], align(center)[*Compilateurs*], + [C], [GCC, Clang/LLVM, icx, MSVC, AOCC, sdcc, CompCert, ...], + [C++], [G++, Clang/LLVM, icx, MSVC, AOCC, C++ Builder, ...], + [Ada], [GNAT (GCC), GNAT Pro/LLVM, GreenHills Ada, PTC, Janus/Ada], + [Scade], [Scade Suite], + [OCaml], [OCaml (ocamlc, ocamlopt)], + [Rust], [rustc] + ) + ) +] + +#slide[ + = Interfaçage + + #align( + center, + table( + columns: (auto, auto), + align: (left, left, left, left), + align(center)[*Langage source*], align(center)[*Langage(s) cibles(s)*], + [C], [ASM], + [C++], [C, ASM], + [Ada], [C], + [Scade], [C, Ada (out)], + [OCaml], [C], + [Rust], [C] + ) + ) +] + + +#slide[ + = Adhérence + + #align( + center, + table( + columns: (auto, auto), + align: (left, left), + align(center)[*Langage*], align(center)[*Adhérence*], + [C], [], + [C++], [], + [Ada], [], + [Scade], [], + [OCaml], [POSIX (natif), VM (objet)], + [Rust], [] + ) + ) +] + +#slide[ + = Gestionnaires de paquets + + #align( + center, + table( + columns: (auto, auto), + align: (left, left), + align(center)[*Langage*], align(center)[*Gestionnaire(s) de paquet(s)*], + [C], [Clib, Conan, vcpkg], + [C++], [Buckaroo, Conan, vcpkg], + [Ada], [Alire], + [Scade], [], + [OCaml], [opam], + [Rust], [Cargo] + ) + ) + + - Agnotisques: Nix, 0install, opam, ... + - Systèmes embarqué : Yocto, Buildroot, ... +] + +#slide[ + = Communauté + + #[ + #set text(size: 18pt) + #align( + center, + table( + columns: (auto, auto, auto, auto, auto), + align: (left, left), + align(center)[*Langage*], + align(center)[*Fondation(s)/Association(s)*], + align(center)[*Entreprise(s)*], + align(center)[*Recherche*], + align(center)[*Volume*], + [C], [FSF], [+++], [], [+++], + [C++], [FSF], [+++], [], [+++], + [Ada], [Ada Europe, Ada Resource Association, Ada France], [Adacore, +], [], [+], + [Scade], [], [Ansys], [Verimag], [+], + [OCaml], [OSF], [Jane Street, OCamlPro, Tarides, +], [INRIA], [+], + [Rust], [RF, Rust France], [AWS, Mozilla, +], [], [++], + ) + ) + ] +] + +#slide[ + = Debugueurs + + #{ + set text(size: 16pt) + + figure( + table( + columns: (auto, auto), + align(center)[*Langage*], + align(center)[*Debugueur(s)*], + [C], [#gdb, #lldb, #totalview, #undo, #valgrind, #vsd, #windbg, #rr, #linaro], + [C++], [#gdb, #lldb, ...], + [Ada], [#gdb, #lldb], + [Scade], [Scade Suite], + [OCaml], [ocamldebug (objet), #gdb, #lldb, ...], + [Rust], [#gdb, #lldb, #windbg] + + ) + ) + } +] + +#slide[ + = Tests + + #align( + center, + table( + columns: (auto, auto), + [C], [#cantata, #parasoft, #TPT, #vectorcast, ...], + [C++], [#cantata, #parasoft, #TPT, #vectorcast, #testwell_ctc, #boost, #gtest, ...], + [Ada], [#aunit, #adatest95, #avhen, #ldra, #vectorcastAda, #rtrt], + [Scade], [Scade Suite], + [OCaml], [#ounit, #alcotest, #qcheck, #crowbar, PPX, Cram, ...], + [Rust], [_builtin_, quickcheck, proptest, mockall, ...] + + ), + ) +] + +#slide[ + + = Parsing + + #align( + center, + table( + columns: (auto, auto), + [C], [Flex/Bison, ANTLR, ...], + [C++], [Flex/Bison, ANTLR, ...], + [Ada], [AFlex/AYacc], + [Scade], [], + [OCaml], [sedlex, ulex, Menhir, ocamllex, ocamlyacc, angstrom, dypgen, ...], + [Rust], [LALRPOP, Hime, Syntax] + ) + ) + +] + +#slide[ + = Méta-programmation (C) + + - Le préprocesseur permet de faire précalculer des expressions simples + par le compilateur (souvent inutile) + - Il existe des _tricks_ d'expansion récursive bornée (à éviter) + ```c + /* #define sum(n) ((n * (n + 1)) / 2) */ + inline int sum(int n) { return (n * (n + 1)) / 2; } + int main() { return sum(10); } + ``` + ```asm + 0x0000000000001040 : endbr64 + 0x0000000000001044 : mov $0x37,%eax + 0x0000000000001049 : retq + ``` +] + +#slide[ + = Méta-programmation (C++) + + Les _templates_ sont Turing-complets et permettent de calculer virtuellement + n'importe quoi qui ne dépende pas d'une IO. + ```cpp + template struct Fact { + enum {Value = N * Fact::Value}; + }; + template<> struct Fact<0> { + enum {Value = 1}; + }; + unsigned int x = Fact<4>::Value; + ``` +] + +#slide[ + = Méta-programmation (Ada & Scade) + + Pas de support de méta-programmation. +] + +#slide[ + = Méta-programmation (OCaml) + + Les PPX permettent de transformer le code source avant la compilation + + ```ocaml + let main () = + [%init 42]; + let v = some_calculus () in + [%do_something v] + ``` +] + +#slide[ + = Méta-programmation (Rust) + + Les macros permettent de transformer le code source avant la compilation + + #[ + #set text(size: 18pt) + ```rust + macro_rules! vec { + ($($x:expr),*) => { + { + let mut temp_vec = Vec::new(); + $(temp_vec.push($x);)* + temp_vec + } + }; + } + ``` + + ```rust + let v = vec![1, 2, 3]; + ``` + ] +] + +#slide[ + = Dérivation (C) + + Les macros permettent une forme archaïque de dérivation + ```c + #define COULEUR X(ROUGE, 0xFF0000) X(VERT, 0x00FF00) X(BLEU, 0x0000FF) + #define X(c, v) c = v, + typedef enum { COULEUR } couleur_t; + #undef X + ``` +] + +#slide[ + = Dérivation (C++) + + On peut avoir une forme de dérivation via les _templates_: + ```cpp + template + struct is_pointer { + static const bool value = false; + }; + template + struct is_pointer { + static const bool value = true; + }; + ``` +] + +#slide[ + = Dérivation (Ada & Scade) + + Pas de support de dérivation. +] + +#slide[ + = Dérivation (OCaml) + + Les PPX permettent de transformer le code source avant la compilation + + ```ocaml + type couleur = Rouge | Vert | Bleu | RGB of int * int * int + [@@deriving show] + + (* val show : couleur -> string + val pp_couleur : Format.formatter -> couleur -> unit *) + ``` +] + +#slide[ + = Dérivation (Rust) + + Les macros permettent de transformer le code source avant la compilation + + ```rust + #[derive(Debug)] + struct Point { + x: i32, + y: i32, + } + ``` +] + + + + #slide[ + = Runtime Errors + + Analyseurs sans faux négatifs: + + #align( + center, + table( + columns: (auto, auto), + align: left, + align(center)[*Langage*], + align(center)[*Analyseurs*], + [C], [#astree, #eclair, #framac, #polyspace, #tisanalyser], + [C++], [#astree (C++17), #framac (?)], + [Ada], [#codepeer, #polyspace, #spark], + [Scade], [Scade suite ?, + outils C/Ada sur le code généré], + [OCaml], [], + [Rust], [(Mirai)], + ) + ) + ] + + #slide[ + = Formalisation + + Il y a globalement deux approches : + + - Par transpilation de ou vers Coq (ou autre) + - Langage $=>$ Coq $=>$ Preuves (Hoare, WP) + - Coq + Preuves $=>$ Langage + - Par annotation et preuve (semi) automatiques: + #[ + #set text(size: 16pt) + ```c + /*@ requires \valid(a) && \valid(b); + @ ensures A: *a == \old(*b) ; + @ ensures B: *b == \old(*a) ; + @ assigns *a,*b ; + @*/ + void swap(int *a,int *b); + ``` + ] + ] + + +#slide[ + = WCET + + Le WCET par analyse statique fonctionne par analyse du binaire avec les + contraintes de l'architecture cible. + #align( + center, + table( + columns: (auto, auto), + align: left, + align(center)[*Langage*], + align(center)[*Analyseurs*], + [C], [#chronos, #bound-T, #aiT, #sweet, #otawa, #rapidtime], + [C++], [outils C], + [Ada], [#rapidtime, #aiT], + [Scade], [#aiT], + [OCaml], [outils C], + [Rust], [outils C], + ) + ) +] + +#slide[ + = Pile + + L'analyse statique de la pile fonctionne également par analyse du + binaire: + #align( + center, + table( + columns: (auto, auto), + align: left, + align(center)[*Langage*], + align(center)[*Analyseurs*], + [C], [#stackanalyser, #armlink, #gcc], + [C++], [outils du C], + [Ada], [#gnatstack], + [Scade], [#stackanalyser], + [OCaml], [outils du C (natif)], + [Rust], [outils du C], + ) + ) +] + +#slide[ + = Qualité numérique + + #align( + center, + table( + columns: (auto, auto, auto), + align: left, + align(center)[*Langage*], + align(center)[*Analyseurs statiques*], + align(center)[*Calcul dynamique*], + [C], [#fluctuat, #astree, #polyspace, #gappa (+ annotations)], [#cadna, #mpfr, #gmp], + [C++], [#astree, #polyspace], [#cadna, #mpfr, #boost, #xsc], + [Ada], [_builtin_, #polyspace, #spark (+annotations)], [#mpfr, #gmp], + [Scade], [], [Scade library ?], + [OCaml], [], [#mpfr, #gmp], + [Rust], [], [biblothèques, #mpfr, #gmp], + ) + ) + +] + +#slide[ + = Assurances + + #align( + center, + table( + columns: (auto, auto, auto), + align: left, + align(center)[*Langage*], + align(center)[*Intrinsèque*], + align(center)[*Externe*], + [C], [😨], [😊], + [C++], [😕], [😕], + [Ada], [😊], [😊], + [Scade], [😊], [😊], + [OCaml], [😊], [😨], + [Rust], [😊], [😕], + ) + ) +] + +#slide[ + + = Assurances / Coût (Sécurité) + + #align( + center, + table( + columns: (auto, auto, auto, auto), + align: left, + align(center)[*Langage*], + align(center)[*Intrinsèque*], + align(center)[*Externe*], + align(center)[*Coût*], + [C], [😨], [😊], [😨], + [C++], [😕], [😕], [😕], + [Ada], [😊], [😊], [😕], + [Scade], [😊], [😊], [😌], + [OCaml], [😊], [😨], [😊], + [Rust], [😊], [😕], [😕], + ) + ) +] + +#slide[ + + = Critique + + #align( + center, + table( + columns: (auto, auto), + align: left, + align(center)[*Langage*], + align(center)[*Domaines critiques*], + [C], [Tous], + [C++], [Tous], + [Ada], [Spatial, Aéronautique, Ferroviaire ], + [Scade], [Aéronautique, Ferroviaire, Nucléaire], + [OCaml], [Outillage (Astree, KCG, ...)], + [Rust], [], + ) + ) +] + +#slide[ + + = Conclusion + + - Quand on peut, privilégier les langages métiers + - OCaml est souvent un bon choix pour l'outillage + - Rust est à la mode mais encore jeune pour être recommandé sans réserve + - Innover pour s'adapter aux nouveaux besoins/contraintes + +] + +#slide[ + + #v(3cm) + #align(center)[*Questions ?*] + +] \ No newline at end of file diff --git "a/src/\303\251tude/Ada.typ" "b/src/\303\251tude/Ada.typ" index 8c52d35..95d7604 100644 --- "a/src/\303\251tude/Ada.typ" +++ "b/src/\303\251tude/Ada.typ" @@ -157,10 +157,6 @@ ], pile: [ - #let gnatstack = link( - "https://www.adacore.com/gnatpro/toolsuite/gnatstack", - "GNATstack" - ) Les outils analysant l'exécutable peuvent le faire tout autant pour les programmes #Ada. Pour les outils ciblant spécifiquement #Ada, il y @@ -369,24 +365,6 @@ tests: [ - #let aunit = link("https://github.com/AdaCore/aunit", "AUnit") - #let adatest95 = link( - "https://www.qa-systems.fr/tools/adatest-95/", - "Ada Test 95" - ) - #let avhen = link("http://ahven.stronglytyped.org/", "Avhen") - #let ldra = link("https://ldra.com/products/ldra-tool-suite/", "LDRA") - #let vectorcastAda = link( - "https://www.vector.com/int/en/products/products-a-z/software/vectorcast/vectorcast-ada/", - "VectorCAST/Ada" - ) - - - #let rtrt = link( - "https://www.ibm.com/products/rational-test-realtime", - "Rational Test RealTime" - ) - Les différents outils de tests recensés pour #Ada sont inddiqués dans la @ada-test. @@ -401,7 +379,7 @@ [*#vectorcastAda*], [UC], [++], [✓], [✓], [*#rtrt*], [UIC], [], [], [], ), - caption: [Comparaison des outils de tests pour le langage C], + caption: [Comparaison des outils de tests pour le langage #Ada], ) #aunit et #avhen sont des implémentations xUnit pour #Ada. Les fonctionnalités sont @@ -446,24 +424,6 @@ Parmi tous les compilateurs Ada, nous listons uniquement ceux qui semblent maintenus et de qualité industrielle. - #let ptcdobjada = link( - "https://www.ptc.com/en/products/developer-tools/objectada", - "PTC ObjectAda" - ) - #let ptcapexada = link( - "https://www.ptc.com/en/products/developer-tools/apexada", - "PTC ApexAda" - ) - #let gnatpro = link("https://www.adacore.com/gnatpro", "GNAT Pro") - #let gnatllvm = link("https://github.com/AdaCore/gnat-llvm", "GNAT LLVM") - #let gaoc = link( - "https://www.ghs.com/products/ada_optimizing_compilers.html", - "GreenHills Ada Optimizing Compiler") - - #let janusada = link( - "http://www.rrsoftware.com/html/blog/ja-312-rel.html", - "Janus/Ada" - ) #figure( diff --git "a/src/\303\251tude/C++.typ" "b/src/\303\251tude/C++.typ" index a726be2..25cada9 100644 --- "a/src/\303\251tude/C++.typ" +++ "b/src/\303\251tude/C++.typ" @@ -207,11 +207,6 @@ va en partie dépendre de l'utilisation d'outils tiers. tests: [ -#let boost_test = link( - "https://www.boost.org/doc/libs/1_85_0/libs/test/doc/html/index.html", - [Boost Test Library] -) -#let catch2 = link("https://github.com/catchorg/Catch2", "Catch2") Certains des outils cités pour le C fonctionnent également pour le C++. C'est le cas pour #cantata ou #parasoft par exemple. D'autres outils ou bibliothèques @@ -223,13 +218,6 @@ les rapports de test ou les possibilités de _fuzzing_. Le _mocking_ est également disponible via une extension. #catch2 propose sensiblement la même chose que #boost_test. -#let gtest = link("https://github.com/google/googletest", "Google Test") -#let google = link("https://about.google", "Google") - -#let safetynet = link( - "https://bitbucket.org/rajinder_yadav/safetynet/src/master/", - "Safetynet" -) #gtest est un cadre logiciel proposé par #google pour le test unitaire. Il est très complet et utilisé pour de gros projets. Il permet de découvrir les @@ -246,11 +234,6 @@ Ruby. L'outil semble cependant moins mature et complet que #gtest. conjointement avec d'autres outils de tests unitaires pour simuler des comportements de fonctions ou de classes à la manière de #opmock. -#let testwell_ctc = link( - "https://www.verifysoft.com/fr_ctcpp.html", - "Testwell CTC++" -) - #testwell_ctc est un outil commercial qui, comme #cantata, #parasoft ou #vectorcast que nous avons déjà présenté dans la partie C, couvre différents types de tests diff --git "a/src/\303\251tude/C.typ" "b/src/\303\251tude/C.typ" index 5e620a2..9c3cfa5 100644 --- "a/src/\303\251tude/C.typ" +++ "b/src/\303\251tude/C.typ" @@ -463,6 +463,7 @@ propre à une utilisation dans le domaine critique. des systèmes d'exploitation et des architectures. Pour simplifier la lecture de ce document, nous ne listons ici que les principaux débugueurs connus. + #figure( table( columns: (auto, auto, auto), @@ -471,9 +472,11 @@ de ce document, nous ne listons ici que les principaux débugueurs connus. [*#gdb*], [x86, x86-64, ARM, PowerPC, SPARC, ...], [GPLv3], [*#lldb*], [i386, x86-65, AArch64, ARM], [Apache v2], [*#totalview*], [x86-64, ARM64, CUDA], [Propriétaire], - [*#undo*], [?], [Propriétaire], + [*#undo*], [x86-64], [Propriétaire], [*#valgrind*], [x86, x86-64, PowerPC, ARMv7], [GPL], [*#vsd*], [x86, x86-64], [Propriétaire], + [*#windbg*], [x86, x86-64], [Gratuit], + [*#rr*], [x86, x86-64, ARM], [GPLv2], ) ) @@ -510,6 +513,13 @@ qu'il soit donc compatible avec toutes les architectures supportées par #gcc. #vsd est le débugueur associé à la suite de développement #visualstudio de #microsoft. Il est propriétaire et ne fonctionne que sous Windows mais offre un support avancé de tous les langages supportés par #visualstudio. +Il ne faut pas confondre #vsd avec #windbg qui est un débugueur plus bas +niveau pour les plateformes Windows et qui est gratuit. + +#rr est un débugueur qui propose la même interface que #gdb mais qui exécute +le code dans une machine virtuelle et permet de remonter dans le temps et rejouer +les exécutions de manière déterministe. Cela permet de débuguer plus facilement +les erreurs aléatoires. ], diff --git "a/src/\303\251tude/links.typ" "b/src/\303\251tude/links.typ" index ca7dfec..e1f2143 100644 --- "a/src/\303\251tude/links.typ" +++ "b/src/\303\251tude/links.typ" @@ -204,4 +204,72 @@ #let spark = link("https://www.adacore.com/about-spark", "SPARK") -#let cvc4 = link("https://cvc4.github.io/", "CVC4") \ No newline at end of file +#let cvc4 = link("https://cvc4.github.io/", "CVC4") + + +#let windbg = link("https://docs.microsoft.com/en-us/windows-hardware/drivers/debugger/debugger-download-tools")[WinDBG] +#let rr = link("https://rr-project.org/")[rr] + +#let boost_test = link( + "https://www.boost.org/doc/libs/1_85_0/libs/test/doc/html/index.html", + [Boost Test Library] +) +#let catch2 = link("https://github.com/catchorg/Catch2", "Catch2") + +#let gtest = link("https://github.com/google/googletest", "Google Test") +#let google = link("https://about.google", "Google") + +#let safetynet = link( + "https://bitbucket.org/rajinder_yadav/safetynet/src/master/", + "Safetynet" +) + + +#let testwell_ctc = link( + "https://www.verifysoft.com/fr_ctcpp.html", + "Testwell CTC++" +) + + +#let aunit = link("https://github.com/AdaCore/aunit", "AUnit") +#let adatest95 = link( + "https://www.qa-systems.fr/tools/adatest-95/", + "Ada Test 95" +) +#let avhen = link("http://ahven.stronglytyped.org/", "Avhen") +#let ldra = link("https://ldra.com/products/ldra-tool-suite/", "LDRA") +#let vectorcastAda = link( + "https://www.vector.com/int/en/products/products-a-z/software/vectorcast/vectorcast-ada/", + "VectorCAST/Ada" +) + + +#let rtrt = link( + "https://www.ibm.com/products/rational-test-realtime", + "Rational Test RealTime" +) + + +#let ptcdobjada = link( + "https://www.ptc.com/en/products/developer-tools/objectada", + "PTC ObjectAda" +) +#let ptcapexada = link( + "https://www.ptc.com/en/products/developer-tools/apexada", + "PTC ApexAda" +) +#let gnatpro = link("https://www.adacore.com/gnatpro", "GNAT Pro") +#let gnatllvm = link("https://github.com/AdaCore/gnat-llvm", "GNAT LLVM") +#let gaoc = link( + "https://www.ghs.com/products/ada_optimizing_compilers.html", + "GreenHills Ada Optimizing Compiler") + +#let janusada = link( + "http://www.rrsoftware.com/html/blog/ja-312-rel.html", + "Janus/Ada" +) + +#let gnatstack = link( + "https://www.adacore.com/gnatpro/toolsuite/gnatstack", + "GNATstack" +)