Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Help, how to use Frama-C to scan linux kernel?

  • Subject: [Frama-c-discuss] Help, how to use Frama-C to scan linux kernel?
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Tue, 5 Apr 2011 09:38:04 +0200
  • In-reply-to: <4D9ABC38.8020408@cea.fr>
  • References: <CE761E84DADF2947A4AF22FB8D97A47356FC27E0@shsmsx501.ccr.corp.intel.com> <CE761E84DADF2947A4AF22FB8D97A47356FC27ED@shsmsx501.ccr.corp.intel.com> <AANLkTin71y2Saw=YiOriu4C=Rv4+wTBq_CbJNhF5RK4P@mail.gmail.com> <E1Q6rfm-0001OQ-Ng@garm.runbox.com> <4D9ABC38.8020408@cea.fr>
Hello Julien and David,

> Le 04/04/2011 23:50, David A. Wheeler a ?crit :
>> Sadly, I know of no package manager which knows how to sort atomic element
>> names. ?So we packagers of Frama-C on Fedora simply use "1." followed by the
>> atomic number (= number of protons). ?Thus, Beryllium becomes "1.4", and so
>> on. ?Then the package manager can figure out stuff like "is there a newer
>> version available in the repository" easily.

I did not know about that (or forgot about it). Thank you for the
explanation. You might have attached some string after the release
number like 1.4-beryllium so mere mortals could understand it. ;-)

2011/4/5 Julien Signoles <Julien.Signoles at cea.fr>:
> The Frama-C release number also contains a number attached to the atomic
> element names and usable for comparing versions. For instance, the exact
> version name of the last stable release is Carbon-20110201 while the exact
> version name of the previous stable release was Boron-20100401.
>
> As 20110201 >= 20100401, you can deduce that Frama-C Carbon is more recent
> than Frama-C Boron even if you don't know the Mendeleiev table.

<rant>
This might be good for packagers and package managers, but not for
mere mortals. Everybody understands the semantics of "major.minor".
Everything else is a pain.

/.*@ predicate Understandable_software_version_number{L}(integer
major, integer minor) =
            0 <= major && 0 <= minor
*/

</rant>

Best regards,
david