--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on November 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Floor problem



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;
}