Stack Overflow
Stack Overflow

Questions tagged [why3]

Why3 is a platform for deductive program verification. It provides rich language for specification and programming called WhyML. WhyML is also used as an intermediate language for the verification of C, Java or Ada programs

Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.). A user can write WhyML programs directly and get correct-by-construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs.

31 questions
6
votes
1 answer

User Error: Prover 'alt-ergo' not found in why3.conf

I am trying to test a function with Frama-c: /*@ ensures \result >= x && \result >= y; ensures \result == x || \result == y; */ int max( int x, int y){ return (x>y) ? x : y; } After I installed all the requirements: OPAM, why3,…
I. Ali
  • 171
  • 2
  • 5
3
votes
0 answers

Need help defining a machine integer

I'm using the mach.int library in a specification (see also this question), and I'm trying to define a constant that is of type int32: let constant_out1: int32 = 1 in … However, when analyzing this, why3 returns the message: This term has type int,…
Ben Hocking
  • 7,790
  • 5
  • 37
  • 52
3
votes
2 answers

How to use Why3 proofs in Frama-C GUI?

This feels like a silly question, but I'm stumped. I'm trying to use Frama-C Sodium and Why3 0.86.1 (both installed via OPAM) to prove some simple properties. Consider this program (toy.c): int main(void) { char *hello = "hello world!"; /*@…
Isabelle Newbie
  • 9,258
  • 1
  • 20
  • 32
3
votes
2 answers

alt-ergo does not run on windows via cygwin

I am trying to run a test file on frama-c with the alt-ergo prover. However,I am getting the followng error with alt-ergo. All the other frama-c checks are fine. I know that the issue is not with the test…
Quantico
  • 2,398
  • 7
  • 35
  • 59
2
votes
1 answer

How to prove why3 generated script in coq?

I use frama-C WP and want to debug my ACSL annotations (to understand why provers say me "don't know"). I have some green or orange results. I open why3 IDE and see the generated scripts. Then I select a theory/goal from the list and able to start…
SeregASM
  • 75
  • 12
2
votes
1 answer

What does [ <- ] mean in why3?

I'm using Frama-C, Alt-Ergo and Why3 for system verifications. One proof obligation generated in Frama-C and sent to Why3 is shown below (this is the Why3 version): (p_StableRemove t_1[a_5 <- x] a_1 x_1 a i_2) I'd like to know what t_1[a_5 <- x]…
Vitor
  • 367
  • 3
  • 12
2
votes
1 answer

The exact mechanism of mapping WhyML into SMT logic

Good day, auto deduction and verification hackers! In order to gain a deeper understanding of how exactly WhyML provides proofs for ACSL-annotated C programs I am trying to manually "reproduce" the job Why3 does with WhyML program while translating…
Evgeniy
  • 383
  • 2
  • 8
2
votes
1 answer

Why3 is unable to run prover on windows via cygwin

I am trying to use cvc4 prover with Frama-c wp plugin through Why3 on Windows environment. I have frama-c and why3 installed on my system. Why3 is configured properly to include cvc4 as a prover : $ why3 --list-provers Known provers: Alt-Ergo…
Gunjan Aggarwal
  • 710
  • 5
  • 19
2
votes
0 answers

OCaml bugs during why3 usage

I'm trying to compile why3ide (why3-0.81) with krakatoa & jessie (why-2.33) for Windows (Cygwin). Everything went fine except I can't make right bottom textbox to show notations (it is always empty), moreover I get the error (highlighted in the…
Vyacheslav Napadovsky
  • 887
  • 7
  • 15
1
vote
1 answer

Frama-C 23 and Coq

After installing Frama-C (23), Why3, and Coq on macOS I ran the command rm -f ~/.why3.conf ; why3 config detect The following message was shown Found prover Coq version 8.10.2, but no Why3 libraries were compiled for it Does this mean I cannot…
Night Heron
  • 11
  • 1
1
vote
1 answer

What is the proper way to type lambdas in Why3ML?

I want to verify a function with a lambda. For instance: let map (t : array int) (f : array int -> array int) : array int = f t However, this yields an error: File "map_reduce.mlw", line 25, characters 4-7: This application instantiates…
Derek Brown
  • 4,232
  • 4
  • 27
  • 44
1
vote
1 answer

array_eq_sub behavior for zero length

I have the following lemma in why3: lemma trivial: forall a : array 'a, b : array 'a. array_eq_sub a b 0 0 This seems like it would be the base case behavior, but apparently isn't. Any ideas on why this isn't working? UPDATE I was able to…
Derek Brown
  • 4,232
  • 4
  • 27
  • 44
1
vote
1 answer

Jessie plugin integration with Frama-c Aluminium

How to integrate Jessie an external plugin(why 2.36) with Frama-c Aluminium?
karan
  • 67
  • 4
1
vote
2 answers

Coq inductive reasoning about ACSL inductive predicates?

Is it possible to use induction on inductive predicates defined in ACSL? Consider the following example from the ACSL manual: struct List { int value; struct List* next; }; /*@ inductive reachable{L}(struct List* root, struct List* to) { @…
Necto
  • 2,594
  • 1
  • 20
  • 45
1
vote
1 answer

Proving simple property of a function over array

Suppose we have the following annotated C-code: int a[3] = {0}; /*@ requires \valid(a+(0..2)); assigns a[0..2]; ensures \forall int j; 0 <= j < 3 ==> (a[j] == j); */ int main() { int i = 0; /*@ loop assigns i, a[0..(i-1)]; …
Evgeniy
  • 383
  • 2
  • 8
1
2 3