--- layout: fc_discuss_archives title: Message 50 from Frama-C-discuss on May 2013 ---
Hi everybody, I am currently using Jessie (with Nitrogen and Oxygen versions of Frama-C) to prove some stuff. I got a problem for proving an assign clause when calling a function with the address of a local variable. More precisely, I have a function comp that compares arrays of integers. It returns an error code thus the result has to be obtained through a poiter parameter: The prototype is (I removed some of the contract annotations that do not interfer). //@ assigns *res error_t comp ( const unsigned a[2], const unsigned b[2], char *res); Then I want to use this function in another one say f and want to prove that f does not modify any memory location excepted the one used to call comp. //@ assigns \nothing int f(const unsigned a[2], const unsigned b[2]) { unsigned res = 0; char tmp; comp( a, b, &tmp); // some code here return res; } I put assigns \nothing since tmp is not visible from postconditions but when launching Jessie and Why3, I obtain an error: "Unbound variable charP_tmp_8_alloc_table" This variable is not allocated in the stack since it is a local variable and I assume this is the reason why there is not such variable. Neverthelesss this variable actually appears in the VCs corresponding to the assigns postcondition. Am I doing something wrong or is it something that obviously will never be proved and that requires some trick to get rid of? Best, Beno?t GERARD [ENVOYE PAR INTERNET] -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130530/27d77c4a/attachment.html>