--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on November 2014 ---
Hi, I tried to use \floor but it raised an error: "The full backtrace is: Raised at file "hashtbl.ml", line 353, characters 18-27 Called from file "hashtbl.ml", line 361, characters 22-38 Plug-in wp aborted: internal error. Reverting to previous state. Look at the console for additional information (if any). Please report as 'crash' at http://bts.frama-c.com/. Your Frama-C version is Neon-20140301. Note that a version and a backtrace alone often do not contain enough information to understand the bug. Guidelines for reporting bugs are at: http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines" So I tried to implement an axiomatic floor function. I am using "Frama-C Neon-20140301" with Alt-Ergo prover on Ubuntu 14.04. I have tried to test it with a simple example but my axiomatic floor doesn't work and I am not able to find the error. I have made a "testFloor" function with assert clauses, but the prover was not able to prove it. I attached the axiomatic Floor definition and the "testFloor" function. Could anyone please suggest how I can proceed with finding a solution to this problem? Thank you very much, Sebastian -------------- next part -------------- /*@ axiomatic Floor { @ logic integer floor{L}(real a) @ reads a; @ axiom floor1{L}: @ \forall real a; (a < -1 ==> floor(a) == floor(a+1) - 1); @ axiom floor2{L}: @ \forall real a; (-1 <= a < 0 ==> floor(a) == -1); @ axiom floor3{L}: @ \forall real a; (0 <= a < 1 ==> floor(a) == 0); @ axiom floor4{L}: @ \forall real a; (a >= 1 ==> floor(a) == floor(a-1) + 1); @ } @*/ void testFloor (){ //@ assert floor(0.1) == 0; //@ assert floor(10.5) == 10; //@ assert floor(-0.1) == -1; //@ assert floor(-10.5) == -11; }