Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] How to support multi-dimensional arrays in Jessie?

  • Subject: [Frama-c-discuss] How to support multi-dimensional arrays in Jessie?
  • From: ds.verification at flecsim.com (ds.verification at flecsim.com)
  • Date: Thu, 5 Apr 2012 12:12:41 +0200 (CEST)
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