meta tagshttps://git.frama-c.com/pub/meta/-/tags2024-02-15T17:14:49Zhttps://git.frama-c.com/pub/meta/-/tags/0.60.6Release 0.6<ul data-sourcepos="2:1-3:71" dir="auto">
<li data-sourcepos="2:1-2:40">compatibility with Frama-C 28.x Nickel</li>
<li data-sourcepos="3:1-3:71">
<code>-meta-check-callee-assigns</code> can now also be given declared functions</li>
</ul>2024-02-15T17:14:49ZVirgile Prevostohttps://git.frama-c.com/pub/meta/-/tags/0.5.10.5.1Virgile Prevostohttps://git.frama-c.com/pub/meta/-/tags/0.50.5<p data-sourcepos="1:1-1:147" dir="auto">Add option <code>-check-callee-assigns</code> to consider <code>assigns</code> and <code>from</code> of some functions for instantiating <code>writing</code> and <code>reading</code> HiLARes in callers.</p>2023-11-07T16:02:57ZVirgile Prevostohttps://git.frama-c.com/pub/meta/-/tags/feature-callee-assignsfeature-callee-assignsVirgile Prevostohttps://git.frama-c.com/pub/meta/-/tags/0.5-beta0.5-beta<p data-sourcepos="1:1-1:104" dir="auto">Add <code>\lhost_read</code> and <code>\lhost_written</code> meta-variables in <code>\reading</code> and <code>\writing</code> contexts respectively</p>2023-05-17T14:23:27ZVirgile Prevostohttps://git.frama-c.com/pub/meta/-/tags/0.40.4<p data-sourcepos="1:1-1:144" dir="auto">Like <a href="https://frama-c.com/fc-versions/iron.html" rel="nofollow noreferrer noopener" target="_blank">Frama-C 26.0 Iron</a> itself, MetAcsl has switched to <a href="https://dune.build/" rel="nofollow noreferrer noopener" target="_blank">dune</a> as build system.</p>2022-12-09T10:00:25ZVirgile Prevostohttps://git.frama-c.com/pub/meta/-/tags/0.4-beta0.4-betaAllan Blanchardhttps://git.frama-c.com/pub/meta/-/tags/pre-dunepre-duneVirgile Prevostohttps://git.frama-c.com/pub/meta/-/tags/0.30.3<p data-sourcepos="1:1-1:65" dir="auto">This is purely a compatibility release for Frama-C 25.0 Manganese</p>
<p data-sourcepos="3:1-3:107" dir="auto">sources: <a href="/pub/meta/uploads/9d6ad7136916ce78965434dde5a62567/frama-c-metacsl-0.3.tar.gz" data-canonical-src="/uploads/9d6ad7136916ce78965434dde5a62567/frama-c-metacsl-0.3.tar.gz" data-link="true" class="gfm">frama-c-metacsl-0.3.tar.gz</a></p>2022-07-05T12:18:23ZVirgile Prevostohttps://git.frama-c.com/pub/meta/-/tags/2022-03-232022-03-23Virgile Prevostohttps://git.frama-c.com/pub/meta/-/tags/0.20.2<p data-sourcepos="1:1-1:174" dir="auto">MetAcsl now has a <a href="https://git.frama-c.com/pub/meta/-/blob/0.2/CHANGELOG.md">Changelog</a>. Beyond compatibility with Frama-C 24.0 Chromium and OCaml 4.13, main changes include:</p>
<ul data-sourcepos="3:1-6:0" dir="auto">
<li data-sourcepos="3:1-3:69">new meta-variable family <code>\called_arg(n)</code> in the <code>\calling</code> context</li>
<li data-sourcepos="4:1-4:43">new meta-variable <code>\func</code> in all contexts</li>
<li data-sourcepos="5:1-6:0">new warning category <code>unknown-func</code>, aborting by default, for names in target set that do not correspond to a function in the program.</li>
</ul>
<p data-sourcepos="7:1-7:120" dir="auto">Download the archive: <a href="/pub/meta/uploads/dc14a37270cad97e382eb246459839e0/frama-c-metacsl-0.2.tar.gz" data-canonical-src="/uploads/dc14a37270cad97e382eb246459839e0/frama-c-metacsl-0.2.tar.gz" data-link="true" class="gfm">frama-c-metacsl-0.2.tar.gz</a></p>2022-01-04T18:20:05ZVirgile Prevostohttps://git.frama-c.com/pub/meta/-/tags/24.0-beta24.0-betaVirgile Prevostohttps://git.frama-c.com/pub/meta/-/tags/0.1.20.1.2Allan Blanchardhttps://git.frama-c.com/pub/meta/-/tags/0.1.10.1.1Virgile Prevostohttps://git.frama-c.com/pub/meta/-/tags/0.10.1<p data-sourcepos="1:1-1:147" dir="auto">This is the first release of MetAcsl. It is meant to be compiled against <a href="https://www.frama-c.com/fc-versions/titanium.html" rel="nofollow noreferrer noopener" target="_blank">Frama-C 22.0 Titanium</a></p>
<h1 data-sourcepos="3:1-3:15" dir="auto">
<a id="user-content-pre-requisite" class="anchor" href="#pre-requisite" aria-hidden="true"></a>Pre-requisite</h1>
<ul data-sourcepos="5:1-8:0" dir="auto">
<li data-sourcepos="5:1-5:23">Frama-C 22.0 Titanium</li>
<li data-sourcepos="6:1-6:65">OCaml compiler (the same as the one used for compiling Frama-C)</li>
<li data-sourcepos="7:1-8:0">SWIProlog (if you want to use the deduction facilities of MetAcsl)</li>
</ul>
<h1 data-sourcepos="9:1-9:32" dir="auto">
<a id="user-content-short-compilation-instructions" class="anchor" href="#short-compilation-instructions" aria-hidden="true"></a>Short compilation instructions</h1>
<ul data-sourcepos="10:1-15:16" dir="auto">
<li data-sourcepos="10:1-10:109">Download <a href="/pub/meta/uploads/deea5fb23305cdfa62976bec2cbce45c/frama-c-metacsl-0.1.tar.gz" data-canonical-src="/uploads/deea5fb23305cdfa62976bec2cbce45c/frama-c-metacsl-0.1.tar.gz" data-link="true" class="gfm">frama-c-metacsl-0.1.tar.gz</a>
</li>
<li data-sourcepos="11:1-11:39"><code>tar xzvf frama-c-metacsl-0.1.tar.gz</code></li>
<li data-sourcepos="12:1-12:22"><code>cd frama-c-metacsl</code></li>
<li data-sourcepos="13:1-13:15"><code>./configure</code></li>
<li data-sourcepos="14:1-14:8"><code>make</code></li>
<li data-sourcepos="15:1-15:16"><code>make install</code></li>
</ul>2020-11-27T14:53:53ZVirgile Prevostohttps://git.frama-c.com/pub/meta/-/tags/compat-fc-22.0-beta-1compat-fc-22.0-beta-1Introducing new option `-meta-separate-annots`Virgile Prevostohttps://git.frama-c.com/pub/meta/-/tags/compat-fc-22.0-betacompat-fc-22.0-betaThis tag is meant to be compiled against Frama-C [22.0-beta](https://git.frama-c.com/pub/frama-c/-/tags/22.0-beta)Virgile Prevostohttps://git.frama-c.com/pub/meta/-/tags/2020-10-162020-10-16Virgile Prevostohttps://git.frama-c.com/pub/meta/-/tags/2020-10-152020-10-15Virgile Prevosto