Merge branch 'master' of git.frama-c.com:pub/pub.frama-c.com

51e09ebf · Augustin Lemesle · 44b9a6a1 · 39c3dd28 · 51e09ebf · 51e09ebf
Commit 51e09ebf authored 5 years ago by Augustin Lemesle
--- a/_layouts/plugin.html
+++ b/_layouts/plugin.html
@@ -13,7 +13,7 @@ css: plugin
            <div>
              <a href="/html/kernel-plugin.html"><i class="icon-arrow-left"></i>Back</a>
            </div><a class="tabLink active" href="/html/kernel-plugin.html">Plugins</a> <em></em> <a class="tabLink" href=
-            "/html/kernel.html">Kernel</a> <em></em> <a class="tabLink" href="/html/gui.html">GUI</a>
+            "/html/kernel.html">Kernel</a> <em></em> <a class="tabLink" href="/html/acsl.html">ACSL</a>
          </div>
        </div>

--- a/html/acsl.html
+++ b/html/acsl.html
+---
+layout: default
+css: plugin
+title: ACSL
+---
+<body class="page-template page-template-page-kernel page-template-page-kernel-php page page-id-179 nonTouch">
+  <div id="wrapper" class="hfeed">
+	{% include headers.html %}
+    <div id="container" class="mainContainer">
+      <div class="tabs">
+        <div class="wrap">
+          <a class="tabLink" href="/html/kernel-plugin.html">Plugins</a> <em></em> <a class="tabLink" href=
+          "/html/kernel.html">Kernel</a> <em></em> <a class="tabLink active" href="/html/acsl.html">ACSL</a>
+        </div>
+      </div>
+      <div class="pageKernel pages">
+        <div class="bgTextbig">
+          ACSL
+        </div>
+        <div class="wrap">
+          <h1>ANSI/ISO C Specification Language</h1>
+          <p>The ANSI/ISO C Specification Langage (ACSL) is a behavioral
+            specification language for C programs. The design of ACSL is
+            inspired of <a class="extlink" href=
+                           "http://www.eecs.ucf.edu/~leavens/JML/index.shtml">JML</a>. It also
+            inherits a lot from the specification language of the source code
+            analyzer <a class="extlink" href=
+                        "http://caduceus.lri.fr/">Caduceus</a>, a previous development of
+            one of the partners in the Frama-C project.</p>
+          <p>ACSL can express a wide range of functional properties. The
+            paramount notion in ACSL is the function contract. <span class=
+                                                                     "slogan"><a class="pdf" href="download/acsl.pdf">ACSL<br />
+                Reference</a></span> While many software engineering experts
+            advocate the "function contract mindset" when designing complex
+            software, they generally leave the actual expression of the
+            contract to run-time assertions, or to comments in the source code.
+            ACSL is expressly designed for writing the kind of properties that
+            make up a function contract.</p>
+          <p>ACSL is a <em>formal</em> language. This means that the
+            specifications written in ACSL can be automatically manipulated by
+            helper programs, in the same way that a programming language is a
+            formal language manipulated by a compiler, and by opposition to
+            informally written comments that can only be useful to humans.</p>
+          <p>ACSL allows to write contracts that range from the low-level
+            (“<i>this function expects a valid pointer to int</i>”) to the
+            high-level (“<i>this function expects a nonempty linked list of
+              ints and returns the greatest of these ints</i>”). It is expressive
+            enough to write complete specifications for many functions, but it
+            can also be used for writing partial specifications. Partial
+            specifications, of which the “<i>expects a valid pointer to
+              int</i>” contract is a typical example, do not describe completely
+            the expected behavior of the function. <span class="slogan">ACSL
+              allows you to write<br />
+              complete specifications.<br />
+              But it does not force you to.</span> Function contracts written as
+            run-time assertions are almost always partial specifications,
+            because a complete specification would be too annoying to write in
+            the same language as the programming language (indeed, most often
+            this would mean programming the function a second time).</p>
+          <p><a href="jessie.html">Jessie</a> and <a href="wp.html">Wp</a>
+            plug-ins use Hoare-style weakest precondition computations to
+            formally prove ACSL properties. The process can be quite automatic,
+            thanks to external theorem provers such as Simplify, or Alt-Ergo,
+            or more interactive, with the use of the Coq proof-assistant. Other
+            plug-ins, such as the <a href="value.html">Eva</a> plug-in, may
+            also contribute to the verification of ACSL properties. They may
+            also report static analysis results in terms of asserted new ACSL
+            properties inside the source code.</p>
+        </div>
+      </div>
+      {% include footer.html %}
+      <div class="clear"></div>
+    </div>
+  </div>
+</body>
--- a/html/gui.html
+++ b/html/gui.html
---
-layout: default
-css: plugin
-title: GUI - Frama-C
---
-<body class="page-template page-template-page-kernel page-template-page-kernel-php page page-id-179 nonTouch">
-  <div id="wrapper" class="hfeed">
-	{% include headers.html %}
-    <div id="container" class="mainContainer">
-      <div class="tabs">
-        <div class="wrap">
-          <a class="tabLink" href="/html/kernel-plugin.html">Plugins</a> <em></em> <a class="tabLink" href=
-          "/html/kernel.html">Kernel</a> <em></em> <a class="tabLink active" href="/html/gui.html">GUI</a>
-        </div>
-      </div>
-      <div class="pageKernel pages">
-        <div class="bgTextbig">
-          GUI
-        </div>
-        <div class="wrap">
-		<p> Write something </p>
-        </div>
-      </div>
-	  {% include footer.html %}
-      <div class="clear"></div>
-    </div>
-  </div>
-</body>
--- a/html/kernel-plugin.html
+++ b/html/kernel-plugin.html
@@ -13,7 +13,7 @@ title: Kernel & Plugins - Frama-C
      <div class="tabs">
        <div class="wrap">
          <a class="active tabLink" href="kernel-plugin.html">Plugins</a> <em></em> <a class="tabLink" href=
-          "/html/kernel.html">Kernel</a> <em></em> <a class="tabLink" href="/html/gui.html">GUI</a>
+          "/html/kernel.html">Kernel</a> <em></em> <a class="tabLink" href="/html/acsl.html">ACSL</a>
          <div class="tabOptions">
            <div class="pluginSearch">

--- a/html/kernel.html
+++ b/html/kernel.html
@@ -14,7 +14,7 @@ title: Kernel & Plugins - Frama-C
      <div class="tabs">
        <div class="wrap">
          <a class="tabLink" href="/html/kernel-plugin.html">Plugins</a> <em></em> <a class="tabLink active" href=
-          "/html/kernel.html">Kernel</a> <em></em> <a class="tabLink" href="/html/gui.html">GUI</a>
+          "/html/kernel.html">Kernel</a> <em></em> <a class="tabLink" href="/html/acsl.html">ACSL</a>
        </div>
      </div>