--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on December 2018 ---
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