diff --git a/html/kernel.html b/html/kernel.html index 213cd99b5a60f087ec72c8abad149661177d5543..ecb256a9340c39bd6159b9278df0a63ddeab4cda 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.