Commits · b6ba91f158b3f25bd087c5cc2f17f9ce583e0ea1 · pub / frama-c

Jan 11, 2023
- [logic] accept \ghost attribute in types, notably casts · b6ba91f1
  Virgile Prevosto authored 2 years ago
  
  Fixes #2638
  b6ba91f1
Sep 21, 2022
- [Extlib] removed filter_out · 64850dc1
  Allan Blanchard authored 2 years ago
  
  64850dc1
Jul 28, 2022
- [parsing] add missing cases in wildcard rules of ACSL parser · 6fcf509c
  Virgile Prevosto authored 2 years ago
  
  6fcf509c
Apr 19, 2022
- [parser] fix rule name · 8c124bd9
  Virgile Prevosto authored 3 years ago
  
  8c124bd9
- [Logic] accepts integer/real as C field · 5334a89c
  Patrick Baudin authored 3 years ago and Virgile Prevosto committed 3 years ago
  
  5334a89c
Feb 23, 2022
- [2022] file headers · 7b02c99c
  Patrick Baudin authored 3 years ago
  
  7b02c99c
Nov 24, 2021
- [kernel] removes deprecated custom annot · 4a600438
  Allan Blanchard authored 3 years ago
  
  4a600438
Feb 18, 2021
- [kernel] fusion of admit lemmas and axioms · f45e591d
  Loïc Correnson authored 4 years ago
  
  f45e591d
Feb 16, 2021
- [headers] 2021 headers · 5a58b23c
  Virgile Prevosto authored 4 years ago
  
  5a58b23c
Feb 03, 2021
- [kernel] New predicate kind: Assert, Check or Admit. · 49f1590f
  David Bühler authored 4 years ago
  
  49f1590f
Jan 13, 2021
- Add location information for many not_yet_implemented errors · c72f4226
  Virgile Prevosto authored 4 years ago
  
  c72f4226
- [logic] Allows any integral constant in an array size, not just decimal ones. · 5f1eaa82
  Virgile Prevosto authored 4 years ago
  
  5f1eaa82
Nov 12, 2020
- [kernel] New warning category for multiple froms · b2df74b1
  Allan Blanchard authored 4 years ago
  
  b2df74b1
Nov 06, 2020
- [parser] Adds warning when dropping froms · e6b7c454
  Allan Blanchard authored 4 years ago
  
  e6b7c454
- [parser] Narrow froms in case of inclusion · f8f9cd0f
  Allan Blanchard authored 4 years ago
  
  f8f9cd0f
- [kernel] Simplifies merge assigns · a0ada244
  Allan Blanchard authored 4 years ago
  
  a0ada244
Nov 05, 2020
- [kernel] Clean from but do not merge them · 637af0a0
  Allan Blanchard authored 4 years ago
  
  637af0a0
- [parser] Update comment · ca041e19
  Allan Blanchard authored 4 years ago
  
  ca041e19
- [parser] Merge assigns dependencies · 336f28f6
  Allan Blanchard authored 4 years ago
  
  336f28f6
- [parser] Merge "assigns x, x, ..." · 3ce322ba
  Allan Blanchard authored 4 years ago
  
  3ce322ba
Oct 14, 2020
- Add support of recursive extended global annotations · 7295a3eb
  Lionel Blatter authored 4 years ago and Virgile Prevosto committed 4 years ago
  
  7295a3eb
Sep 15, 2020
- [logic] allow empty list of arguments after an extension keyword. · bd9be0d6
  Virgile Prevosto authored 4 years ago
  
  bd9be0d6
Sep 10, 2020
- [kernel] support for parsing/printing check of generalized invariant · 0d2b237b
  Virgile Prevosto authored 4 years ago
  
  0d2b237b
- [parser] prepare parser for generalized 'check' keyword · 69950db6
  Virgile Prevosto authored 4 years ago
  
  69950db6
Mar 27, 2020
- [parser] Fix long-standing shift/reduce conflict in logic parser · 8e553747
  Virgile Prevosto authored 5 years ago
  
  original issue introduced here: b9a1eb43
  8e553747
- [Logic] New predicate object_pointer. Not yet supported by the plugins. · 5b4c1196
  David Bühler authored 5 years ago
  
  5b4c1196
Mar 16, 2020
- [ACSL] fixes casts to unsigned short int · 2653a4e6
  Patrick Baudin authored 5 years ago
  
  2653a4e6
Mar 06, 2020
- update copyright to 2020 · 325661e6
  Andre Maroneze authored 5 years ago and Virgile Prevosto committed 5 years ago
  
  325661e6
Feb 13, 2020
- [kernel] Acsl_extension.category is not an option anymore · 68af70f7
  Allan Blanchard authored 5 years ago and Virgile Prevosto committed 5 years ago
  
  68af70f7
- [Parsing] lexical transformation for ACSL extensions · 69731fb8
  Allan Blanchard authored 5 years ago and Virgile Prevosto committed 5 years ago
  
  69731fb8
Oct 03, 2019
- [logic] fix qualifier parsing · b9a1eb43
  Virgile Prevosto authored 5 years ago
  
  b9a1eb43
Jul 12, 2019
- [lex/yacc] supression of Psubtype and PLsubtype (jessie) · 17f1af2c
  Patrick Baudin authored 5 years ago
  
  17f1af2c
Jun 28, 2019
- supression of TCoerce, TCoerceE, PLcoercion and PLCoercionE · bf154b79
  Tristan Le Gall authored 6 years ago and Julien Signoles committed 5 years ago
  
  bf154b79
- supression of Psubtype and PLsubtype (jessie) · d5b08c0d
  Tristan Le Gall authored 6 years ago and Julien Signoles committed 5 years ago
  
  d5b08c0d
Jun 19, 2019
- [ACSL] fixes bug with the precedence of \in (to be cont.) · bd92e903
  Patrick Baudin authored 5 years ago
  
  bd92e903
Apr 15, 2019
- [ACSL] fixes parsing issues about C fields · c4daae63
  Patrick Baudin authored 6 years ago
  
  c4daae63
- [ACSL] grammar extension for ACSL-importer · f277c11a
  Patrick Baudin authored 6 years ago
  
  f277c11a
Mar 05, 2019

[Kernel] New assertion kind: Assert or Check. · 30cee395

David Bühler authored 6 years ago and

Virgile Prevosto committed 6 years ago

Asserts are both evaluated and used as hypotheses afterwards.
Checks are only evaluated, but are not used as hypotheses: they must not affect
the analyses.

30cee395

Feb 05, 2019
- Merge branch 'feature/server/plugin' of git.frama-c.com:frama-c/frama-c into feature/server/plugin · 4bf2c145
  Loïc Correnson authored 6 years ago
  
  4bf2c145
Jan 21, 2019
- [Headers] upgrade distributed files · 45f9b04a
  Loïc Correnson authored 6 years ago
  
  (blind make headers from specifications)
  45f9b04a