GitLab

- "Alt-Ergo 0.93"
- "0.93.1"

I am assuming these numbers are not negative. This assumption has always
existed for integers and the lexer cannot create negative real numbers
anyway. So, as long as a transformation does not create negative numbers,
there won't be any issue. (Transformations applying a negation to positive
numbers are fine though.)

This is getting tedious. There should be a way to drop the content of a
whole theory.

. but need further cleaning

meta "instantiate : auto" on as many terms as possible.

The transformation is rather naive, since it doesn't look for term
candidates under quantifiers, if-then-else, let-in, and so on. So it can
only appear late in the transformation pipe.

It is only enabled for Gappa and its target axioms are the ones that state
that any floating-point value is bounded. It was the last transformation
from Why2 still missing in Why3.

Thanks to this transformation, Gappa is now able to prove all the safety
obligations from the following code, including the ones about division and
downcast, which is definitely frightening.

/*@ assigns \nothing;
  @ ensures \result == \abs(x);
  @*/
extern double fabs(double x);

/*@ requires \valid(AB_Ptr) && \valid(CD_Ptr);
  @ assigns *AB_Ptr, *CD_Ptr;
  @ ensures \abs(*AB_Ptr) <= 6.111111e-2;
  @ ensures \abs(*CD_Ptr) <= 6.111111e-2;
  @ */
void limitValue(float *AB_Ptr, float *CD_Ptr)
{
   double Fabs_AB, Fabs_CD;
   double max;

   Fabs_AB = fabs (*AB_Ptr);
   Fabs_CD = fabs (*CD_Ptr);

   max = Fabs_AB;
   if (Fabs_CD > Fabs_AB)  max = Fabs_CD;

   if ( max > 6.111111e-2)
   {
      *AB_Ptr = (float) (((*AB_Ptr) * 6.111111e-2) / max);
      *CD_Ptr = (float) (((*CD_Ptr) * 6.111111e-2) / max);
   }
}

In particular, they are now sufficient to prove that the difference of two
nonnegative floating-point numbers do not overflow.

Note that CVC3 doesn't care about syntax errors and it will still answer
valid at the end. Currently, CVC3 chokes on the following kind of
declarations (Div_mult, Abs_real_pos, and so on).

  ASSERT
  (FORALL (x : INT, y : INT, z : INT):PATTERN (div(((x * y) + z), x)):
  (((0 < x) AND ((0 <= y) AND (0 <= z))) => (div(((x * y) + z), x) = (y +
  div(z, x)))));

Modify the source buffer so that the filename is used for selecting syntax highlighting rather than always using why.

This ensures that C files (coming from Jessie) are not uniformly blue due to pointer deferencing "(*ptr)".
For unrecognized files (e.g. Jesse files), the IDE falls back to the old approach, that is, using Why highlighting.

diff in every case, even success
detailed mail subject