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] Question about Impact analysis results

Hello,

2017-01-27 11:51 GMT+01:00 Divya Muthukumaran <divya84 at gmail.com>:
> Hi All,
>
> I was playing around with the impact analysis with the following example:
> I have two variables conf_data and nonconf_data and I am tagging the
> assignment to the former. I was expecting to see the call to and definition
> of
>  harmlessFunction() in the results but I get the following, which contains
> the
> assignment to nonconf_data and its use. Could someone explain to me why they
> get included? The command I am running is commented out at the beginning of
> the
> code.

I'd say that this is a side-effect of the way Frama_C_interval is
specified in __fc_builtin.h: it relies on an extern volatile global
Frama_C_entropy_source to introduce some non-determinism, and its
specification indicates that it makes both read and write accesses to
this variable. Hence the calls to Frama_C_interval in the first loop
potentially have an impact to the calls to Frama_C_interval in the
second loop. You can avoid that by specifying another interval
function relying on another entropy source that is only read, e.g.

volatile int entropy_source;

/*@ assigns \result \from entropy_source;
    ensures min <= \result <= max;
*/
int my_interval(int min, int max);

(note that technically, it could be argued that the number of read
accesses could have an impact on the value read from entropy_source,
so that impact should still consider that the second loop is impacted
by the first, but the actual implementation does not do that).

Finally, the call to harmlessFunction is not impacted by a statement
writing to the content of conf_data because harmlessFunction never
dereference its pointer argument: only the first call to malloc has an
impact here. The call to harmfullFunction is impacted by writing to
the content of nonconf_data because of the val = *array_D instruction
in verboseLog. By transitive closure, in the case where assignment to
noncond_data[i] is considered as impacted by assignment to
conf_data[i], this latter assignment impacts the call to
harmfullFunction.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile