-
Allan Blanchard authoredAllan Blanchard authored
using-frama-c.html 4.90 KiB
---
layout: default
title: Using Frama-C - Frama-C
css: plugin
---
<body class="page-template page-template-page-usingFramac page-template-page-usingFramac-php page page-id-12 nonTouch">
<div id="wrapper" class="hfeed">
{% include headers.html header="using" %}
<div id="container" class="mainContainer">
<div class="defaultPage usagePage" id="content" role="main">
<article id="post-12" class="post-12 page type-page status-publish hentry">
<h1 class="entry-title hide">Using Frama-C</h1>
<section class="articleContent">
<div class="usagePageContent">
<div class="codeDemoHead usageCodeDemo">
<figure>
<img src="/assets/img/using-framac-img.png" alt=
"Using Frama-C">
</figure>
</div>
<div class="contentWrap">
<div class="paragraphGroup">
<h3>Using Frama-C to grasp source code internals</h3>
<p>The C language has been in use for a long time, and numerous programs today make use of C routines. This
ubiquity is due to historical reasons, and to the fact that C is well adapted for a significant number of
applications (e.g. embedded code). However, the C language exposes many notoriously awkward constructs.</p>
<p><b>Many Frama-C plug-ins are able to reveal what the analyzed C code actually does. Equipped with Frama-C, you
can:</b></p>
<div class="tabsBlock">
<details>
<summary>
Observe sets of possible values for the variables of the program at each point of the execution;
</summary>
</details>
<details>
<summary>
Slice the original program into simplified ones;
</summary>
</details>
<details>
<summary>
Navigate the dataflow of the program, from definition to use or from use to definition.
</summary>
</details>
</div>
</div>
<div id="">
<div class="paragraphGroup">
<h3>Proving formal properties for critical software</h3>
<p>Frama-C allows to verify that the source code complies with a provided formal specification. Functional
specifications can be written in a dedicated language, ACSL. The specifications can be partial, concentrating
on one aspect of the analyzed program at a time.</p>
<p>The most structured sections of your existing design documents can also be considered as formal
specifications. For instance, the list of global variables that a function is supposed to read from or write to
is a formal specification. Frama-C can compute this information automatically from the source code of the
function, allowing you to verify that the code satisfies this part of the design document, faster and with less
risks than a code review.</p> </div>
</div>
<!-- <div id="group_code_standards">
<div class="paragraphGroup">
<h3>Enforce code standards</h3>
</div>
</div>
<div id="group_security_defects">
<div class="paragraphGroup">
<h3>Detect security defects</h3>
</div>
</div> -->
</div>
<!--<div class="contentFluid recommendBlock">
<div class="contentWrap">
<h3>Case Studies</h3>
<div id="case_study_list" class="caseStudyList swiper-container">
<div class="swiper-wrapper">
{% for case_study in site.case_studies %}
<div class="swiper-slide">
<div class="caseStudyItem">
<div>
<h4>{{ case_study.title }}</h4>
<p>{{ case_study.content | strip_html | truncatewords: 50 }}</p><a href="{{ case_study.url }}" class="btn"><small>Discover More</small></a>
</div>
</div>
</div>
{% endfor %}
</div>
<div class="swiper-button-prev"></div>
<div class="swiper-button-next"></div>
</div>
</div>
</div>-->
</div>
</section>
</article>
</div>
{% include footer.html %}
<div class="clear"></div>
</div>
</div>
</body>