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] Frama-C: GUI's response time

  • Subject: [Frama-c-discuss] Frama-C: GUI's response time
  • From: Dillon.Pariente at dassault-aviation.com (Pariente Dillon)
  • Date: Tue, 21 Apr 2009 15:44:45 -0000
  • In-reply-to: <5030C1BB-9A4C-458A-B0CB-DA49C3EABB13@cea.fr>
Hello,
 
I owe you an answer about GUI's performances.
 
Frama-C is applied to the same code as described in my previous message below (100 fns, 10K Sloc).
And the computed state is saved (-save my_state.sav).
Frama-c processing elapsed time is about 7 minutes (Value Analysis computations are "minimal").
 
When launching frama-c-gui -load my_state.sav, elapsed time is about 30 minutes, before Frama-C-GUI window is displayed.
-debug 100 didn't give a lot of hints.
Lablgtk 2.12.0 is used when building frama-c-gui, and ./configure has option --enable-custommodel as you recommended.
 
Do you have some hints to instrument frama-c-gui in such a way to identify which of the frama-c-gui "sub-processes" is the most time-consuming?
 
Best regards,
Dillon
 



________________________________

	De : frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] De la part de Pascal Cuoq
	Envoy? : jeudi 2 avril 2009 16:02
	? : Frama-C public discussion
	Objet : Re: [Frama-c-discuss] Frama-C: GUI's response time
	
	
	
	

		I'm currently working on a larger source code of about 100 functions, for a total of 10K Sloc.
		Value Analysis is performed on the whole code through a classical command line like:
		frama-c-gui -val ... 
		 
		After some computations (~40 minutes elapsed time), Frama-C's GUI is displayed.

	
	
	The 40 minutes and the ~500Mb of memory are the resources used
	by the value analysis itself. You can avoid the wait the next time
	you need the results of the value analysis by using
	the -save / -load options, typically :
	frama-c -val *.c -save state
	frama-c-gui -load state

 

	Hi,
	If you are using the latest lablgtk release, you may configure Frama-C with the --enable-custommodel option.
	./configure --enable-custommodel
	make
	make install
	Please report your performance improvements with this configuration.
	Cheers,
	-- 
	| Benjamin Monate | mailto:benjamin.monate at cea.fr <mailto:benjamin.monate at cea.fr>  
	| Head of Software Safety Lab. CEA-LIST/DRT/DTSI/SOL/LSL |

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090421/d4b21e2a/attachment-0001.htm