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

[Frama-c-discuss] Average Problem



Hi,
Thank you very much for your previous reply.
I followed your instructions and I tried to implement the axiomatic Sum.
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 Sum 
doesn't work and I am not able to find the error.
I have made a "functionTest" function that calls "testSum" function with 
array elements that satisfy the requirements of "testSum" requires 
clause, but the prover was not able to prove it.
I attached the axiomatic Sum definition, the "testSum" function and the 
"functionTest" function.
Could you please suggest how I can proceed with finding a solution to 
this problem?

Thank you very much.
Best regards,
Sebastian



Il 29/09/14 14:12, Lo?c Correnson ha scritto:
> Hi,
> \sum and \lambda are unsupported with WP.
> Instead, you can axiomatize your sum or use an inductive predicate.
>
> See http://www.fokus.fraunhofer.de/de/sqc/_download_sqc/ACSL-by-Example.pdf
> ? 3.8.1 is a good hint.
> 	L.
>
>
>
> Le 29 sept. 2014 ? 10:00, Sebastian <sdavrieux at gmail.com> a ?crit :
>
>> Good morning,
>>     I'm trying to do the average without overflow, however I'm not able to check an assert that contains \sum annotation.
>> So I decided to make a simpler function that only uses \sum, but it doesn't work. What can I do to solve the problem?
>>
>> Best regards,
>> Sebastian
>> <testSum.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
> _______________________________________________
> 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 --------------
/*@
	axiomatic SumAxiomatic
	{
		logic integer Sum{L}(unsigned int* a, integer i, integer j) reads a[i], a[j-1];
		
		axiom Sum0:
				\forall unsigned int* a, int i, j;
				i > j ==> Sum(a, i, j) == 0;
		axiom Sum1:
				\forall  unsigned int* a, int i, j, k;
				0 <= i < j <= k ==> Sum(a, i, k) == Sum(a, i, j) + Sum(a, j, k);
		axiom Sum2:
				\forall unsigned int* a, int i, j;
				i == j ==> Sum(a, i, j) == a[i];
	 }
*/
/*@
  requires Sum(a, 0, length) == 10; 
*/
void testSum (unsigned int *a, unsigned int length){
}

/* Function used to test Sum */
void functionTest () {
	unsigned int a[] = {5U, 2U, 3U};
	testSum (a, 3U);
}