Commit 22fdb978 authored by François Bobot's avatar François Bobot
Browse files

Write a Katex formula

parent 8ac2d05a
---
layout: default
date: 01-01-2000
date: 01-09-2000
short_title: First COLIBRI
title: Start of the development of COLIBRI
link: /fc-plugins/frama-clang.html
......
This source diff could not be displayed because it is stored in LFS. You can view the blob instead.
This source diff could not be displayed because it is stored in LFS. You can view the blob instead.
......@@ -86,56 +86,40 @@ description: "Colibri - A family of Constraint Solvers"
<div class="swiper-slide">
<div class="sidetext">
<div>
<p>When invoked with the command-line: </p>
<pre>frama-c -eva -eva-precision 1 first.c</pre>
<p>Frama-C
creates an analysis project for the file first.c.
<p>COLIBRI good for because
</p>
<p>The <tt>-eva</tt> option on the command-line causes
the Eva plug-in to run and have its results ready
before the interface appears.
</p>
<p>The <tt>-eva-precision</tt> option is one of several
options that influence the precision of the Eva
plug-in. The actions of creating new analysis
projects and activating plug-ins can also be done
interactively.
<p> Example:
{% katex display %}
c = \pm\sqrt{a^2 + b^2}
{% endkatex %}
x-y=0.1 => x \in [..;..] /\ y \in [..,..]
</p>
</div>
</div>
<img class="sideimg" src="/assets/img/home/gui-overview.png">
<img class="sideimg" src="/assets/img/colibri/interreduction.png">
</div>
<div class="swiper-slide">
<div class="sidetext">
<div>
<p>The Eva plug-in computes sets of possible
values for every variable at each point of the program.
When providing such results, Frama-C guarantees that the
variable does not take at that point any value other
than those listed.
<p>COLIBRI good for because
</p>
<p>When the execution reaches this point inside the loop,
the variable <tt>S</tt> always contains either 0, 1, 3, or 6.
<p> Example: x-y=0.1 => x \in [..;..] /\ y \in [..,..]
</p>
</div>
</div>
<img class="sideimg" src="/assets/img/home/value-analysis.png">
<img class="sideimg" src="/assets/img/colibri2/framework.svg">
</div>
<div class="swiper-slide">
<div class="sidetext">
<div>
<p>For each statement, Frama-C can provide an exhaustive
list of the memory cells that may be modified by this
statement during the execution, even if the statement
uses pointers.
<p>Colibrics proved in why3
</p>
<p>Frama-C guarantees that anytime it is executed, the
statement <tt>*tmp = S;</tt> does not change any memory location
other than the cells of the array <tt>T</tt>.
<p>
</p>
</div>
</div>
<img class="sideimg" src="/assets/img/home/effect-analysis.png">
<img class="sideimg" src="/assets/img/colibrics/proof.svg">
</div>
</div>
</div>
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment