3 ms·
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. sou
by 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 agoI 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 agoNote that it's especially nasty in C, because it's either true or undefined behavior due to signed integer overflow.
- ritter2a 6y agoHaving 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 agoRight, that makes total sense yes. Thanks.
- Chris2048 6y agocould you add some modifier? "iff a =/= MAXINT"
- Jtsummers 6y agoIn 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 agoYou 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.
- mcguire 6y agoFrama-C has a wp plugin that generates assertions about overflow and underflow, which is one of the best tools it has. It's not spectacular about telling you where the problem is, and wasn't great with floats, though.
- aidenn0 6y agoComplicating it even more, if "a" is a signed-integer than the compiler will assume that statement holds and optimize accordingly, put your correctness prover would instead need to flag that (or add the caveat that a < INT_MAX)
- dvfjsdhgfv 6y agoIf I remember correctly, in ANSI C int is guaranteed to have the maximum value of only 65,535 when unsigned, so basically bounds checking is a must. Of course it's even more important for shorter types like char.