Commits · 3fa7de0c695188a9b0adf7a8b8bfb24a335c1df7 · pub / frama-c · GitLab

Snippets Groups Projects

Feb 19, 2021
- Merge branch 'feature/kernel/axioms' into 'master' · 3fa7de0c
  Virgile Prevosto authored 4 years ago
  
  [kernel] merging admit lemmas & axioms See merge request frama-c/frama-c!3058
  3fa7de0c
Feb 18, 2021
- Merge branch 'bugfix/basile/999-rtl-spec-merge' into 'master' · 92c3ccb9
  Basile Desloges authored 4 years ago
  
  [eacsl] Merge contracts between RTL and stdlib Closes #999 See merge request frama-c/frama-c!3032
  92c3ccb9
- [eacsl] Update tests · 26595e9f
  Basile Desloges authored 4 years ago
  
  26595e9f
- [eacsl] Update contracts of allocation functions · b58f650a
  Basile Desloges authored 4 years ago
  
  The contracts are updated to mention the behaviors in the contracts of `stdlib.h` and satisfy Eva.
  b58f650a
- [eacsl] Merge the specifications from the RTL functions with the corresponding... · e76ace79
  Basile Desloges authored 4 years ago
  
  [eacsl] Merge the specifications from the RTL functions with the corresponding functions from the user's project
  e76ace79
- [kernel] Add function to add a spec to a function or statement · 518863e3
  Basile Desloges authored 4 years ago
  
  518863e3
- Merge branch 'feature/andre/audit-sources' into 'master' · 0531e525
  David Bühler authored 4 years ago
  
  add source audit options See merge request frama-c/frama-c!2947
  0531e525
- [Eva] Removes unused changes in value_parameters. · 58e7bc34
  David Bühler authored 4 years ago
  
  58e7bc34
- [Eva] Audit mode: changes the warning message on missing files. · ed9297ff
  David Bühler authored 4 years ago
  
  ed9297ff
- [Eva] Fixes a typo in the user manual. · 4e1473b5
  David Bühler authored 4 years ago
  
  4e1473b5
- [Eva] Updates header. · b7342390
  David Bühler authored 4 years ago
  
  b7342390
- [Kernel] minor audit fixes following review · ae3f2dab
  Andre Maroneze authored 4 years ago and David Bühler committed 4 years ago
  
  ae3f2dab
- [Kernel] audit mode: add check for missing hashes, with tests · d449dba5
  Andre Maroneze authored 4 years ago and David Bühler committed 4 years ago
  
  d449dba5
- [Kernel] audit mode failure triggers an error · bb1e66e8
  Andre Maroneze authored 4 years ago and David Bühler committed 4 years ago
  
  bb1e66e8
- [Eva/Doc] document audit-related options · bb2b6e51
  Andre Maroneze authored 4 years ago and David Bühler committed 4 years ago
  
  bb2b6e51
- [kernel] File: minor refactoring · be565648
  Andre Maroneze authored 4 years ago and David Bühler committed 4 years ago
  
  be565648
- [Eva] Minor rewritings in eva_audit. · 63626c79
  David Bühler authored 4 years ago
  
  63626c79
- [Eva] Moves audit functions in a new file utils/eva_audit.ml · 50fc3341
  David Bühler authored 4 years ago
  
  50fc3341
- [kernel] File: rewrites function [compute_sources_table]. · 89620efb
  David Bühler authored 4 years ago
  
  89620efb
- [kernel] File: fixes an abort message. · 2b9be50b
  David Bühler authored 4 years ago
  
  2b9be50b
- [kernel] File: new utilitary function [create_temp_file]. · e6bc8387
  David Bühler authored 4 years ago
  
  e6bc8387
- [kernel] File: renames [filepath_of_file] into [get_filepath]. · 1851b74f
  David Bühler authored 4 years ago
  
  Uses it in [get_name].
  1851b74f
- [tests] add tests for audit mode · 231552ec
  Andre Maroneze authored 4 years ago and David Bühler committed 4 years ago
  
  231552ec
- [Kernel/Eva] add audit options and checks · 1da1be72
  Andre Maroneze authored 4 years ago and David Bühler committed 4 years ago
  
  1da1be72
- [Eva] Renames the message key 'correctness' into 'config'. · 7f31522c
  David Bühler authored 4 years ago
  
  7f31522c
- [Eva] Optionally prints the status of Eva warning categories. · bed150f6
  David Bühler authored 4 years ago
  
  bed150f6
- [Eva] Optionally prints the correctness parameters of an analysis. · 429837b6
  David Bühler authored 4 years ago
  
  429837b6
- [logic] refine duplicate lemma error message · ac88b4ba
  Loïc Correnson authored 4 years ago
  
  ac88b4ba
- [logic] pretty-printing predicate kinds · 93637166
  Loïc Correnson authored 4 years ago
  
  93637166
- [kernel] fusion of admit lemmas and axioms · f45e591d
  Loïc Correnson authored 4 years ago
  
  f45e591d
Feb 17, 2021
- Update nix/frama-ci.* · 2fd32d15
  Virgile Prevosto authored 4 years ago
  
  2fd32d15
- [ci] use master branch of Frama-CI following merge · 3085bfa0
  Virgile Prevosto authored 4 years ago
  
  3085bfa0
- Merge branch 'feature/headers/2021' into 'master' · 5582b9c3
  Virgile Prevosto authored 4 years ago
  
  Bump © year to 2021 See merge request frama-c/frama-c!3063
  5582b9c3
- [headers] No headers in tests · d635d4a8
  Virgile Prevosto authored 4 years ago
  
  d635d4a8
- .gitignore · 345e0e0c
  Virgile Prevosto authored 4 years ago
  
  345e0e0c
- [Makefile] distribute cg_viewer.yes.ml even if current env does not have dgraph · af70a04a
  Virgile Prevosto authored 4 years ago
  
  af70a04a
- [man] simplify production of man/frama-c.1 · 91f1e6da
  Virgile Prevosto authored 4 years ago
  
  91f1e6da
- Merge branch 'feature/andre/libc-wcscasecmp' into 'master' · d6a60899
  Valentin Perrelle authored 4 years ago
  
  Feature/andre/libc wcscasecmp See merge request frama-c/frama-c!3056
  d6a60899
- [man] update URL of Frama-C BTS, bump © year and move to CC-BY-SA licence · 6dd62079
  Virgile Prevosto authored 4 years ago
  
  6dd62079
Feb 16, 2021
- Merge branch 'feature/automata/vertex-control-flow' into 'master' · 82a0d55a
  Valentin Perrelle authored 4 years ago
  
  [kernel] add vertex control-flow infos on automata See merge request frama-c/frama-c!3061
  82a0d55a