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

[Frama-c-discuss] New Frama-C version: Fluorine



On 24/04/2013 15:45, Cristiano Sousa wrote:
> Hi Lo?c,
>
> Here is an example: http://pastebin.com/jzq4Qg0r
>

The axiomatic was indeed inconsistent.


diff --git a/src/wp/share/memory.why b/src/wp/share/memory.why
index d75c81b..eaddcb2 100644
--- a/src/wp/share/memory.why
+++ b/src/wp/share/memory.why
@@ -41,7 +41,7 @@ theory Memory
      p.base = q.base -> (addr_le p q <-> p.offset <= q.offset)

    axiom addr_lt_def: forall p q :addr [addr_lt p q].
-    p.base = q.base -> (addr_le p q <-> p.offset < q.offset)
+    p.base = q.base -> (addr_lt p q <-> p.offset < q.offset)

    axiom addr_le_bool_def : forall p q : addr [ addr_le_bool p q].
      addr_le p q <-> addr_le_bool p q = True

Thanks for finding it! (thanks also z3!)

-- 
Fran?ois