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] Provide information to the value analysis

Hi Anne,

Your first mail went just fine, but the number of technical
discussions on the list is on the rise, and it is not always easy to
cope. Sorry for that, but complicated questions require complicated
answers, and in this case a fair amount of musings on my part.

On Thu, Apr 12, 2012 at 12:29 PM, Anne Pacalet <anne.pacalet at free.fr> wrote:
> int T[10];
>
> /*@ ensures \result == \null || \result == T+i; */
> extern int * fptr (int i);
[...]
> but I always get :
> p ? {‌{ &NULL ; &alloced_return_fptr + [0..2147483644],0%4 }‌}

First, for a function without a definition, if you want to use Value,
you _must_ write an 'assigns \from' clause. The \from clause is
important for correction, as Value uses it to compute what will go
into \result. Without 'assigns', as in this your example, you get a
dummy value that is supposed to represent the returned pointer. But,
as a rule of thumb : if something has value &alloced_return_foobar in
your analysis, the results won't be what you expect. This alloced_
mechanism is the best we have, but it is not even sound.

Second, why does your 'ensures' not work here? In Value, 'ensures' are
always evaluated after the 'assigns' clause, and can only be used to
reduce the post-assigns state. There are good reasons for this, chief
and foremost the fact that most derived analyzes use only the assigns
clauses. If Value did not start by using the assigns clause, the
results of those analyzes would be incoherent, and probably unsound.

Here,with the implicit 'assigns' generated, your ensures won't do what
you want. In the post-assigns state, &alloced_return_fprtr+[...] and
T+i are necessarily disjoint, and after reduction the second case
would be judged impossible. In Nitrogen, reduction seems not to be as
aggressive as possible. However, if you write
/* ensures \result == 0 || \result == T+i; */ // 0 instead of NULL
you obtain the behavior I'm speaking about: p is equal to NULL only.

A correct assigns from your function would be assigns \result \from i,
T. However, this does not parse, because we cannot currently refer to
addresses of globals in \from clauses. As an (ugly) workaround, you
can use a dummy pointer:
--------------------------
int T[10];

int *pt = T;

/*@ assigns \result \from i, pt;
    ensures \result == 0 || \result == T+i; */
extern int* fptr (int i);
-----------------------------------

This now does what you want. There is also no need to split after the
call to fptr, as the 'if' will do the disjunction implicitly.

Now, for the bad news. The way reduction on pointers proceeds has
changed in Oxygen, and this code will no longer work, nor actually any
other. There were good reasons for the change, so it is not clear what
will be in the final version of Oxygen.

Hope this clears things up,

-- 
Boris