--- layout: fc_discuss_archives title: Message 45 from Frama-C-discuss on April 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [PROVENANCE INTERNET] Re: New Frama-C version: Fluorine



Small detail about your Length axiomatic :

axiomatic Length
  {
    logic integer Length{L}(char *s) reads *s;

    axiom string_length{L}:
       \forall integer n, char *s ; Length_of_str_is(s, n) <==> Length(s) == n ;
  }

This is over-specified. I choose only (==>) in my solution.
Actually, I'm afraid there is an inconsistency with (<==>).
Your axioms proves that for all pointer s, Length_of_str_is(s,Length(s)).
This means that all strings have a length. Which is false, indeed.

	L.