---
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
- Subject: [Frama-c-discuss] [PROVENANCE INTERNET] Re: New Frama-C version: Fluorine
- From: loic.correnson at cea.fr (Loïc Correnson)
- Date: Fri, 19 Apr 2013 15:45:19 +0200
- In-reply-to: <26107_1366378932_r3JDgBS3008854_6CD1ABCC-F4B9-4F61-8DBB-244A2948D3DB@cea.fr>
- References: <CAEt_dEohQ_aL9UhxzmAN=1reSMwWewwuXFERnAaPFh2ft7tu0w@mail.gmail.com> <26107_1366378932_r3JDgBS3008854_6CD1ABCC-F4B9-4F61-8DBB-244A2948D3DB@cea.fr>
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.