Commits · master · pub / meta

21 Jan, 2021 3 commits
- Merge branch 'bugfix/patrick/A228' into 'master' · d7e53454
  Patrick Baudin authored Jan 21, 2021
```
next to a WP fix about smp_eq_with_lor

See merge request frama-c/meta!35
```
  d7e53454
- [tests] ensure Eva is launched after Wp in uncalled.c · 398b6f18
  Virgile Prevosto authored Jan 21, 2021
  
  398b6f18
- next to a WP fix about smp_eq_with_lor · 0c24bf0a
  Patrick Baudin authored Jan 21, 2021
  
  0c24bf0a
12 Jan, 2021 1 commit
- Merge branch 'feature/basile/update-machdep-default' into 'master' · 4c0675cf
  Andre Maroneze authored Jan 12, 2021
```
[tests] Update tests for new machdep default in Frama-C

See merge request frama-c/meta!32
```
  4c0675cf
05 Jan, 2021 1 commit
- Merge branch 'feature/andre/extlib-migrate-408' into 'master' · 7f09fd51
  Virgile Robles authored Jan 05, 2021
```
Refactoring related to OCaml 4.08 and frama-c/frama-c!3005

See merge request frama-c/meta!33
```
  7f09fd51
23 Dec, 2020 1 commit
- synchronize with frama-c/frama-c!3005 · 7bb578a4
  Andre Maroneze authored Dec 23, 2020
  
  7bb578a4
16 Dec, 2020 1 commit
- [tests] Update tests for new machdep default in Frama-C · 437ac55c
  Basile Desloges authored Dec 15, 2020
  
  437ac55c
09 Dec, 2020 1 commit
- Makefile: correct share dir name · 4a68dd2f
  Virgile Robles authored Dec 09, 2020
  
  4a68dd2f
22 Nov, 2020 3 commits
- [annotate] Fix AST · 0587c4b9
  Virgile Robles authored Nov 22, 2020
  
  0587c4b9
- [annotate] Ignore unspecified sequence attributes for reading · 40748e2a
  Virgile Robles authored Nov 22, 2020
  
  40748e2a
- [annotate] Do not ignore simpl flag · bd96e3b3
  Virgile Robles authored Nov 22, 2020
  
  bd96e3b3
12 Nov, 2020 3 commits
- Merge branch 'add_conditional_invariant' into 'master' · e9f160d4
  Virgile Prevosto authored Nov 12, 2020
```
Add conditional invariant context

See merge request frama-c/meta!30
```
  e9f160d4
- [readme] fixes typos · bdb8efd4
  Virgile Prevosto authored Nov 12, 2020
  
  bdb8efd4
- [proofs] parametrize program · 1b6a8b61
  Virgile Robles authored Nov 12, 2020
  
  1b6a8b61
11 Nov, 2020 2 commits
- [proofs] recordize func type for further additions · 6a24bf61
  Virgile Robles authored Nov 12, 2020
  
  6a24bf61
- [proofs] recordize prop type · 4933d603
  Virgile Robles authored Nov 11, 2020
  
  4933d603
09 Nov, 2020 1 commit
- [deduction] Retry when Prolog times out · ed7c5e51
  Virgile Robles authored Nov 09, 2020
  
  ed7c5e51
06 Nov, 2020 3 commits
- Correct conditional invariant generation · 7d118479
  Virgile Robles authored Nov 06, 2020
  
  7d118479
- Update test oracles · 0f9afe6c
  Virgile Robles authored Nov 06, 2020
  
  0f9afe6c
- Add conditional invariant context · c7e28528
  Virgile Robles authored Nov 06, 2020
  
  c7e28528
05 Nov, 2020 7 commits
- Merge branch 'stable/titanium' · b970ffdf
  Virgile Prevosto authored Nov 05, 2020
  
  b970ffdf
- shorter option name for separating annotations + update README · 4c29c7bb
  Virgile Prevosto authored Nov 05, 2020
  
  4c29c7bb
- Merge branch 'feature/separate-annot' into 'stable/titanium' · 1815c5ce
  Virgile Robles authored Nov 05, 2020
```
Option for putting generated annotations on their own instruction

See merge request frama-c/meta!29
```
  1815c5ce
- [tests] ensure name of generated temp file does not appear in oracles · 02a45c9a
  Virgile Prevosto authored Nov 05, 2020
  
  02a45c9a
- add test for separation of annotations to distinct statements · 91a4e3c9
  Virgile Prevosto authored Nov 05, 2020
  
  91a4e3c9
- [translation] add option to have annotation on separate (nop) instructions · 59cb2bb8
  Virgile Prevosto authored Nov 02, 2020
```
allows for a stricter sequencing of annotations against each other.
```
  59cb2bb8
- Merge branch 'fix/integrity-check-failure' into 'stable/titanium' · 1ff27022
  Virgile Robles authored Nov 05, 2020
```
Ensure that AST after MetAcsl run passes integrity check

See merge request frama-c/meta!28
```
  1ff27022
04 Nov, 2020 9 commits
- update wp-cache · f4d0ba0b
  Virgile Prevosto authored Nov 04, 2020
  
  f4d0ba0b
- do not use varinfos in external assoc list for ACSL extensions · cb27c0fb
  Virgile Prevosto authored Nov 04, 2020
```
Especially if there is a copy visitor that operates between the time
when the table is filled and when it is used. Integrity of the new AST will
suffer...
```
  cb27c0fb
- fix typing of generated realloc call · 868c064f
  Virgile Prevosto authored Nov 04, 2020
  
  868c064f
- recompute cfg when adding code for metavariables bindings · bb185b9e
  Virgile Prevosto authored Nov 04, 2020
  
  bb185b9e
- preserve unicity of logic_var records during alpha renaming · 7988bcdf
  Virgile Prevosto authored Nov 04, 2020
  
  7988bcdf
- do not generate status proxy for requires of an uncalled function · 1c7c9cec
  Virgile Prevosto authored Nov 04, 2020
  
  1c7c9cec
- [tests] requires of main are no longer considered valid by CallPrecondition · 7762e5bb
  Virgile Prevosto authored Nov 04, 2020
```
They should never had been so. Possibly a side-effect of properly marking
AST as grown/changed after the translation?
```
  7762e5bb
- force cfg recomputation when adding statements and signal that AST has changed · 27eca8c6
  Virgile Prevosto authored Nov 04, 2020
  
  27eca8c6
- trigger integrity check at end of transformation when -check is enabled · 4a4a0c59
  Virgile Prevosto authored Nov 04, 2020
  
  4a4a0c59
03 Nov, 2020 1 commit
- [why3] Cleanup and stronger definition · 38634def
  Virgile Robles authored Nov 03, 2020
  
  38634def
27 Oct, 2020 3 commits
- Merge branch 'stable/titanium' · e5d0f3d7
  Virgile Prevosto authored Oct 27, 2020
  
  e5d0f3d7
- Merge branch 'fix/union-simpl' into 'stable/titanium' · 6ae75d54
  Virgile Prevosto authored Oct 27, 2020
```
Do not oversimplify unions

See merge request frama-c/meta!27
```
  6ae75d54
- Do not oversimplify unions · 97e30b9a
  Virgile Robles authored Oct 27, 2020
  
  97e30b9a