--- layout: fc_discuss_archives title: Message 127 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Information hiding: how to handle module's private static variables in Frama-C?



27/11/2013 14:20, David MENTRE wrote:
> Hello,
>
> 2013/11/27 BAUDIN Patrick <Patrick.Baudin at cea.fr>:
>> The ACSL importer plug-in (used to import external ACSL file) takes care of
>> that situation.
>> Unfortunately, this plugin isn't free.
> Even if this plug-in is not available, how one would use this plug-in
> to solve this issue?
>
As you will see, it is easy to use: it automatically does the 
transformation.

ACSL specification are allowed in C files, but aren't mandatory.
Here, I removed all ACSL specifcation from your C files and just created 
this file:
 > cat q18.acsl
function g:
contract :
requires p <= 10;
ensures \result == p + 1;
assigns a;

function incr_a:
contract :
requires a <= 10;
ensures a == \old(a) + 1;
assigns a;

function f:
contract :
assigns a;

Then the following command gives :
 > frama-c q18_a.c q18_b.c -acsl-import q18.acsl -print
[kernel] preprocessing with "gcc -C -E -I. q18_a.c"
[kernel] preprocessing with "gcc -C -E -I. q18_b.c"
[acsl-importer] Success for q18.acsl
[acsl-importer] Done: 1 file.
/* Generated by Frama-C */
int f(int p);

static int a = 0;
/*@ requires a ? 10;
ensures a ? \old(a)+1;
assigns a; */
void incr_a(void)
{
a ++;
return;
}

/*@ requires p ? 10;
ensures \result ? \old(p)+1;
assigns a; */
int f(int p)
{
int __retres;
if (a <= 10) incr_a();
__retres = p + 1;
return __retres;
}

/*@ requires p ? 10;
ensures \result ? \old(p)+1;
assigns a; */
int g(int p)
{
int tmp;
tmp = f(p);
return tmp;
}