Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Frama-C is a suite of tools dedicated to the analysis of software written in C

frama-c.com

Post reply on HN
Print view View original

1–10 of 18 posts

Re: Frama-C is a suite of tools dedicated to the analysis of software written in C

#3

Post by emmelaich »

rhth54656 wrote: post #2

The only option for windows is manual compilation using a POSIX library. Any suggestions for a similar tool?

Here's a list.

http://en.wikipedia.org/wiki/List_of_tools_for_static_code_a...

but sorry no suggestions or recommendations.

Re: Frama-C is a suite of tools dedicated to the analysis of software written in C

#7

Post by TorKlingberg »

It would be good to hear other HN:ers experience with various static analysis tools for C.

I have had good experiences with Flexelint (PC-Lint). It does not attempt to deeply analyze control flow, more like compiler additional warnings. It flags a lot of common mistakes and can basically turn C into a more strictly typed language. I feel a lot more confident in C code if I know that it passes lint, since it warns if you try to mix unsigned and signed ints, cast away const, call functions with wrong types etc.

Like many static analyzers it takes some work to set it up, and tune which warnings you actually car about. It is definitely business-priced and feel a bit old (although command line tools age well.

The is a clear lack of good open source tools. I tried all i could find, but Splint was the only one that would flag switch-cases without break. It was last updated in 2010.

Re: Frama-C is a suite of tools dedicated to the analysis of software written in C

#8

Post by nullc »

I like Frama-C a lot in theory, though in practice I found it hard to use except on very small code segments.

When its unable to prove a range the feedback you get from the solvers is inscrutable enough that its very hard to figure out what additional data it would need to satisfy the analysis. (Sort of like parsing C++ compiler template related errors)

I'd hoped that language features like the typestate stuff that used to be in Rust would someday make the work required to use sound analysis tools in production code smaller. I'm not sure if much thought has been given to what kinds of accommodations languages could give to ease static analysis while still being programmer friendly.

It seems that newer languages have actually moved away from analysis friendliness in some respects, however. E.g. in C a signed overflow is always a bug so if analysis can prove one is possible you have something to fix. Several modern languages have defined signed operations to wrap and so that obvious safety test is no longer available. (You could define in your own code that it should never wrap, effectively writing in a subset of the language, but as soon as you call into third party code you never know if an overflow was intended and safe or not— not without extensive analysis)

Re: Frama-C is a suite of tools dedicated to the analysis of software written in C

#9

Post by eliteraspberrie »

One feature you can start using right now: prove an assertion with the WP plugin. [1] It's especially useful to prove the absence of some undefined behaviour, bounds on variables, or invariance conditions.

[1] http://frama-c.com/wp.html

Re: Frama-C is a suite of tools dedicated to the analysis of software written in C

#10

Post by pcwalton »

nullc wrote: post #8

I like Frama-C a lot in theory, though in practice I found it hard to use except on very small code segments. When its unable to prove a range the feedback you get from the solvers is inscrutable enough that its very hard to figure out what additional data it would need to satisfy the analysis. (Sort of like parsing C++ compiler template related errors) I'd hoped that language features like the typestate stuff that u…

> I'd hoped that language features like the typestate stuff that used to be in Rust would someday make the work required to use sound analysis tools in production code smaller. I'm not sure if much thought has been given to what kinds of accommodations languages could give to ease static analysis while still being programmer friendly.

Well, since the Rust borrow check is basically a static analysis that's always on and is required to pass for the compiler to emit code, we've put a lot of thought into how to make it as programmer friendly as possible. The final trick that seemed to got it to fall into place was restricting data to only one mutable reference at all times—this was a restriction that's easy enough to understand and can be readily explained through error messages and tutorials. There's still a learning curve, of course, but I think we've got the system down to a reasonable level.

Post reply on HN