[SystemSafety] C for OSs

[David Crocker]

C does have a first-class Boolean type since the 1999 version. Sadly,
it's type-convertible to integer; but any MISRA-C checker will take care
of that.

David Crocker, Escher Technologies Ltd.
http://www.eschertech.com
Tel. +44 (0)20 8144 3265 or +44 (0)7977 211486

On 09/09/2019 11:13, Olwen Morgan wrote:
>
>
> I agree with your point about different compilers. It's a hefty
> challenge for any C tool developer to come up with retrofitted formal
> semantics that fit many compilers.
>
> As regards the lack of features in C, again I agree. AFAI recall QAC
> can produce diagnostics that make up for the lack of named type
> equivalence. Functions can make up to a significant extent for the
> lack of first-class Boolean and array types. One can program around
> the lack of user-defined scalar types. But of course, C simply does
> not have packages.
>
> But for all the possibility of workarounds, they remain just that. It
> takes effort to give yourself anything approaching the convenience of
> Ada's superior language design.
>
> Your comment about an acceptable false-positive rate is illuminating.
> Very early in my use of QAC, I simply decided to live with a high
> false-positive rate as the price of getting good diagnostics. Only
> gradually did I reduce the false positives by adopting the
> paranoid-critical C programming style that I use today - and here the
> surrealist overtones are not entirely frivolous.
>
> For the avoidance of doubt, _IMO yo__u _*_c_**_annot _**_equal_*_SPARK
> Ada code quality in C_. I've only ever said that you can approach it
> (albeit, I'm confident, fairly closely) by using different
> best-of-breed tools and exercising a severe coding discipline that
> takes a long time - and perhaps a peculiar mindset - to acquire.
>
> And all that hassle really shouldn't be necessary in the first place.
>
> Olwen
>
>
> On 09/09/2019 10:29, Roderick Chapman wrote:
>>
>> On 08/09/2019 18:23, Olwen Morgan wrote:
>>> Rod Chapman and I have a long-standing (and exceedingly civilised
>>> :-) difference of opinion in this area. If you have the right tools,
>>> and if you are prepared to observe draconian coding discipline, then
>>> I believe that you can in C approach a SPARK Ada level of code
>>> quality. Rod, if I am not traducing him, has lingering doubts about
>>> this. IMO tools are no longer the problem since those who write them
>>> simply retrofit sensible formal semantics to (annotation-extended
>>> subsets of) C and then perform verifications accordingly.
>>
>> I still have reservations. The big challenge is to come up with a
>> formal semantics that is implemented by both your favourite
>> verification tool and all versions of all compilers that you might
>> have to use during the lifetime of a project. If you can "lock in" to
>> exactly ONE compiler, then things are significantly simpler... but
>> this is not a good place to be when, in twenty years time, you really
>> do have to change compiler for a hardware update or some other
>> reason, but the vendor has long since gone out of business. I see far
>> too many projects stuck in this particular rut.
>>
>> In SPARK, it works by the complete removal of undefined behaviours
>> and any dependence on unspecified behaviour. This requires subsetting
>> and forms of analysis, which you need to be demonstrably sound and
>> efficient enough to scale up to large programs.
>>
>> I am currently engaged in writing some highly critical C code, using
>> the latest Frama-C toolset. I find the experience rather
>> frustrating... the problem seems to be two-fold:
>>
>> 1. C is lacking some fundamental features that make SPARK work. (The
>> short version: user-defined scalar types, named type equivalence, a
>> first-class Boolean type, packages, formal parameter modes, and
>> first-class array types).
>>
>> 2. Some very basic things in C are undefined. Worst-offender: signed
>> integer overflow.
>>
>> The upshot is that I find it's very hard to get to an acceptable
>> false-positive rate from the Frama-C WP tool. On a recent SPARK
>> project, the "acceptable" false alarm rate for type-safety proof was
>> ZERO.. so perhaps my expectations are set too high?
>>
>> Example: in SPARK, we use user-defined scalar types all over the
>> place to describe invariants from the problem domain which apply to
>> every parameter, constant and variable of each type. That info is
>> used by the VC generator to constrain the values of variables, so
>> that proving non-overflow becomes tractable. I don't know how to do
>> that in C... (if anyone does know how, please help me out...)
>>
>>  - Rod
>>
>>
>>
>>
>> _______________________________________________
>> The System Safety Mailing List
>> systemsafety at TechFak.Uni-Bielefeld.DE
>> Manage your subscription:
>> https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
>
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription: https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20190909/e19c0d1f/attachment-0001.html>