Commits · 726be74cce3d35c496d89e082a82c9af6551af88 · pub / frama-c · GitLab

Snippets Groups Projects

Aug 28, 2020
- sample program results passes Sarif 2.1.0 validation · 726be74c
  Virgile Prevosto authored 4 years ago
  
  726be74c
Aug 27, 2020
- lint · ce371426
  Virgile Prevosto authored 4 years ago
  
  ce371426
- [sarif] continue upgrade to SARIF 2.1 · 9890f9d7
  Virgile Prevosto authored 4 years ago
  
  9890f9d7
- [sarif] on the road to sarif 2.1.0 migration · dd888597
  Virgile Prevosto authored 4 years ago
  
  dd888597
- [MdR] update to SARIF 2.1.0 · eeef90a4
  Andre Maroneze authored 4 years ago and Virgile Prevosto committed 4 years ago
  
  eeef90a4
- [MdR] do not emit location in SARIF if unknown · 446b2246
  Andre Maroneze authored 4 years ago and Virgile Prevosto committed 4 years ago
  
  446b2246
- [MdR] use report kind to set output extension · 490ec6c7
  Andre Maroneze authored 4 years ago and Virgile Prevosto committed 4 years ago
  
  490ec6c7
- [MdR] fix minor typos in SARIF output · 52d32d5c
  Andre Maroneze authored 4 years ago and Virgile Prevosto committed 4 years ago
  
  52d32d5c
- fix indentation · abe63e69
  Virgile Prevosto authored 4 years ago and Andre Maroneze committed 4 years ago
  
  abe63e69
- Let logical operators accept any scalar type as argument · f008db55
  Virgile Prevosto authored 4 years ago
  
  f008db55
- fix typo in comment · 1d52e20b
  Virgile Prevosto authored 4 years ago
  
  1d52e20b
Aug 26, 2020
- [Eva] remove generated option -eva-no-builtins-list · b45463ab
  Andre Maroneze authored 4 years ago
  
  b45463ab
- [e-acsl:changelog] move '.' (dot) at the end of sentences · 0ba1713a
  Julien Signoles authored 4 years ago
  
  0ba1713a
- [e-acsl:changelog] fixed duplicated entries · 8524d0b0
  Julien Signoles authored 4 years ago
  
  8524d0b0
- [eacsl] Update implementation manual · 9fe04063
  Basile Desloges authored 4 years ago
  
  9fe04063
Aug 25, 2020
- [WP] fix exception raised by invalid option in -wp-why3-opt · 4f02ced6
  Andre Maroneze authored 4 years ago
  
  4f02ced6
- [Server] fail more gracefully with invalid JSON files · ee8bf048
  Andre Maroneze authored 4 years ago
  
  ee8bf048
Aug 24, 2020
- [eacsl] Update changelog · 315ab85d
  Basile Desloges authored 4 years ago
  
  315ab85d
- [eacsl] Add tests for the support of logic arrays · 1e6b0636
  Basile Desloges authored 4 years ago
  
  1e6b0636
- [eacsl] Add support for logic arrays in `Translate.comparison_to_exp` · 3441230f
  Basile Desloges authored 4 years ago
  
  3441230f
- [eacsl] Add a module supporting the translation of logic arrays to expressions · 52b0e43a
  Basile Desloges authored 4 years ago
  
  52b0e43a
- [eacsl] Add a way to filter generated RTE annotations · d788d610
  Basile Desloges authored 4 years ago
  
  d788d610
- [eacsl] Create a function in Env to call an RTL function and store the result in a new variable · 5aa26731
  Basile Desloges authored 4 years ago
  
  5aa26731
- [eacsl] Update code with calls to Constructor module · 7496a86a
  Basile Desloges authored 4 years ago
  
  7496a86a
- [eacsl] Add constructor functions to manipulate expressions and statements · 9c5b45de
  Basile Desloges authored 4 years ago
  
  9c5b45de
- [eacsl] Add a function to check if a type is any of the GMP types · efe25831
  Basile Desloges authored 4 years ago
  
  efe25831
Aug 06, 2020
- [eacsl] Remove `reverse` parameter of `mk_runtime_check` · 7cf1420c
  Basile Desloges authored 4 years ago
  
  7cf1420c
- [eacsl] Update div by zero guard to not use `~reverse:true` · 57a28d88
  Basile Desloges authored 4 years ago
  
  57a28d88
- [eacsl] Update call sites of `mk_runtime_check` · b71b9727
  Basile Desloges authored 4 years ago
  
  b71b9727
- [eacsl] Fix `reverse` parameter of `mk_runtime_check` · 95b03c27
  Basile Desloges authored 4 years ago
  
  95b03c27
Jul 29, 2020
- [Dive] Server interface: if Eva has not been computed, emit an error. · f604eea3
  David Bühler authored 4 years ago
  
  Do not run Eva without warning when the Ivette component is open.
  f604eea3
Jul 28, 2020
- [eacsl] Update changelog · 624ce675
  Basile Desloges authored 4 years ago
  
  624ce675
- [eacsl] Add support of bitwise operations in E-ACSL implementation manual · 1d7a1e88
  Basile Desloges authored 4 years ago
  
  1d7a1e88
- [eacsl:tests] Update tests · b3d5eb0d
  Basile Desloges authored 4 years ago
  
  b3d5eb0d
- [eacsl:codegen] Add support for left and right shift with GMP parameters · b2af2148
  Basile Desloges authored 4 years ago
  
  b2af2148
- [eacsl:runtime] Enable functions of the GMP API to support shift operations · 1513b247
  Basile Desloges authored 4 years ago
  
  - Add `mp_bitcnt_t` type; - Add `__gmpz_mul_2exp()` (resp. `__gmpz_tdiv_2exp()`) to support left shift (resp. right shift); - Add `__gmpz_fits_ulong_p()` and `__gmpz_fits_slong_p()` to guard GMP to C integer coercions.
  1513b247
- [eacsl:codegen] Add support for bitwise AND, OR and XOR when using GMP parameters · bd647334
  Basile Desloges authored 4 years ago
  
  bd647334
- [eacsl:runtime] Register GMP bitwise and, or and xor API functions · 4afbcfd4
  Basile Desloges authored 4 years ago
  
  4afbcfd4
Jul 27, 2020
- [eacsl] Add a dependency to RTE · 2a770618
  Basile Desloges authored 4 years ago
  
  2a770618
- [Kernel] fix typo in rarely-seen message · 3fcbc990
  Andre Maroneze authored 4 years ago
  
  3fcbc990