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] Tutorial ACSL By Example + WP plugin.

Hi everybody,

Yes, WP and Jessie have not exactly the same capabilities.
We are currently writing a tutorial on WP using exactly the algorithms  
of "ACSL By Example", with work-arounds and hints when necessary.
Previous work ? Fraunhoffer FIRST already reveal precious hints for  
improving WP there and there.
As a first hint list of 'hints' to validate "ACSL By Example" with WP:
  - fullfill all missing "assigns" clauses, eg. by including local  
variables modified during loop steps (1)
  - use option -wp-rte to generate proof obligations against runtime  
errors (default in Jessie, not in WP)
  - increase Alt-Ergo's timeout in presence of user-defined  
precidates, or use Z3 (2)
  - using -wp-split sometimes help

You should then manage to validate most of algorithms from "ACSL By  
Example" with these hints.
Regards,
	Loic Correnson.

(1) Actually, assigns clause must completely refer *all* assigned  
location, not only those allocated on the heap.
The memory model of Jessie is sometimes able to reason with incomplete  
assigns clause that do not mention local variables, provided their  
address is not taken (probably).
This a convenient extension, but not correct in ACSL sense. In Frama-C  
we are developping a plug-in to infer those missing assigns clause,  
but it is not distributed yet.

(2) This problem is due to non-optimal triggers for Alt-Ergo. It is  
already corrected for next release.