--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on August 2012 ---
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>