--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on November 2018 ---
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