From 1ace0fe38d4d478bf24c948d94bc24c7c4e4c831 Mon Sep 17 00:00:00 2001 From: Allan Blanchard <allan.blanchard@cea.fr> Date: Mon, 11 May 2020 12:35:43 +0200 Subject: [PATCH] Links in Kernel page --- html/kernel.html | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/html/kernel.html b/html/kernel.html index 213cd99b..ecb256a9 100755 --- a/html/kernel.html +++ b/html/kernel.html @@ -7,12 +7,12 @@ active: 2 <p>The Frama-C platform allows checking security, verifying requirement and guaranteeing trust in C programs, thanks to a collection of collaborative - <a href="https://frama-c.frama-c.com/html/kernel-plugin.html">plugins</a> that + <a href="/html/kernel-plugin.html">plugins</a> that perform static analysis, deductive verification, and testing, for safety- and security-critical software. Collaborative verification across cooperating plug-ins is enabled by their integration on top of a shared kernel and datastructures, and their compliance to - <a href="https://frama-c.frama-c.com/html/acsl.html">a common specification language</a>. + <a href="/html/acsl.html">a common specification language</a>. </p> <h1>Architecture</h1> @@ -20,7 +20,7 @@ active: 2 <a href="https://link.springer.com/chapter/10.1007/3-540-45937-5_16">CIL</a>. CIL is a front-end for C that parses ISO C99 programs into a normalized representation. Frama-C extends CIL to support - <a href="https://frama-c.frama-c.com/html/acsl.html">ACSL</a>. + <a href="/html/acsl.html">ACSL</a>. This modified CIL front-end produces the C + ACSL abstract syntax tree (AST), an abstract view of the program shared among all analyzers. In addition to the AST, the kernel provides several general services. -- GitLab