--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on August 2011 ---
Hello, Thank you for your answer of my question about "separated memory model". But I still have some problems about how to use it. I write a program "copy2.c" to test "separated memory model". The function "void copy(const value_type* a, size_type n, value_type* b)" could be proved, only if "separated memory model" is used. I start the program "copy2.c" with the following command: "frama-c-gui -wp -wp-proof alt-ergo copy2.c". The version of Frama-c is "Frama-C Carbon-20110201+dev". The following commands: "#pragma SeparationPolicy(regions)" and "requires \separated(a+(0..n-1), b+(0..n-1));" are used to ensure, that array a and array b are separated. The result is, that Line 39, "//@ assert i==0 ==> b[0] == a[0];" can be proved, while Line 40, "//@ assert i==1 ==> b[0] == a[0];" cannot be proved. The most likely problem of this result is, that array a and array b are not separated. I want to know, whether my usage of "separated memory model" is right or not? If not, could you give me an example, to illustrate, how to use it? Thank you Liangliang Gu -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110804/77301fac/attachment.htm> -------------- next part -------------- A non-text attachment was scrubbed... Name: copy2.c Type: text/x-csrc Size: 869 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110804/77301fac/attachment.c>