how to use this repo

[chaomaer]

Hi, i am new to frama-c. I want to know how to use this repo.
I download this repo, and type make, then I don't know how to use it.
When i type make is_sorted.wp(in the is_sorted subdir), it gives me a error, could you please tell me
how to use this repo, I am confused with readme.txt. Thanks.

[jensgerlach]

Hello,

thank you for your interest. The readme might to be very precise...
On the other hand, could you please describe your error message?
When I run make is_sorted.wp the output looks like this.
How does it look on your side?

make is_sorted.wp
[kernel] Parsing is_sorted.c (with preprocessing)
[rte] annotating function is_sorted
[wp] 16 goals scheduled
[wp] Proved goals:   16 / 16
  Qed:                7  (0.32ms-2ms-11ms)
  Coq:                1 
  Alt-Ergo (why3):    8  (10ms-20ms-50ms) (interrupted: 1)
  Why3 (cvc3):        0  (interrupted: 1)
  CVC4:               0  (interrupted: 1)
  Why3 (eprover):     0  (interrupted: 1)
  Z3:                 0  (interrupted: 1)

[jensgerlach]

By the way, here is a very nice introductory document to Frama-C/WP.

https://allan-blanchard.fr/frama-c-wp-tutorial.html

[chaomaer]

Thanks for your quick reply and recommanded tutorial.
My error message is as follows:

$ make is_sorted.wp

[kernel] Parsing is_sorted.c (with preprocessing)
[wp] Running WP plugin...
[rte] annotating function is_sorted
[wp] 16 goals scheduled
[wp] [Coq] Goal typed_ref_external_lemma_SortedImpliesWeaklySorted : Default tactic
[wp] [Failed] Goal typed_ref_external_lemma_SortedImpliesWeaklySorted
        Z3: Unknown (54ms)
  Why3 (eprover): Unknown (54ms)
      CVC4: Unknown (54ms)
  Why3 (cvc3): Unknown (54ms)
  Alt-Ergo (why3): Unknown (53ms)
       Coq: Unknown
[wp] [Coq] Goal typed_ref_external_lemma_WeaklySortedImpliesSorted : Saved script
[wp] [Coq] Goal typed_ref_external_lemma_WeaklySortedImpliesSorted : Valid
[wp] [Coq] Goal typed_ref_external_is_sorted_ensures : Default tactic
[wp] [Failed] Goal typed_ref_external_is_sorted_ensures
        Z3: Unknown (Qed:45ms) (54ms)
  Why3 (eprover): Unknown (Qed:45ms) (54ms)
      CVC4: Unknown (Qed:45ms) (54ms)
  Why3 (cvc3): Unknown (Qed:45ms) (54ms)
  Alt-Ergo (why3): Unknown (Qed:45ms) (54ms)
       Coq: Unknown (Qed:45ms)
[wp] [Coq] Goal typed_ref_external_is_sorted_loop_invariant_sorted_preserved : Default tactic
[wp] [Failed] Goal typed_ref_external_is_sorted_loop_invariant_sorted_preserved
        Z3: Unknown (Qed:14ms) (54ms)
  Why3 (eprover): Unknown (Qed:14ms) (54ms)
      CVC4: Unknown (Qed:14ms) (54ms)
  Why3 (cvc3): Unknown (Qed:14ms) (54ms)
  Alt-Ergo (why3): Unknown (Qed:14ms) (54ms)
       Coq: Unknown (Qed:14ms)
[wp] [Coq] Goal typed_ref_external_is_sorted_loop_invariant_sorted_established : Default tactic
[wp] [Failed] Goal typed_ref_external_is_sorted_loop_invariant_sorted_established
        Z3: Unknown (Qed:3ms) (54ms)
  Why3 (eprover): Unknown (Qed:3ms) (54ms)
      CVC4: Unknown (Qed:3ms) (54ms)
  Why3 (cvc3): Unknown (Qed:3ms) (54ms)
  Alt-Ergo (why3): Unknown (Qed:3ms) (54ms)
       Coq: Unknown (Qed:3ms)
[wp] [Qed] Goal typed_ref_external_is_sorted_assert_rte_unsigned_overflow : Valid
[wp] [Coq] Goal typed_ref_external_is_sorted_assert_rte_mem_access : Default tactic
[wp] [Failed] Goal typed_ref_external_is_sorted_assert_rte_mem_access
        Z3: Unknown (Qed:4ms) (54ms)
  Why3 (eprover): Unknown (Qed:4ms) (54ms)
      CVC4: Unknown (Qed:4ms) (54ms)
  Why3 (cvc3): Unknown (Qed:4ms) (54ms)
  Alt-Ergo (why3): Unknown (Qed:4ms) (55ms)
       Coq: Unknown (Qed:4ms)
[wp] [Coq] Goal typed_ref_external_is_sorted_assert_rte_mem_access_2 : Default tactic
[wp] [Failed] Goal typed_ref_external_is_sorted_assert_rte_mem_access_2
        Z3: Unknown (Qed:2ms) (54ms)
  Why3 (eprover): Unknown (Qed:2ms) (54ms)
      CVC4: Unknown (Qed:2ms) (54ms)
  Why3 (cvc3): Unknown (Qed:2ms) (54ms)
  Alt-Ergo (why3): Unknown (Qed:2ms) (54ms)
       Coq: Unknown (Qed:2ms)
[wp] [Coq] Goal typed_ref_external_is_sorted_assert_rte_unsigned_overflow_2 : Default tactic
[wp] [Failed] Goal typed_ref_external_is_sorted_assert_rte_unsigned_overflow_2
        Z3: Unknown (Qed:2ms) (54ms)
  Why3 (eprover): Unknown (Qed:2ms) (54ms)
      CVC4: Unknown (Qed:2ms) (54ms)
  Why3 (cvc3): Unknown (Qed:2ms) (54ms)
  Alt-Ergo (why3): Unknown (Qed:2ms) (54ms)
       Coq: Unknown (Qed:2ms)
[wp] [Qed] Goal typed_ref_external_is_sorted_assert_rte_unsigned_overflow_3 : Valid
[wp] [Qed] Goal typed_ref_external_is_sorted_loop_assigns : Valid
[wp] [Qed] Goal typed_ref_external_is_sorted_assigns_part1 : Valid
[wp] [Qed] Goal typed_ref_external_is_sorted_assigns_part2 : Valid
[wp] [Qed] Goal typed_ref_external_is_sorted_assigns_part3 : Valid
[wp] [Qed] Goal typed_ref_external_is_sorted_loop_variant_decrease : Valid
[wp] [Coq] Goal typed_ref_external_is_sorted_loop_variant_positive : Saved script
[wp] [Coq] Goal typed_ref_external_is_sorted_loop_variant_positive : Valid
[wp] Proved goals:    9 / 16
  Qed:                7  (0.87ms-1ms-3ms)
  Coq:                2  (unknown: 7)
  Alt-Ergo (why3):    0  (unknown: 9)
  Why3 (cvc3):        0  (unknown: 9)
  CVC4:               0  (unknown: 9)
  Why3 (eprover):     0  (unknown: 9)
  Z3:                 0  (unknown: 9)

[jensgerlach]

Did you after the installation of Frama-C run the command why3 config --detect ?
This will register the installed provers with Why3. Frama-C accesses most provers through the Why3 software,

[chaomaer]

I indeed forget to run the why3 config --detect command. Thank you, It works.

[jensgerlach]

I am glad I could help.