Comments (6)
jensgerlach
commented on May 20, 2024
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)
from acsl-by-example.
jensgerlach
commented on May 20, 2024
By the way, here is a very nice introductory document to Frama-C/WP.
https://allan-blanchard.fr/frama-c-wp-tutorial.html
from acsl-by-example.
chaomaer
commented on May 20, 2024
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)
from acsl-by-example.
jensgerlach
commented on May 20, 2024
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,
from acsl-by-example.
chaomaer
commented on May 20, 2024
I indeed forget to run the why3 config --detect command. Thank you, It works.
from acsl-by-example.
jensgerlach
commented on May 20, 2024
I am glad I could help.
from acsl-by-example.
Related Issues (10)
- Minor mistake in section 3.5.2 HOT 7
- TravisCI: clean the cache HOT 1
- tautological inequality in the find algorithm ACSL HOT 2
- preparing potassium for travis HOT 1
- Test issue HOT 1
- Make error for `heap` HOT 3
- communication check
- V16.1.0 : Figure 5.5 appears to be incorrect HOT 2
- Different default values in makefile and readme HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from acsl-by-example.