--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on December 2018 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] why3 1.1.0 support in frama-c/wp



Hello Benjamin,

Niche to see that you look into the problem of various versions of Frama-C/WP and Why3!
You could try to test your work with our “ACSL by Example” suite from

	https://github.com/fraunhoferfokus/acsl-by-example

The appendix in ACSL-by-Example.pdf describes which provers we are using.
Once you have them installed, and set the variable 

	export FRAMAC_SHARE=`frama-c -print-share-path`

in your shell, you can go to the directory StandardAlgorithms and run

	$ make report-clean
	$ make report

The output of the latter command looks like

$ time make report
report nonmutating
   find                           [19    19   ( 10   9   0   0   0   0   0)]     100%
   find2                          [19    19   ( 10   9   0   0   0   0   0)]     100%
   find_first_of                  [25    25   ( 16   9   0   0   0   0   0)]     100%
   adjacent_find                  [22    22   ( 10  12   0   0   0   0   0)]     100%
   mismatch                       [20    20   ( 10  10   0   0   0   0   0)]     100%
   equal                          [7      7   (  6   1   0   0   0   0   0)]     100%
   search                         [30    30   ( 18  12   0   0   0   0   0)]     100%
  …

Overall verification time of the 72 examples should be around 45 minutes.

Regards

Jens