--- layout: fc_discuss_archives title: Message 34 from Frama-C-discuss on November 2014 ---
Hi, There are several issues you face with. 1. Defining the \floor builtin (undefined by default in Neon) 2. Axiomatizing a \floor function such that Alt-Ergo can reason about it The tow points are discussed in turn below. Point 1. is easily handled by using wp drivers (Cf. User Manual, option -wp-driver) Using driver, you can state that a logic predicate is equal to another function already defined in other place. And you can also ask WP to use supplementary Alt-Ergo, Coq and Why-3 files. You should have a look to file `<frama-c-share>/wp/wp.driver` for syntax example. It is interesting to notice that WP translates a double d into an int with `to_uint32(truncate (d))`. So in your case, you should use a driver directive like: ``` logic real \floor(real) = "truncate" ; ``` However, I?m afraid `truncate` is not yet axiomatized completely, but you can provide supplementary axioms about the `truncate` function on your own. Point 2. is not easy. Basically, all your axioms can not be instantiated by Alt-Ergo, or are infinitely instantiated and Alt-Ergo is overwhelmed. In your case, just remark that floor(x) = floor(x-1)+1 can be instantiated infinitely many times? You should document yourself about `triggers`. When you can not rely on triggers, you can finely control instantiation by using so-called `lemma functions`: // This is a `standard` lemma: //@ lemma FloorSmall : \forall real e ; 0.0 <= e < 1.0 ==> \floor(e) == e ; // This is a `lemma function`: //@ predicate FloorInt(integer k, real e) = \floor(k+e) = k + \floor(e); //@ lemma FloorInt_correct : \forall integer k,real e; FloorInt(k,e); These two lines are equivalent to asserting \forall k,e; \floor(k+e) = k+\floor(e) directly, But this formulation allows you to perform instantiations by hand wherever you need it: { ? //@ assert A: FloorInt( 10 , 0.5 ); //@ assert B: \floor(10.5) == 10.0 ; } (A) will be discharged by FloorInt_correct (A) will be inlined by Alt-Ergo as \floor( 10.0 + 0.5 ) = 10.0 + \floor(0.5) (B) will be finally discharged by FloorSmall Remark: you can turn these lemmas into axioms if you want to axiomatize \floor. Or you can prove them with Coq by using your axioms. Regards, L. Le 18 nov. 2014 ? 10:00, Sebastian <sdavrieux at gmail.com> a ?crit : > 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 > <testFloorAssiomatica.c>_______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20141118/740e831a/attachment-0001.html>