Skip to content
Snippets Groups Projects
  1. Jan 14, 2025
  2. May 13, 2024
  3. Mar 12, 2024
  4. Jul 31, 2023
  5. Jul 17, 2023
  6. May 09, 2023
  7. Jun 17, 2022
    • David Bühler's avatar
      [Inout] Records Inout results on all function calls for Eva. · b62c4e33
      David Bühler authored
      Eva relies on the inout plugin to ensure that a function call has not modified
      the values of its concrete arguments, meaning that at the end of the call, the
      values of formal parameters can be backward propagated to the corresponding
      concrete arguments. This is useful when the values of some parameters have been
      reduced by the call, for instance by some preconditions.
      
      To this end, Eva uses the Inout callback Record_Inout_Callbacks from Db, but
      this callback was only applied by Inout for functions whose body is analyzed.
      
      This commit modifies Inout to also record its result through this callback
      on functions interpreted by a builtin or a specification, thus allowing a
      precise backward propagation of the values of formal parameters to concrete
      arguments in all cases.
      b62c4e33
  8. Mar 21, 2022
    • Virgile Prevosto's avatar
      [kernel] Better casts introduction · b387e3bd
      Virgile Prevosto authored
      - always remove FC's internal attribute everywhere before deciding whether
        a cast is needed.
      - ACSL and C decisions to cast are similar
      - only unroll type for checking equality. If a cast is needed, keep
        typedef (if any) as target
      b387e3bd
  9. Feb 08, 2022
  10. Jan 14, 2022
  11. Jan 06, 2022
  12. Sep 03, 2020
  13. Jul 15, 2020
  14. May 25, 2020
  15. Mar 08, 2019
  16. Feb 05, 2019
  17. Jan 14, 2019
  18. Dec 12, 2018
  19. Dec 04, 2018
  20. Dec 03, 2018
  21. Nov 28, 2018
  22. Nov 23, 2018
  23. Nov 22, 2018
  24. Nov 16, 2018
  25. Oct 31, 2018
Loading