Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Floor problem

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>