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] I wrote a blog post about my experiences with Frama-C so far

ons 2018-11-21 klockan 16:07 +0100 skrev Virgile Prevosto:
> Hello Tomas,
> 
> > Le mer. 21 nov. 2018 à 12:02, Tomas Härdin <tjoppen at acc.umu.se> a écrit :
> 
> > 
> > As I've written earlier on this list, I'm still a beginner. But I think
> > someone might still find my experiences so far useful, so I decided to
> > document them:
> > 
> > http://www.härdin.se/blog/2018/11/20/trying-out-frama-c/
> > > > <http://www.xn--hrdin-gra.se/blog/2018/11/20/trying-out-frama-c/>
> > 
> > 
> 
> Thanks for sharing your experience. It is always interesting for us to have
> feedback on how Frama-C gets used in order to understand where improvements
> would be the most useful(*)
> In particular, your point about separation of strings warrant some thinking
> about \separated hypotheses that can be safely made by the memory models of
> WP.

Yeah. It also seems WP doesn't understand restrict, and doesn't
understand that string literals can't change (even with -wp-init-const)

> Regarding termination of recursive functions, this is indeed not yet
> implemented by WP, but ACSL introduces a decreases clause, which is similar
> to a loop variant: any recursive call must be done on a strictly smaller
> 'decreases' term than its direct caller, and that term must stay positive.

That sounds mighty useful. Here's hoping that makes it into WP soonish
:)

> However, for single recursive
> functions, a simple syntactic transformation should be able to generate an
> ACSL assertion at each recursive call from the content of the decreases
> clause.

A depth argument could work maybe, and an assertion that depth <= N for
some N that depends on the size of the original input (ceil(log2(hi-
lo+1))). A good compiler would optimize it out if the function is
static, effectively turning it into ghost code.

> Finally, the point about verification time is just a matter of perspective:
> just wait until Frama-C get a proper C++ front-end, and I'm sure we will be
> able to have a smaller execution time than the (C++) compiler 😝. On a more
> serious note, as was highlighted by one of our partners, the comparison
> should rather be done with the time taken by running a test suite with an
> extremely high level of coverage, a task which is not exactly free.

This is actually a topic I have planned for a future post. Comparing
the CPU time and developer time vs benefit of some common software QA
methods. Verification can replace unit testing outright, in my opinion.

You still need various forms of regression testing though, and fuzzing,
since many programs can be turned into busy beavers or behave in ways
that are hard to write contracts against.

/Tomas