4 ms·

Warning! Lots of disjointed thoughts below. I've used Frama-C ACSL+WP and it was incredibly painful to use to prove basically anything. For me the main issue

• unwind 6y ago
  This: C's semantics also makes a lot of things which I would assume was "trivially true" fail verification. This isn't Frama-C's fault however, of course. sounds really interesting, do you remember some concrete example? Not saying you're wrong or anything, just curious of what kind of code is hard to analyze like this.
  • rwmj 6y ago
    I was wondering about this too. If I was going to guess I would say it could be stuff that applies to any language that uses fixed width machine types, and not only C. For example, this is not true: ∀a: a+1 > a if the type of 'a' is 32 bit int. Similarly negate(a) ≠ -a for some numbers.
    • steerablesafe 6y ago
      Note that it's especially nasty in C, because it's either true or undefined behavior due to signed integer overflow.
    • ritter2a 6y ago
      Having written test cases for a similar semantic program analysis tool, I agree: Integer overflow is a very likely cause for such "obviously correct but actually wrong" program invariants. The C semantics can make this problem even worse since signed integer overflow is undefined, leaving the user of such a framework to the mercy of the design decisions of the creators of the framework regarding undefined behavior.
    • unwind 6y ago
      Right, that makes total sense yes. Thanks.
    • Chris2048 6y ago
      could you add some modifier? "iff a =/= MAXINT"
    • Jtsummers 6y ago
      In SPARK/Ada you'd have to constrain the input for something like that or it wouldn't be able to discharge the proof. Suppose you wanted a simple function (which is too simple to write in reality, but for brevity): function Increment(A : Integer) return Integer with Post => Increment'Result = A + 1; It would find the counterexample for the situation where A is equal to Integer'Last. So you'd need to add a precondition like: function Increment(A : Integer) return Integer with Pre => A < Integer'Last, Post => Increment'Result = A + 1; (doing this from memory and not fluent, so syntax may be off but the idea isn't)
      • tom_mellior 6y ago
        You can do that in Frama-C as well. But now this new precondition must be propagated somewhere. For example, if you have some function (syntax from memory as well): /*@ ensures \result > a; */ int increment(int a) { return a + 1; } you would change it to: /*@ requires a < INT_MAX; ensures \result > a; */ int increment(int a) { return a + 1; } But if this function has N call sites, you now have N problems: At every call site you must prove that the precondition holds.
• doonesbury 6y ago
  >I had to provide my own loop invariants, which is also a pain You either make your spec up as you go along and don't check it as its hidden in the code, or provide it so that static analysis tools and/or things like tla+ can help confirm. There never was any getting around that regardless of language. The code follows from spec which both follow from requirements
  • creata 6y ago
    The loop invariants aren't part of the spec, they're part of the proof, and the computer's job is to automate as much of the proof as it can. That being said, automatically finding loop invariants is a hard and messy problem, so I can't really blame the Frama-C authors.
    • doonesbury 6y ago
      Wait - what are you arguing? That Frama or some other code can come up with loop invariants by itself from the code? Even if this is true and doable, it's bad. The question always was: does the code satisfy the spec, not whether we can derive a spec from the code and prove the spec is valid. In the other case - no - it's just what I wrote above.
      • creata 6y ago
        What? The loop invariants aren't part of the spec! The loop invariants are just an intermediate step in your proof that the preconditions are enough to guarantee that the postconditions will hold. If I was proving that 0 + 1 + .. n = n(n+1)/2, I wouldn't say that whatever induction step I chose to use was "part of the theorem", would I?
    • Jtsummers 6y ago
      The loop invariants that you can detect may not be the loop invariants that they want. Consider: for(int i = 0; i < n; i++) {..} It looks like the invariant should be: 0 <= i < n But if they mistyped the loop that would be wrong. You have to explicitly state your invariants. At best, you could detect them and ask for confirmation. And that's for an easy to detect case.
• creata 6y ago
  What kind of properties did you use Frama-C to verify?