Skip to content
Snippets Groups Projects
index.html 10.4 KiB
Newer Older
Augustin Lemesle's avatar
Augustin Lemesle committed
---
css: home
layout: default
title: Frama-C
---
Augustin Lemesle's avatar
Augustin Lemesle committed

<body class="home page-template-default page page-id-7 nonTouch">
  <div id="wrapper" class="hfeed">
Augustin Lemesle's avatar
Augustin Lemesle committed
	{% include headers.html %}
Augustin Lemesle's avatar
Augustin Lemesle committed

    <div id="container" class="mainContainer">
      <div class="pageContent titleIn secure" id="content" role="main">
        <section class="section fullScreen verticalFlex">
Augustin Lemesle's avatar
Augustin Lemesle committed
          <div class="sectionContent">
            <h2 class="banner-title">A platform to make your C and C++ code safer and more secure</h2>

            <p class="banner-desc">
              Frama-C is an open-source extensible and collaborative platform dedicated to
              source-code analysis of C and C++ software. The Frama-C analyzers assist you
              in various source-code-related activities, from the navigation through
              unfamiliar projects up to the certification of critical software.
            </p>
            <a class="btn cta-download" href="/html/get-frama-c.html"><span>Download <b>Frama-C</b><span><i class=
Augustin Lemesle's avatar
Augustin Lemesle committed
            "icon icon-curly-left"></i><i class="icon icon-download-arrow"></i><i class=
            "icon icon-curly-right"></i></span></span></a>
Augustin Lemesle's avatar
Augustin Lemesle committed
          </div>
Augustin Lemesle's avatar
Augustin Lemesle committed

        </section>

        <section class="section fullScreen codeDemoScreen textCenter">
Augustin Lemesle's avatar
Augustin Lemesle committed
          <div class="sectionContent">
Augustin Lemesle's avatar
Augustin Lemesle committed
            <h3>Overview of a Frama-C analysis for<br>
Augustin Lemesle's avatar
Augustin Lemesle committed
            a simple C program</h3>

            <div class="slideHeader">
              <h4>Browsing the analysis results with Frama-C</h4>

              <div id="home_code_swiper" class="tabSlider swiper-container">
                <div class="sliderWrapper swiper-wrapper">
                  <div class="swiper-slide">
                    <div role="button" class="slideTxt" target="tab_0">
                      <span>Interface Overview</span>
Augustin Lemesle's avatar
Augustin Lemesle committed
                    </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
                  </div>

                  <div class="swiper-slide">
                    <div role="button" class="slideTxt" target="tab_1">
                      <span>Value Analysis</span>
Augustin Lemesle's avatar
Augustin Lemesle committed
                    </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
                  </div>

                  <div class="swiper-slide">
                    <div role="button" class="slideTxt" target="tab_2">
                      <span>Effects Analysis</span>
Augustin Lemesle's avatar
Augustin Lemesle committed
                    </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
                  </div>

                  <div class="swiper-slide">
                    <div role="button" class="slideTxt" target="tab_3">
                      <span>Dependency Analysis</span>
Augustin Lemesle's avatar
Augustin Lemesle committed
                    </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
                  </div>

                  <div class="swiper-slide">
                    <div role="button" class="slideTxt" target="tab_4">
                      <span>Impact Analysis</span>
Augustin Lemesle's avatar
Augustin Lemesle committed
                    </div>
                  </div>
                </div>
Augustin Lemesle's avatar
Augustin Lemesle committed

Augustin Lemesle's avatar
Augustin Lemesle committed
                <div class="swiper-button-prev" style="color: #f7931c"></div>
Augustin Lemesle's avatar
Augustin Lemesle committed

Augustin Lemesle's avatar
Augustin Lemesle committed
                <div class="swiper-button-next" style="color: #f7931c"></div>
Augustin Lemesle's avatar
Augustin Lemesle committed
              </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
            </div>

            <div class="codeDemoBlock">
              <div id="home_code_detail_swiper" class="swiper-container">
                <div class="swiper-wrapper">
                  <div class="swiper-slide">
                    <div class="sidetext">
Augustin Lemesle's avatar
Augustin Lemesle committed
                      <div>
                        <p>When invoked with the above command-line, Frama-C
                           creates an analysis project for the file first.c.
                        </p>
                        <p>The <tt>-val</tt> option on the command-line causes the value
                           analysis plug-in to run and have its results ready
                           before the interface appears.
                        </p>
                        <p>The <tt>-slevel</tt> option is one of several options that
                           influence the precision of the value analysis. The
                           actions of creating new analysis projects and
                            activating plug-ins can also be done interactively.
                        </p>
                      </div>
                    </div>
                    <img class="sideimg" src="/assets/img/home/gui-overview.png">
Augustin Lemesle's avatar
Augustin Lemesle committed
                  </div>
                  <div class="swiper-slide">
                    <div class="sidetext">
Augustin Lemesle's avatar
Augustin Lemesle committed
                      <div>
                        <p>The value analysis 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>
                        <p>When the execution reaches this point inside the loop,
                           the variable <tt>S</tt> always contains either 0, 1, 3, or 6.
                        </p>
                      </div>
                    </div>
                    <img class="sideimg" src="/assets/img/home/value-analysis.png">
Augustin Lemesle's avatar
Augustin Lemesle committed
                  </div>
                  <div class="swiper-slide">
                    <div class="sidetext">
Augustin Lemesle's avatar
Augustin Lemesle committed
                      <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>
                        <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>
                      </div>
                    </div>
                    <img class="sideimg" src="/assets/img/home/effect-analysis.png">
Augustin Lemesle's avatar
Augustin Lemesle committed
                  </div>
                  <div class="swiper-slide">
                    <div class="sidetext">
Augustin Lemesle's avatar
Augustin Lemesle committed
                      <div>
                        <p>The dependencies plug-in makes use of the results of
                           the value analysis plug-in to highlight the statements
                           that define the value of variable <tt>S</tt> at the selected
                           program point.
                        </p>
                        <p>The value contained in variable <tt>S</tt> at the statement
                           <tt>*tmp = S;</tt> was defined by the statement
                           <tt>S += i;</tt>.
                        </p>
                      </div>
                    </div>
                    <img class="sideimg" src="/assets/img/home/dep-analysis.png">
Augustin Lemesle's avatar
Augustin Lemesle committed
                  </div>
                  <div class="swiper-slide">
                    <div class="sidetext">
Augustin Lemesle's avatar
Augustin Lemesle committed
                      <div>
                        <p>This analysis highlights in green all the statements
                           impacted by the selected statement.
                        </p>
                        <p>The statement <tt>p = T;</tt> has repercussions on the statements
                           <tt>tmp = p; p++; *tmp = S;</tt>.
                        </p>
                        <p>It is guaranteed not to affect the statements <tt>S += i;</tt>
                           and <tt>i ++;</tt>.
                        </p>
                      </div>
                    </div>
                    <img class="sideimg" src="/assets/img/home/impact-analysis.png">
Augustin Lemesle's avatar
Augustin Lemesle committed
                  </div>
                </div>
              </div>
            </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
          </div>
        </section>

        <section id="latest_events" class="section fullScreen calendarScreen" data-title="TIMELINE">
Augustin Lemesle's avatar
Augustin Lemesle committed
          <div class="sectionContent">
            <h3>Frama-C Timeline</h3>
Augustin Lemesle's avatar
Augustin Lemesle committed

            <div class="eventScaleBlock">
              <div class="scaleBg">
                <u></u>
              </div>

              <div id="event_calender_swiper" class="swiper-container">
                <div class="swiper-wrapper">
                  {% for event in site.events %}
                  <div class="swiper-slide">
                    <a role="button" class="eventLink"><time>{{ event.date | date: "<b>%Y</b>" }}</time><span>{{ event.event }}</span></a>
                  </div>
                  {% endfor %}
                </div>
              </div>
            </div>

            <div id="events_iv_point" class="inviewCenter"></div>

Augustin Lemesle's avatar
Augustin Lemesle committed
            <div id="event_detail_swiper" class="eventDetailsBlock swiper-container">
              <div class="swiper-wrapper">
                {% for event in site.events %}
Augustin Lemesle's avatar
Augustin Lemesle committed
                <div class="swiper-slide">
                  <div class="eventDetail">
Augustin Lemesle's avatar
Augustin Lemesle committed
                    <div class="contentBlk">
Allan Blanchard's avatar
Allan Blanchard committed
                      <time>{{ event.date | date: "<b>%B </b><b>%-d</b><small> %Y</small>" }}</time>
Augustin Lemesle's avatar
Augustin Lemesle committed
                        <h3>{{ event.title }}</h3>
Augustin Lemesle's avatar
Augustin Lemesle committed

Augustin Lemesle's avatar
Augustin Lemesle committed
                      </div>
                    </div>
                  </div>
                </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
              </div>
            </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
          </div>
        </section>

        <section class="section downloadSection fullScreen verticalFlex" data-title="DOWNLOAD">
Augustin Lemesle's avatar
Augustin Lemesle committed
          <div class="sectionContent">
            <div class="head">
              <h3>Get Frama-C</h3>

              <nav>
Augustin Lemesle's avatar
Augustin Lemesle committed
                <span class="currentVersion">Latest Version</span><a role="button" href="/html/get-frama-c.html">{{ site.fc-versions.last.name }}</a><a href="/html/framac-versions.html" class="previousVersion">Previous Versions</a>
Augustin Lemesle's avatar
Augustin Lemesle committed
              </nav>
Augustin Lemesle's avatar
Augustin Lemesle committed
            </div>
Augustin Lemesle's avatar
Augustin Lemesle committed

            <div class="linkBlk">
Augustin Lemesle's avatar
Augustin Lemesle committed
              <p>Frama-C is only available for Desktop</p><a class="btn mobileLink" href="/html/get-frama-c.html"><span>Discover
              more about <b>Frama-C</b></span></a> <a class="btn cta-download" href="/html/get-frama-c.html"><span>Download
Augustin Lemesle's avatar
Augustin Lemesle committed
              <b>Frama-C</b><span><i class="icon icon-curly-left"></i><i class="icon icon-download-arrow"></i><i class=
              "icon icon-curly-right"></i></span></span></a>
Augustin Lemesle's avatar
Augustin Lemesle committed
            </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
          </div>

          <div id="download_iv_point" class="inviewCenter"></div>
        </section>
Augustin Lemesle's avatar
Augustin Lemesle committed
      {% include footer.html %}
      <div class="clear"></div>
Augustin Lemesle's avatar
Augustin Lemesle committed
    </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
  </div>
Augustin Lemesle's avatar
Augustin Lemesle committed
  <script type='text/javascript' src='/assets/js/swiper.js'></script>
  <head><script type='text/javascript' src='/assets/js/main.js'></script></head>