Commits · 6e2b195d816fb88af43c420f322d9563d4b2928b · pub / frama-c · GitLab

Snippets Groups Projects

May 13, 2024
- [libc] add spec for memrchr · 6e2b195d
  Andre Maroneze authored 1 year ago
  
  6e2b195d
- [libc] add specification for wcsdup · 3d940998
  Andre Maroneze authored 1 year ago
  
  3d940998
- [libc] improve spec of strrchr · 0b5b8594
  Andre Maroneze authored 1 year ago
  
  0b5b8594
May 06, 2024
- [kernel] Fixes typo in warning about integer compatibility. · 17f4d8c5
  David Bühler authored 10 months ago
  
  17f4d8c5
- [kernel] Ast-diff mark func with different code annot has having changed body · 0991027f
  Virgile Prevosto authored 11 months ago and David Bühler committed 10 months ago
  
  0991027f
- [kernel] infrastructure for custom comparison of ACSL extension in AST diff · 0eecc4a1
  Virgile Prevosto authored 11 months ago and David Bühler committed 10 months ago
  
  0eecc4a1
- [tests] more stable oracle for ast-diff test · 51b7c945
  Virgile Prevosto authored 11 months ago and David Bühler committed 10 months ago
  
  51b7c945
- [tests] add test for diffing ACSL extensions · 37e947b8
  Virgile Prevosto authored 11 months ago and David Bühler committed 10 months ago
  
  37e947b8
Apr 29, 2024
- [kernel] Warning key for arrays larger than SIZE_MAX. · 8fcf3467
  David Bühler authored 11 months ago
  
  8fcf3467
Apr 26, 2024
- [Eva] add a few more tests for memset builtin warnings · ed54762d
  Andre Maroneze authored 11 months ago
  
  ed54762d
- [Eva] Memory builtins: reduce arguments to valid locations. · 7e8b3697
  David Bühler authored 1 year ago and Andre Maroneze committed 11 months ago
  
  7e8b3697
- [Eva] Rewrites memcpy and memmove builtins. · e92da27f
  David Bühler authored 1 year ago and Andre Maroneze committed 11 months ago
  
  Avoids using exceptions, splits the implementation into several functions, adds some comments.
  e92da27f
- [Eva] Reports red statuses in post_analysis, and not in the main function. · b841e3db
  David Bühler authored 11 months ago and Andre Maroneze committed 11 months ago
  
  Thus, red statuses are only reported at the end of an analysis.
  b841e3db
- [Eva] Adds test of -eva-report-red-statuses parameter. · b943d024
  David Bühler authored 1 year ago and Andre Maroneze committed 11 months ago
  
  b943d024
Apr 24, 2024
- [tests] add a few more tests for nested implicit calls · 11d8d193
  Virgile Prevosto authored 11 months ago
  
  11d8d193
- [cabs2cil] Check type consistency between call varinfo and its arguments · e9522581
  Thibault Martin authored 11 months ago and Virgile Prevosto committed 11 months ago
  
  e9522581
- [cabs2cil] Check argument compatibility for calls without a prototype · 42293691
  Thibault Martin authored 11 months ago and Virgile Prevosto committed 11 months ago
  
  42293691
- [Cil] Better format indentation for ranges and term names · e3ddf133
  Thibault Martin authored 11 months ago
  
  e3ddf133
- [Cil] Print range names like in self#term · 8b44a329
  Thibault Martin authored 11 months ago
  
  8b44a329
- [tests] Add the example from issue 1373 as a test · f3557e7c
  Benjamin Jorge authored 11 months ago and Thibault Martin committed 11 months ago
  
  f3557e7c
- [Cil] Pretty print ranges · 38baa20b
  Benjamin Jorge authored 11 months ago and Thibault Martin committed 11 months ago
  
  38baa20b
Apr 19, 2024
- [test] Update oracles, cover sizeof in constFoldTerm · ba5357de
  Thibault Martin authored 11 months ago
  
  ba5357de
Apr 18, 2024
- [tests] add test case for builtin macro censorship · 385da6ac
  Virgile Prevosto authored 11 months ago
  
  385da6ac
- [tests] update tests · 8df1fe5f
  Virgile Prevosto authored 11 months ago
  
  8df1fe5f
- [Cil] fix handling of LNot in constfoldTerm · bbc462c7
  Andre Maroneze authored 11 months ago and Thibault Martin committed 11 months ago
  
  bbc462c7
- [tests] Add a test for constFoldTerm · 28ad9e61
  Thibault Martin authored 11 months ago
  
  28ad9e61
Apr 17, 2024
- [slicing] Removes useless loop pragma about Eva widening in tests. · f7d3deab
  David Bühler authored 11 months ago
  
  f7d3deab
- [Eva] Removes useless pragma in test. · 1502373a
  David Bühler authored 11 months ago
  
  1502373a
- [cabs2cil] Add label to dummyStmt to avoid crash when debuging · b02a6118
  Thibault Martin authored 11 months ago
  
  b02a6118
Apr 16, 2024
- [kernel] abort properly when a function is redefined (fixes #1360 ) · bd176b1a
  Virgile Prevosto authored 11 months ago
  
  bd176b1a
- [Eva] Uses the new kernel API to set the current location. · 94f1dd54
  David Bühler authored 11 months ago
  
  No need to reset the current location after the analysis of a function or after calling a visitor, as the new API ensures that this is the case.
  94f1dd54
Apr 15, 2024
- [tests] use double quotes when including Frama-C-specific libc header · 8590f367
  Andre Maroneze authored 11 months ago
  
  8590f367
Apr 05, 2024
- [Eva] Adds a test of the cvalue reduction by \base_addr. · a6b3c402
  David Bühler authored 11 months ago
  
  a6b3c402
Apr 04, 2024
- [Eva] Adds a test of successive runs using -eva-domains-function. · 2018460f
  David Bühler authored 11 months ago
  
  2018460f
- [tests] simpler test for builtin labels · 1fa9dbe4
  Allan Blanchard authored 11 months ago
  
  1fa9dbe4
- [kernel] simplify label name selection · c107d973
  Allan Blanchard authored 11 months ago
  
  - since we rename builtin labels, let us just try to find a label that does not need renaming
  c107d973
- [typing] rename C labels when name clashes with a builtin ACSL label · c0a3ed4f
  Virgile Prevosto authored 11 months ago
  
  c0a3ed4f
Apr 03, 2024
- [kernel] warn when using logic labels in code · 0d31e926
  Allan Blanchard authored 1 year ago and Virgile Prevosto committed 11 months ago
  
  - guarantee that pp code has the same semantics in such a case
  0d31e926
- [Eva] Rewraps absolute addresses of pointer values, seeen as unsigned integers. · 8bb63bdb
  David Bühler authored 1 year ago
  
  8bb63bdb
- [Eva] Adds test for negative absolute addresses. · 12274e4f
  David Bühler authored 1 year ago
  
  12274e4f