--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on August 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Plug-in Jessie



Test of the tutorial Jessie : 2.1)Memory safety on frama-c , Nitrogen, plug-in Jessie(I have not the GUI Jessie) :

#pragma JessieIntegerModel(math)
#pragma JessieTerminationPolicy(user)
int binary_search(long t[], int n, long v) {
int l = 0, u = n-1;
while (l <= u) {
int m = (l + u) / 2;
if (t[m] < v)
l = m + 1;
else if (t[m] > v)
u = m - 1;
else return m;
}
return -1;
}


After this test, the following information appear:

[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir /home/Perco/Users/dahan/frama-c-Nitrogen-20111001_sav/tests/Jessie_2.jessie
[jessie] File /home/Perco/Users/dahan/frama-c-Nitrogen-20111001_sav/tests/Jessie_2.jessie/Jessie_2.jc written.
[jessie] File /home/Perco/Users/dahan/frama-c-Nitrogen-20111001_sav/tests/Jessie_2.jessie/Jessie_2.cloc written.
[jessie] Calling Jessie tool in subdir /home/Perco/Users/dahan/frama-c-Nitrogen-20111001_sav/tests/Jessie_2.jessie
[jessie] user error: Jessie subprocess failed:   jessie  -why3ml  -v       -locs Jessie_2.cloc Jessie_2.jc

But we have not information about the memory safety, what can I do to have information about memory safety?

[@@THALES GROUP RESTRICTED@@]

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120824/9407ea77/attachment.html>