Skip to content

GitLab

Commit b34e818c authored by Augustin Lemesle's avatar Augustin Lemesle
Browse files

Change to jekyll

parent bcec989b
Hide whitespace changes
Inline Side-by-side
404.html 0 → 100644
View file @ b34e818c
---
permalink: /404.html
layout: default
---
<style type="text/css" media="screen">
.container {
margin: 10px auto;
max-width: 600px;
text-align: center;
}
h1 {
margin: 30px 0;
font-size: 4em;
line-height: 1;
letter-spacing: -1px;
}
</style>
<div class="container">
<h1>404</h1>
<p><strong>Page not found :(</strong></p>
<p>The requested page could not be found.</p>
</div>
Gemfile 0 → 100644
View file @ b34e818c
source "https://rubygems.org"
# Hello! This is where you manage which Jekyll version is used to run.
# When you want to use a different version, change it below, save the
# file and run `bundle install`. Run Jekyll with `bundle exec`, like so:
#
# bundle exec jekyll serve
#
# This will help ensure the proper Jekyll version is running.
# Happy Jekylling!
gem "jekyll", "~> 4.0.0"
# This is the default theme for new Jekyll sites. You may change this to anything you like.
gem "minima", "~> 2.5"
# If you want to use GitHub Pages, remove the "gem "jekyll"" above and
# uncomment the line below. To upgrade, run `bundle update github-pages`.
# gem "github-pages", group: :jekyll_plugins
# If you have any plugins, put them here!
group :jekyll_plugins do
gem "jekyll-feed", "~> 0.12"
end
# Windows and JRuby does not include zoneinfo files, so bundle the tzinfo-data gem
# and associated library.
install_if -> { RUBY_PLATFORM =~ %r!mingw|mswin|java! } do
gem "tzinfo", "~> 1.2"
gem "tzinfo-data"
end
# Performance-booster for watching directories on Windows
gem "wdm", "~> 0.1.1", :install_if => Gem.win_platform?
Gemfile.lock 0 → 100644
View file @ b34e818c
GEM
remote: https://rubygems.org/
specs:
addressable (2.6.0)
public_suffix (>= 2.0.2, < 4.0)
colorator (1.1.0)
concurrent-ruby (1.1.5)
em-websocket (0.5.1)
eventmachine (>= 0.12.9)
http_parser.rb (~> 0.6.0)
eventmachine (1.2.7)
ffi (1.11.1)
forwardable-extended (2.6.0)
http_parser.rb (0.6.0)
i18n (1.6.0)
concurrent-ruby (~> 1.0)
jekyll (4.0.0)
addressable (~> 2.4)
colorator (~> 1.0)
em-websocket (~> 0.5)
i18n (>= 0.9.5, < 2)
jekyll-sass-converter (~> 2.0)
jekyll-watch (~> 2.0)
kramdown (~> 2.1)
kramdown-parser-gfm (~> 1.0)
liquid (~> 4.0)
mercenary (~> 0.3.3)
pathutil (~> 0.9)
rouge (~> 3.0)
safe_yaml (~> 1.0)
terminal-table (~> 1.8)
jekyll-feed (0.12.1)
jekyll (>= 3.7, < 5.0)
jekyll-sass-converter (2.0.0)
sassc (> 2.0.1, < 3.0)
jekyll-seo-tag (2.6.1)
jekyll (>= 3.3, < 5.0)
jekyll-watch (2.2.1)
listen (~> 3.0)
kramdown (2.1.0)
kramdown-parser-gfm (1.1.0)
kramdown (~> 2.0)
liquid (4.0.3)
listen (3.1.5)
rb-fsevent (~> 0.9, >= 0.9.4)
rb-inotify (~> 0.9, >= 0.9.7)
ruby_dep (~> 1.2)
mercenary (0.3.6)
minima (2.5.1)
jekyll (>= 3.5, < 5.0)
jekyll-feed (~> 0.9)
jekyll-seo-tag (~> 2.1)
pathutil (0.16.2)
forwardable-extended (~> 2.6)
public_suffix (3.1.1)
rb-fsevent (0.10.3)
rb-inotify (0.10.0)
ffi (~> 1.0)
rouge (3.9.0)
ruby_dep (1.5.0)
safe_yaml (1.0.5)
sassc (2.1.0)
ffi (~> 1.9)
terminal-table (1.8.0)
unicode-display_width (~> 1.1, >= 1.1.1)
thread_safe (0.3.6)
tzinfo (1.2.5)
thread_safe (~> 0.1)
tzinfo-data (1.2019.2)
tzinfo (>= 1.0.0)
unicode-display_width (1.6.0)
wdm (0.1.1)
PLATFORMS
ruby
DEPENDENCIES
jekyll (~> 4.0.0)
jekyll-feed (~> 0.12)
minima (~> 2.5)
tzinfo (~> 1.2)
tzinfo-data
wdm (~> 0.1.1)
BUNDLED WITH
2.0.2
_config.yml 0 → 100644
View file @ b34e818c
# Welcome to Jekyll!
#
# This config file is meant for settings that affect your whole blog, values
# which you are expected to set up once and rarely edit after that. If you find
# yourself editing this file very often, consider using Jekyll's data files
# feature for the data you need to update frequently.
#
# For technical reasons, this file is *NOT* reloaded automatically when you use
# 'bundle exec jekyll serve'. If you change this file, please restart the server process.
#
# If you need help with YAML syntax, here are some quick references for you:
# https://learn-the-web.algonquindesign.ca/topics/markdown-yaml-cheat-sheet/#yaml
# https://learnxinyminutes.com/docs/yaml/
#
# Site settings
# These are used to personalize your new site. If you look in the HTML files,
# you will see them accessed via {{ site.title }}, {{ site.email }}, and so on.
# You can create any custom variable you would like, and they will be accessible
# in the templates via {{ site.myvariable }}.
title: Your awesome title
email: your-email@example.com
description: >- # this means to ignore newlines until "baseurl:"
Write an awesome description for your new site here. You can edit this
line in _config.yml. It will appear in your document head meta (for
Google search results) and in your feed.xml site description.
baseurl: "" # the subpath of your site, e.g. /blog
url: "" # the base hostname & protocol for your site, e.g. http://example.com
twitter_username: jekyllrb
github_username: jekyll
# Build settings
theme: minima
plugins:
- jekyll-feed
include: ['html', '_plugins']
collections:
- plugins
# Exclude from processing.
# The following items will not be processed, by default.
# Any item listed under the `exclude:` key here will be automatically added to
# the internal "default list".
#
# Excluded items can be processed by explicitly listing the directories or
# their entries' file path in the `include:` list.
#
# exclude:
# - .sass-cache/
# - .jekyll-cache/
# - gemfiles/
# - Gemfile
# - Gemfile.lock
# - node_modules/
# - vendor/bundle/
# - vendor/cache/
# - vendor/gems/
# - vendor/ruby/
_includes/footer.html 0 → 100644
View file @ b34e818c
<footer id="footer" class="mainFooter">
<a href="/index.html" rel="home" class="footLogo" title="Frama-C"><img src="/assets/img/framac.gif"
alt=""></a>
<nav>
<a href="https://twitter.com/frama_c" target="_blank" class="twitterLink"><i class="icon icon-twitter"></i></a>
</nav>
<div class="copyright">
<span>Copyright © 2015-2018 Frama-C. All Rights Reserved.</span>
<ul id="menu-footer-menu" class="footer-list-menu">
<li id="menu-item-214" class="menu-item menu-item-type-post_type menu-item-object-page menu-item-214">
<a href="/html/terms-of-use.html">Terms Of Use</a>
</li>
<li id="menu-item-233" class="menu-item menu-item-type-post_type menu-item-object-page menu-item-233">
<a href="/html/authors.html">Authors</a>
</li>
</ul>
</div>
<div id="copyright" class="hide">
&copy 2019 Frama-C. All Rights Reserved.
</div>
</footer>
\ No newline at end of file
_includes/headers.html 0 → 100644
View file @ b34e818c
<header class="siteHeader" id="site_header">
<div id="header_iv_point" class="inviewTop"></div><span class="brandLogo"><a href="../index.html" rel="home" title=
"Frama-C"><img src="/assets/img/framac.gif" alt=""><span>Frama-C</span></a></span><a role="button" id=
"menu_toggle" class="menuToggle"><span class="open"><i></i><i></i><i></i></span><span class="close"><i></i><i></i></span></a>
<nav id="menu" role="navigation">
<div class="menu-primary-meny-container">
<ul id="menu-primary-meny" class="menu">
{% if include.header != null and include.header == 1 %}
<li id="menu-item-25" class=
"menu-item menu-item-type-post_type menu-item-object-page current-menu-item page_item page-item-12 current_page_item menu-item-25">
{% else %}
<li id="menu-item-25" class="menu-item menu-item-type-post_type menu-item-object-page menu-item-25">
{% endif %}
<a href="/html/using-frama-c.html">Using Frama C</a>
</li>
{% if include.header != null and include.header == 2 %}
<li id="menu-item-26" class=
"menu-item menu-item-type-post_type menu-item-object-page current-menu-item page_item page-item-16 current_page_item menu-item-26">
{% else %}
<li id="menu-item-26" class="menu-item menu-item-type-post_type menu-item-object-page menu-item-26">
{% endif %}
<a href="/html/kernel-plugin.html">Kernel &amp; Plugins</a>
</li>
{% if include.header != null and include.header == 3 %}
<li id="menu-item-27" class=
"menu-item menu-item-type-post_type menu-item-object-page current-menu-item page_item page-item-18 current_page_item menu-item-27">
{% else %}
<li id="menu-item-27" class="menu-item menu-item-type-post_type menu-item-object-page menu-item-27">
{% endif %}
<a href="/html/contact.html">Contact</a>
</li>
{% if include.header != null and include.header == 4 %}
<li id="menu-item-28" class=
"menu-item menu-item-type-post_type menu-item-object-page current-menu-item page_item page-item-20 current_page_item menu-item-28">
{% else %}
<li id="menu-item-28" class="menu-item menu-item-type-post_type menu-item-object-page menu-item-28">
{% endif %}
<a href="/html/documentation.html">Documentation</a>
</li>
{% if include.header != null and include.header == 5 %}
<li id="menu-item-29" class=
"menu-item menu-item-type-post_type menu-item-object-page current-menu-item page_item page-item-22 current_page_item menu-item-29">
{% else %}
<li id="menu-item-29" class="menu-item menu-item-type-post_type menu-item-object-page menu-item-29">
{% endif %}
<a href="/html/blog.html">Blog</a>
</li>
</ul>
</div><a role="button" href="/html/get-frama-c.html" id="header_download_link" class="btnDownload"><span><i class=
"icon icon-curly-left"></i><i class="icon icon-download-arrow"></i><i class="icon icon-curly-right"></i></span></a>
</nav>
</header>
\ No newline at end of file
_layouts/default.html 0 → 100644
View file @ b34e818c
<!DOCTYPE html>
<html lang="en-US" class="framac-site">
<head>
<meta charset="UTF-8">
<meta name="viewport" content="width=device-width,initial-scale=1,maximum-scale=1,user-sclable=no">
<title>{{ page.title }}</title>
<link rel="stylesheet" href="/assets/css/main.css">
<link rel="stylesheet" href="/assets/css/page.css">
<link rel="stylesheet" href="/assets/css/home.css">
<link rel="stylesheet" href="/assets/css/icomoon.css">
<link rel="stylesheet" href="/assets/css/default.css">
<link rel="stylesheet" href="/assets/css/blog.css">
<link rel="stylesheet" href="/assets/css/documentation.css">
{% if layout.css !=null %}
<link rel="stylesheet" href="/assets/css/{{ layout.css }}.css">
{% endif %}
{% if page.css !=null %}
<link rel="stylesheet" href="/assets/css/{{ page.css }}.css">
{% endif %}
<link rel="shortcut icon" href="/assets/img/favicon.ico" type="image/x-icon">
</head>
{{ content }}
</div>
<script type='text/javascript' src='/assets/js/manifest.js'></script>
<script type='text/javascript' src='/assets/js/lib.js'></script>
<script type='text/javascript'>
var ajax = {"url":"http:\/\/localhost:8000\/wp\/wp-admin\/admin-ajax.php","ajax_var":{"template_directory_uri":"http:\/\/localhost:8000\/app\/themes\/frama"},"apikey":"AIzaSyDwKjbfd43-rY5muMW76XUdAFMb7mL9kU8","nonce":"eb10361e5c"};
</script>
<script type='text/javascript' src='/assets/js/main.js'></script>
</body>
</html>
_layouts/plugin.html 0 → 100644
View file @ b34e818c
---
layout: default
css: plugin
---
<div id="wrapper" class="hfeed">
{% include headers.html %}
<div id="container" class="mainContainer">
<div class="pluginDetail">
<div class="tabs">
<div class="wrap">
<div class="goBackBtn">
<a class="goBack" href="../../kernel-plugin/index.html"><i class="icon-arrow-left"></i>Back</a>
</div><a class="tabLink active" href="../../kernel-plugin/index.html">Plugins</a> <em></em> <a class="tabLink" href=
"../../kernel/index.html">Kernel</a> <em></em> <a class="tabLink" href="../../gui/index.html">GUI</a>
</div>
</div>
<div class="pages">
<div class="bgTextbig">
Plugins
</div>
<div class="wrap">
{{ content }}
</div>
</div>
</div>
{% include footer.html %}
<div class="clear"></div>
</div>
</div>
_plugins/eva.html 0 → 100644
View file @ b34e818c
---
layout: default
css: plugin
title: Evolved Value Analysis (EVA) - Frama-C
---
<h2 class="subTitle">Evolved Value Analysis (EVA)</h2>
<figure class="pluginDetailThumb">
<img src="/assets/img/plugins/eva.png" alt="">
</figure>
<aside>
<p>Automatically computes variation domains for the variables of the program.</p>
</aside>
<dl class="defnitionList">
<dt class="subTitle">Value analysis based on abstract interpretation</dt>
<dd>
<p>The <b>Evolved Value Analysis</b> plug-in computes variation domains for variables. It is quite automatic,
although the user may guide the analysis in places. It handles a wide spectrum of C constructs. This plug-in uses
abstract interpretation techniques.</p>
<p>The results of <b>EVA</b> can be exploited directly in two ways.</p>
<ul>
<li>They can be used to infer the absence of run-time errors. The results are displayed in reverse, that is,
alarms are emitted for all the operations that could lead to a run-time error. If an alarm is not emitted for an
operation in the source code, then this operation is guaranteed not to cause a run-time error.</li>
<li>The Frama-C graphical user interface displays the inferred sets for possible values of a variable in each
point of the analyzed program.</li>
</ul>
<p>Maturity: industrialized.</p>
</dd>
<dt class="subTitle">Quick Start</dt>
<dd>
<p>The plug-in can be used both with the graphical user interface and in batch mode. In batch mode, the command
line may look like:</p>
<pre>
frama-c -val file1.c file2.c
</pre>
<p>A list of alarms (corresponding to possible run-time errors as computed by the analysis) is produced on the
standard output.</p>
<p>The results of <b>EVA</b> are used by many other plug-ins. In this cases, the analysis is initiated
automatically by the exploiting plug-in, but it is still possible to configure it for the case at hand (<i>e.g.</i>
through the same command-line options that would be used in conjunction with <tt>-val</tt>).</p>
</dd>
<dt class="subTitle">First Example</dt>
<dd>
<p>Consider the following function, in file <em>test.c</em>:</p>
<pre>
int abs(int x) {
if (x &lt; 0) return -x;
else return x;
}
</pre>
<p>On this code, Eva reports the possible integer overflow when <tt>x</tt> is the smallest negative integer by
emitting an alarm at line 2. The alarm is the ACSL assertion <tt>assert -x ≤ 2147483647;</tt> that guards against
the overflow.<br>
Eva also displays the possible values of the variables at the end of the function. Here, we can see that the result
is always positive.</p>
<pre>
$ frama-c -val test.c -main abs
[…]
mytests/test.c:2:[value] warning: signed overflow. assert -x ≤ 2147483647;
[value] done for function abs
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function abs:
__retres ∈ [0..2147483647]
</pre>
<p>One can also inspect in the graphical interface of Frama-C the alarms emitted by Eva, as well as the possible
values inferred at each program point.</p>
</dd>
<dt class="subTitle">Technical Notes</dt>
<dd>
<p>Recursive calls are currently not supported.</p>
<p>Only sequential code can be analyzed at this time.</p>
</dd>
<dt class="subTitle">Further Readings</dt>
<dd>
<p>The options to configure the analysis as well as the syntax of the results are described in the <a class="plain"
href="http://frama-c.com/download/frama-c-value-analysis.pdf">EVA user manual</a>.</p>
</dd>
<dt class="subTitle"></dt>
<dd></dd>
</dl>
\ No newline at end of file
_plugins/eva2.html 0 → 100644
View file @ b34e818c
---
layout: default
css: plugin
title: Evolved Value Analysis (EVA) - Frama-C
---
<h2 class="subTitle">Evolved Value Analysis (EVA)</h2>
<figure class="pluginDetailThumb">
<img src="/assets/img/plugins/eva.png" alt="">
</figure>
<aside>
<p>Automatically computes variation domains for the variables of the program.</p>
</aside>
<dl class="defnitionList">
<dt class="subTitle">Value analysis based on abstract interpretation</dt>
<dd>
<p>The <b>Evolved Value Analysis</b> plug-in computes variation domains for variables. It is quite automatic,
although the user may guide the analysis in places. It handles a wide spectrum of C constructs. This plug-in uses
abstract interpretation techniques.</p>
<p>The results of <b>EVA</b> can be exploited directly in two ways.</p>
<ul>
<li>They can be used to infer the absence of run-time errors. The results are displayed in reverse, that is,
alarms are emitted for all the operations that could lead to a run-time error. If an alarm is not emitted for an
operation in the source code, then this operation is guaranteed not to cause a run-time error.</li>
<li>The Frama-C graphical user interface displays the inferred sets for possible values of a variable in each
point of the analyzed program.</li>
</ul>
<p>Maturity: industrialized.</p>
</dd>
<dt class="subTitle">Quick Start</dt>
<dd>
<p>The plug-in can be used both with the graphical user interface and in batch mode. In batch mode, the command
line may look like:</p>
<pre>
frama-c -val file1.c file2.c
</pre>
<p>A list of alarms (corresponding to possible run-time errors as computed by the analysis) is produced on the
standard output.</p>
<p>The results of <b>EVA</b> are used by many other plug-ins. In this cases, the analysis is initiated
automatically by the exploiting plug-in, but it is still possible to configure it for the case at hand (<i>e.g.</i>
through the same command-line options that would be used in conjunction with <tt>-val</tt>).</p>
</dd>
<dt class="subTitle">First Example</dt>
<dd>
<p>Consider the following function, in file <em>test.c</em>:</p>
<pre>
int abs(int x) {
if (x &lt; 0) return -x;
else return x;
}
</pre>
<p>On this code, Eva reports the possible integer overflow when <tt>x</tt> is the smallest negative integer by
emitting an alarm at line 2. The alarm is the ACSL assertion <tt>assert -x ≤ 2147483647;</tt> that guards against
the overflow.<br>
Eva also displays the possible values of the variables at the end of the function. Here, we can see that the result
is always positive.</p>
<pre>
$ frama-c -val test.c -main abs
[…]
mytests/test.c:2:[value] warning: signed overflow. assert -x ≤ 2147483647;
[value] done for function abs
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function abs:
__retres ∈ [0..2147483647]
</pre>
<p>One can also inspect in the graphical interface of Frama-C the alarms emitted by Eva, as well as the possible
values inferred at each program point.</p>
</dd>
<dt class="subTitle">Technical Notes</dt>
<dd>
<p>Recursive calls are currently not supported.</p>
<p>Only sequential code can be analyzed at this time.</p>
</dd>
<dt class="subTitle">Further Readings</dt>
<dd>
<p>The options to configure the analysis as well as the syntax of the results are described in the <a class="plain"
href="http://frama-c.com/download/frama-c-value-analysis.pdf">EVA user manual</a>.</p>
</dd>
<dt class="subTitle"></dt>
<dd></dd>
</dl>
\ No newline at end of file
_posts/2019-08-22-welcome-to-jekyll.markdown 0 → 100644
View file @ b34e818c
---
layout: post
title: "Welcome to Jekyll!"
date: 2019-08-22 13:59:15 +0200
categories: jekyll update
---
You’ll find this post in your `_posts` directory. Go ahead and edit it and re-build the site to see your changes. You can rebuild the site in many different ways, but the most common way is to run `jekyll serve`, which launches a web server and auto-regenerates your site when a file is updated.
Jekyll requires blog post files to be named according to the following format:
`YEAR-MONTH-DAY-title.MARKUP`
Where `YEAR` is a four-digit number, `MONTH` and `DAY` are both two-digit numbers, and `MARKUP` is the file extension representing the format used in the file. After that, include the necessary front matter. Take a look at the source for this post to get an idea about how it works.
Jekyll also offers powerful support for code snippets:
{% highlight ruby %}
def print_hi(name)
puts "Hi, #{name}"
end
print_hi('Tom')
#=> prints 'Hi, Tom' to STDOUT.
{% endhighlight %}
Check out the [Jekyll docs][jekyll-docs] for more info on how to get the most out of Jekyll. File all bugs/feature requests at [Jekyll’s GitHub repo][jekyll-gh]. If you have questions, you can ask them on [Jekyll Talk][jekyll-talk].
[jekyll-docs]: https://jekyllrb.com/docs/home
[jekyll-gh]: https://github.com/jekyll/jekyll
[jekyll-talk]: https://talk.jekyllrb.com/
_site/404.html 0 → 100644
View file @ b34e818c
<!DOCTYPE html>
<html lang="en-US" class="framac-site">
<head>
<meta charset="UTF-8">
<meta name="viewport" content="width=device-width,initial-scale=1,maximum-scale=1,user-sclable=no">
<title></title>
<link rel="stylesheet" href="/assets/css/main.css">
<link rel="stylesheet" href="/assets/css/page.css">
<link rel="stylesheet" href="/assets/css/home.css">
<link rel="stylesheet" href="/assets/css/icomoon.css">
<link rel="stylesheet" href="/assets/css/default.css">
<link rel="stylesheet" href="/assets/css/blog.css">
<link rel="stylesheet" href="/assets/css/documentation.css">
<link rel="shortcut icon" href="/assets/img/favicon.ico" type="image/x-icon">
</head>
<style type="text/css" media="screen">
.container {
margin: 10px auto;