Skip to content
Snippets Groups Projects
Commit 1ace0fe3 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

Links in Kernel page

parent f49304f3
No related branches found
No related tags found
1 merge request!34Acsl and kernel pages
......@@ -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.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment