Stack Overflow
Stack Overflow

Questions tagged [alt-ergo]

Alt-Ergo is an open source automatic theorem prover dedicated to program verification.

Alt-Ergo is an open source automatic theorem prover dedicated to program verification. See http://alt-ergo.lri.fr/ for more information. It is an SMT solver based on CC(X): a congruence closure algorithm parameterized by an equational theory X. Alt-Ergo is based on a home-made SAT-solver and implements an instantiation mechanism for quantified formulas.

21 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
5
votes
2 answers

Proofs for code that relies on unsigned integer overflow?

How should I approach proving the correctness of code like the following, which, to avoid some inefficiency, relies on modular arithmetic? #include uint32_t my_add(uint32_t a, uint32_t b) { uint32_t r = a + b; if (r < a) …
Barrie Slaymaker
  • 65
  • 2
3
votes
1 answer

frama-c wp plugin fails to validate the swap function from the manual

How to make frama-c -wp verify the example from the wp manual - a trivial swap function (swap.c): /* @ requires \valid(a) && \valid(b); @ ensures A: *a == \old(*b); @ ensures B: *b == \old(*a); @ assigns *a,*b; @*/ void swap(int * a, int…
Necto
  • 2,594
  • 1
  • 20
  • 45
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
2 answers

Cannot prove euclidean division in frama-c

I'd like to prove this loop implementation of Euclidean division in Frama-C : /*@ requires a >= 0 && 0 < b; ensures \result == a / b; */ int euclid_div(const int a, const int b) { int q = 0; int r = a; /*@ loop invariant a == b*q+r &&…
V. Semeria
  • 3,128
  • 1
  • 10
  • 25
2
votes
1 answer

Is there a theory for uninterpretable functions (congruence analysis)?

I have a set of symbolic variables: int a, b, c, d, e; A set of unknown functions, constrained by a number of axioms: f1(a, b) = f2(c, b) f1(d, e) = f1(e, d) f3(b, c, e) = f1(b, e) c = f1(a, b) b = d Here functions f1, f2, f3 are unknown, but…
Necto
  • 2,594
  • 1
  • 20
  • 45
2
votes
2 answers

Calculate the range of an input which results in satisfying a predicate

Lets say we have the following C code: int my_main(int x){ if (x > 5){ x++; if (x > 8){ x++; if (x < 15){ //@(x >= 9 && x <= 14); } } } return 0; } I'd like…
Maor Veitsman
  • 1,544
  • 9
  • 21
2
votes
1 answer

SMT prover yields 'unknown' despite strong proven assertions

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

Why WP can't deduce "else" close?

I'm trying to write the specification for a function which takes 2 pointers to int and put the smaller value to the first pointer and the other to the second. Here is the code and the specification: /*@ requires \valid(a) && \valid(b); …
Dorian
  • 490
  • 2
  • 10
1
vote
1 answer

What should I do when this error occurs? Alt-Ergo: "Unknown error"

When I run the WP example, there is an error, and i don't know what it is. /*@ requires \valid(a) && \valid(b); @ ensures A: *a == \old(*b) ; @ ensures B: *b == \old(*a) ; @ assigns *a,*b ; @*/ void swap(int *a, int *b){ int tmp = *a; …
王少鹏
  • 11
  • 2
1
vote
1 answer

Any way to dump the alt-ergo proof obligations that frama-c creates?

I'm currently playing around with frama-c and I'm looking to see how frama-c encodes the various proof obligations for giving to a prover (or proof assistant). In this instance, alt-ergo. I was wondering if there's any specific way to "dump" the…
oldjohn1994
  • 359
  • 4
  • 12
1
vote
1 answer

frama-c wp const variable and const array

I'm trying to prove some C code with the WP plugin of Frama-C and have problem with example below: typedef unsigned char uint8_t; const uint8_t globalStringArray[] = "demo"; const int STRING_LEN = 5; /*@ requires \valid(src) && \valid(dest) && len…
bataliero1234
  • 145
  • 10
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
vote
1 answer

ensures proved even though code is defective?

In the following, how are the postconditions for behavior neg_limit being proven true when the relevant C code is commented-out? One of the Safety->check arithmetic overflow isn't provable, as expected, but it seems like neg_limit should also be…
Barrie Slaymaker
  • 65
  • 2
1
vote
1 answer

How to execute the following SMT-LIB code using Alt-Ergo

The following SMT-LIB code runs without problems in Z3, MathSat and CVC4 but it is not running in Alt-Ergo, please let me know what happens, many thanks: (set-logic QF_UF) (set-option :incremental true) (set-option :produce-models true) (declare-fun…
Juan Ospina
  • 1,317
  • 1
  • 7
  • 15
1
2