Commits · c80b4dda7d4aeec42342d3505cd0011141aab79d · pub / frama-c · GitLab

Snippets Groups Projects

Jun 20, 2022
- [e-acsl] review · c80b4dda
  Thibaut Benjamin authored 2 years ago
  
  c80b4dda
- [e-acsl] typing contexts for binary relations · 66e9bb5c
  Thibaut Benjamin authored 2 years ago
  
  66e9bb5c
- [e-acsl] fourth review · f49affc6
  Thibaut Benjamin authored 2 years ago
  
  f49affc6
- [e-acsl] update oracles · 08404489
  Thibaut Benjamin authored 2 years ago
  
  08404489
- [e-acsl] translation preserve C types · a877440a
  Thibaut Benjamin authored 2 years ago
  
  a877440a
- [e-acsl] typing specific types moved to analyses_types · c9c5d089
  Thibaut Benjamin authored 2 years ago
  
  c9c5d089
- [e-acsl] third review · e2662519
  Thibaut Benjamin authored 2 years ago
  
  e2662519
- [e-acsl] refactor types for interval and typing · cddcb896
  Thibaut Benjamin authored 2 years ago
  
  cddcb896
- [e-acsl] first review · e13e1baf
  Thibaut Benjamin authored 2 years ago
  
  e13e1baf
- [e-acsl] fix typing bug with at translations · b6be8a9e
  Thibaut Benjamin authored 3 years ago
  
  b6be8a9e
- [e-acsl] fixpoint for recursive functions · a8b350c2
  Thibaut Benjamin authored 3 years ago
  
  a8b350c2
- [e-acsl] bugfix: function typing with gmp_only option · 9ddb5792
  Thibaut Benjamin authored 3 years ago
  
  9ddb5792
Jun 17, 2022
- [e-acsl] update oracles · 7fc6036c
  Thibaut Benjamin authored 3 years ago
  
  7fc6036c
- [e-acsl] code simplification · 68987122
  Thibaut Benjamin authored 3 years ago
  
  68987122
- [e-acsl] add logic functions · 9ce6a32b
  Thibaut Benjamin authored 3 years ago
  
  9ce6a32b
- [e-acsl] compute interval during at generation · ed599deb
  Thibaut Benjamin authored 3 years ago
  
  ed599deb
- [e-acsl] add interval inference for quantifiers · 75e0727f
  Thibaut Benjamin authored 3 years ago
  
  75e0727f
- [e-acsl] deprecate type_term and type_predicate · d5935aa3
  Thibaut Benjamin authored 3 years ago
  
  d5935aa3
- [e-acsl] intervals for \let constructor · baf10035
  Thibaut Benjamin authored 3 years ago
  
  baf10035
- [e-acsl] better recursion during interval phase · 287f6d07
  Thibaut Benjamin authored 3 years ago
  
  287f6d07
- [e-acsl] interval perform recursion on predicates · ff4eb3a1
  Thibaut Benjamin authored 3 years ago
  
  ff4eb3a1
- [e-acsl] linear typing for arithmetic operations · 24c29ebf
  Thibaut Benjamin authored 3 years ago
  
  24c29ebf
- [e-acsl] new interface for logic environment · 8137f198
  Thibaut Benjamin authored 3 years ago
  
  8137f198
- [e-acsl] auxilliary functions for error management · 38322971
  Thibaut Benjamin authored 3 years ago
  
  38322971
Jun 16, 2022
- Merge branch 'fix/ghost/result_type' into 'master' · 1d7b6e92
  Virgile Prevosto authored 2 years ago
  
  [kernel] fix \result type for ghost functions See merge request frama-c/frama-c!3778
  1d7b6e92
- Merge remote-tracking branch 'origin/stable/manganese' · ccca90c3
  Virgile Prevosto authored 2 years ago
  
  ccca90c3
- [tests] add variation on \ghost result type and assigns test · eea8022a
  Virgile Prevosto authored 2 years ago
  
  eea8022a
- [kernel] minor refactoring (Kernel_function.get_vi instead of pattern-match) · baaea844
  Virgile Prevosto authored 2 years ago
  
  baaea844
- [kernel] fix typing of \result for ghost functions · 6b174499
  Allan Blanchard authored 2 years ago and Virgile Prevosto committed 2 years ago
  
  6b174499
Jun 15, 2022
- Merge branch 'fix/ci/ocamlfind-version' into 'master' · ee8a0822
  Allan Blanchard authored 2 years ago
  
  [ci] downgrade ocamlfind See merge request frama-c/frama-c!3798
  ee8a0822
- [ci] downgrade ocamlfind · 72ff70fa
  Allan Blanchard authored 2 years ago
  
  72ff70fa
Jun 14, 2022
- Merge branch 'fix/andre/cil-types-debug-bugs' into 'master' · 57e4b3d1
  Virgile Prevosto authored 2 years ago
  
  [Kernel] avoid recursion and fix layout of debug pretty-printers See merge request frama-c/frama-c!3784
  57e4b3d1
- Merge branch 'fix/andre/hdrck-double-slashes' into 'master' · 435742b9
  Patrick Baudin authored 2 years ago
  
  [hdrck] avoid double slashes when concatenating paths See merge request frama-c/frama-c!3795
  435742b9
- [hdrck] avoid double slashes when concatenating paths · ef531e26
  Andre Maroneze authored 3 years ago
  
  ef531e26
- Merge branch 'fix/andre/glibc-2-35-predefs' into 'master' · a375065f
  Virgile Prevosto authored 2 years ago
  
  [Kernel] add predefined macros to avoid compiler warnings See merge request frama-c/frama-c!3787
  a375065f
Jun 13, 2022
- Merge branch 'fix/eva/results' into 'stable/manganese' · 6088e10f
  David Bühler authored 2 years ago
  
  [Eva] Changes the opening comment of the not so experimental Results interface. See merge request frama-c/frama-c!3793
  6088e10f
- [Eva] Changes the opening comment of the not so experimental Results interface. · 46478bb1
  David Bühler authored 2 years ago
  
  46478bb1
- Merge branch 'fix/e-acsl/headers' into 'stable/manganese' · 3c551593
  François Bobot authored 2 years ago
  
  Fix E-ACSL header date See merge request frama-c/frama-c!3789
  3c551593
Jun 10, 2022
- Merge branch 'feature/patrick/fixes-syntax' into 'master' · 6b1ea313
  Patrick Baudin authored 2 years ago
  
  Fixes syntax on some ML files See merge request frama-c/frama-c!3790
  6b1ea313
- [lint] allows wildcards · 9f5ab7b2
  Patrick Baudin authored 2 years ago
  
  9f5ab7b2