1. 22 Jul, 2022 1 commit
    • MARCHE Claude's avatar
      New attribute `[@vc:trusted_wf]` · 4ce10791
      MARCHE Claude authored
      It allows one to declare a relation well-founded without need to prove it
      
      As a side-effect, it does not require to import `relations.WellFounded`
      
      See issue #626
      4ce10791
  2. 08 Jul, 2022 1 commit
  3. 07 Jul, 2022 1 commit
  4. 02 Jun, 2022 3 commits
  5. 06 Apr, 2022 1 commit
  6. 29 Oct, 2021 1 commit
  7. 29 Sep, 2021 2 commits
  8. 23 Sep, 2021 1 commit
  9. 22 Sep, 2021 1 commit
  10. 21 Sep, 2021 1 commit
  11. 31 Aug, 2021 1 commit
  12. 23 Aug, 2021 1 commit
  13. 13 Jul, 2021 1 commit
  14. 27 Jun, 2021 3 commits
  15. 24 Jun, 2021 1 commit
    • paulpatault's avatar
      Micro Python : syntax improvements & added functions · 2cc29e89
      paulpatault authored
      - added break and continue
      - added range with one, two or three argument(s)
      - added slice (`list[i1:i2]`)
      - added negative index (`list[n], with -len(list) ≤ n < len(list)`)
      - added lists methods:
        - `list.append(n)`
        - `list.pop()`
        - `list.clear()`
        - `list.sort()`
        - `list.reverse()`
      - added `is_permutation(list1, list2)` predicate
      - added assignment operators `+=`, `-=`, `*=`, `//=`, `%=`
      - functions can now return `bool` and `list`
      2cc29e89
  16. 31 May, 2021 1 commit
  17. 12 Mar, 2021 1 commit
  18. 10 Mar, 2021 1 commit
  19. 10 Feb, 2021 2 commits
  20. 09 Feb, 2021 1 commit
    • MARCHE Claude's avatar
      Update bitvector modules for use in programs. · 694753fb
      MARCHE Claude authored
      Makes both signed and unsigned operations, which have
      slightly different pre-conditions.
      
      Further improvement needed: overflow checks are still
      using functions `to_int` or `to_uint`, which are not
      suitable for SMT solvers with bit-vector support.
      694753fb
  21. 08 Feb, 2021 1 commit
  22. 07 Feb, 2021 1 commit
  23. 06 Feb, 2021 1 commit
  24. 05 Feb, 2021 1 commit
  25. 29 Jan, 2021 1 commit
  26. 15 Jan, 2021 1 commit
    • Benedikt Becker's avatar
      Separate logical and program function Array.make · 1bb0c818
      Benedikt Becker authored
      When defined as a `val function` the postcondition of the program function
      `make` is just `result = make n v`, referring to the logical function `make`.
      But the equality cannot be proven because array equality is not defined.
      
      To facilitate proofs about results of the program functions `make`, this
      commit separates the definitions of the logical function from the program
      function `make`, so that the postconditions of the program function `make`
      refer to the properties of the resulting arrey.
      1bb0c818
  27. 13 Jan, 2021 1 commit
  28. 05 Dec, 2020 1 commit
  29. 08 Sep, 2020 1 commit
    • Yannick Moy's avatar
      T824-034 Add support for 128-bit bitvectors · f9c46976
      Yannick Moy authored and Benedikt Becker's avatar Benedikt Becker committed
      This entails creating the modules for conversions between these and smaller
      bitvectors, as well as to the larger (and newly created) 256-bit bitvector
      for verifying absence of overflows on operations over 128-bit bitvectors.
      
      Change-Id: I6089b63b7c37c6cc6b00ab13795e2edeb8b048df
      f9c46976
  30. 26 Aug, 2020 1 commit
  31. 25 Aug, 2020 1 commit
  32. 14 Jul, 2020 1 commit
  33. 02 Jul, 2020 1 commit
  34. 30 Jun, 2020 1 commit