1. 11 Sep, 2011 2 commits
  2. 10 Sep, 2011 2 commits
  3. 07 Sep, 2011 1 commit
  4. 06 Sep, 2011 3 commits
  5. 02 Sep, 2011 5 commits
  6. 01 Sep, 2011 3 commits
  7. 31 Aug, 2011 1 commit
  8. 23 Aug, 2011 2 commits
    • Guillaume Melquiond's avatar
    • Guillaume Melquiond's avatar
      Add a new transformation that instantiates the axioms marked with the · 4d7dd217
      Guillaume Melquiond authored
      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);
         }
      }
      4d7dd217
  9. 22 Aug, 2011 1 commit
  10. 20 Aug, 2011 1 commit
    • Guillaume Melquiond's avatar
      Modify the source buffer so that the filename is used for selecting syntax... · d9caac0a
      Guillaume Melquiond authored
      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.
      d9caac0a
  11. 16 Aug, 2011 1 commit
  12. 11 Aug, 2011 7 commits
  13. 09 Aug, 2011 1 commit
  14. 05 Aug, 2011 4 commits
  15. 04 Aug, 2011 1 commit
  16. 28 Jul, 2011 1 commit
  17. 26 Jul, 2011 1 commit
    • Jean-Christophe Filliâtre's avatar
      Coq output: recursive definitions · 59b180cb
      Jean-Christophe Filliâtre authored
      introduced new transformation eliminate_non_struct_recursion for that purpose
      uses Decl.check_termination tomake the check and the pretty-print
      (could probably be improved to avoid 3 calls to check_termination)
      59b180cb
  18. 21 Jul, 2011 1 commit
  19. 13 Jul, 2011 2 commits