--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on April 2012 ---
Hello, i am currently trying to add ?native? support of multi-dimensional arrays to Jessie, using a local copy of the sourcecode. The reason is we have sources i would like to check but rewriting them to be Jessie- compatible is ?not an option?. So i tried to extend the retype_base_pointer visitor in norm.ml to do the job by using the ?each dimension into a sub-struct-technique?. So far i was able to verify the default behaviour of a few annotated functions with a contract like this: #define MAX_X 7 #define MAX_Y 5 typedef int AnArray2[MAX_X][MAX_Y]; /*@requires \valid(pTarget); @ensures \forall integer x, y; (x >= 0 && x < MAX_X) && (y >= 0 && y < MAX_Y) ==> (*pTarget)[x][y] == k; */ void Fill2(AnArray2 *pTarget, int k) { ... } Now i wonder where to go from here. My first idea were to run the test folder of the why-2.30 distribution, but i failed to figure out how to run the tests. To complicate things further, all development i do is Windows-based, so Unix/Linux tools are unavailable to me in general. However, any practical use of such a change requires it to be safe and reliable, and i still suspect my successfull verifications to originate from sheer luck. Maybe someone could drop me a tip how to proceed? I have a feeling other people might benefit from such feature as well. Thanks in advance Daniel F+S Fleckner und Simon Informationstechnik GmbH Am Kissel 1a 65549 Limburg Deutschland / Germany Phone Front Desk +49 (6431) 40 90 1 - 0, Fax - 30 http://www.FlecSim.de Sitz der Gesellschaft: D-65549 Limburg Registergericht: Limburg HRB 1731 Gesch?ftsf?hrer: Dipl.-Ing. Josef Horstk?tter, Dipl.-Ing. Andr? Zeh