Commits · 419583f8c00dd12a9527c8498aa3f96b816f91fb · pub / frama-c · GitLab

Snippets Groups Projects

Apr 12, 2017
- Headers 2017 · 419583f8
  Virgile Prevosto authored 7 years ago
  
  419583f8
- [Makefile] Use CEA_LGPL from main directory when in internal mode · bc740bcb
  Virgile Prevosto authored 7 years ago
  
  bc740bcb
- [Makefile] Fixes headers target to do the correct thing in internal mode · 76fe9b59
  Virgile Prevosto authored 7 years ago
  
  Integration within main distribution might work at some non-so-far-way point in the future after all.
  76fe9b59
- Merge branch 'feature/virgile/transient-blocks' into 'stable/phosphorus' · 2b3312ae
  Virgile Prevosto authored 7 years ago
  
  handling of transient blocks See merge request !126
  2b3312ae
Apr 10, 2017
- update oracle · bb75804d
  Virgile Prevosto authored 7 years ago
  
  bb75804d
- update oracles · 32f1d4db
  Virgile Prevosto authored 7 years ago
  
  32f1d4db
- update oracle · 9c25d457
  Virgile Prevosto authored 7 years ago
  
  9c25d457
- Add test case for local_init with annotation and update gcc-e-acsl script · ff46b374
  Virgile Prevosto authored 8 years ago
  
  ff46b374
- update oracles · 1beb1ffd
  Virgile Prevosto authored 8 years ago
  
  1beb1ffd
- continue to debug transient blocks; generate much less brackets · 6f0bf770
  Julien Signoles authored 8 years ago and Virgile Prevosto committed 7 years ago
  
  6f0bf770
- [tests] add test for local_init (without oracle for the time being) · eb70f350
  Julien Signoles authored 8 years ago and Virgile Prevosto committed 7 years ago
  
  eb70f350
- fix bug with local init which contains an annotation · 09471b0c
  Julien Signoles authored 8 years ago and Virgile Prevosto committed 7 years ago
  
  09471b0c
- Merge branch 'cherry-pick-oracles' into 'stable/phosphorus' · 15b6816e
  Virgile Prevosto authored 7 years ago
  
  synchronize oracles See merge request !137
  15b6816e
- synchronize with frama-c/frama-c!1238 · 0ab988f4
  Tristan Le Gall authored 8 years ago and Virgile Prevosto committed 7 years ago
  
  0ab988f4
Apr 05, 2017
- Merge branch 'kostyantyn/feature/trivial-annot' into 'master' · f5239343
  Andre Maroneze authored 7 years ago
  
  [scripts] Do not use trivial-annotations by default See merge request !134
  f5239343
- [scripts] Do not use trivial-annotations by default · c0cd7ef3
  Kostyantyn Vorobyov authored 7 years ago
  
  c0cd7ef3
Mar 31, 2017
- Merge branch 'feature/andre/val-builtins-list' into 'master' · 975dd307
  Boris Yakobowski authored 7 years ago
  
  synchronize with frama-c/frama-c!1232 See merge request !131
  975dd307
- synchronize with frama-c/frama-c!1232 · a056d8c4
  Andre Maroneze authored 8 years ago
  
  a056d8c4
- Merge branch 'feature/eva/remove-redundant-alarms-default' into 'master' · 1bbba459
  Boris Yakobowski authored 7 years ago
  
  Adapt to trunk branch feature/eva/remove-redundant-alarms-default See merge request !132
  1bbba459
Mar 30, 2017
- Merge branch 'kostyantyn/bugfix/printf' into 'master' · dfbafbbf
  Julien Signoles authored 8 years ago
  
  Kostyantyn/bugfix/printf See merge request !129
  dfbafbbf
- [mmodel_analysis] simpler version for Env.check_heap_allocation + reindentation of do_call · 38f23015
  Julien Signoles authored 8 years ago
  
  38f23015
- Added test case checking initialization of memory layout · 9589568f
  Kostyantyn Vorobyov authored 8 years ago
  
  9589568f
- Fix an issue where shadowing has been performed without active layout · e21964f5
  Kostyantyn Vorobyov authored 8 years ago
  
  e21964f5
- Prevent heap-shadowing if the shadow layout has not been initialized · f3c8a4d6
  Kostyantyn Vorobyov authored 8 years ago
  
  f3c8a4d6
- Suppress a spurious warning in ocaml v4.04.0 · 55371cb9
  Kostyantyn Vorobyov authored 8 years ago
  
  55371cb9
Mar 29, 2017
- Adapt to trunk branch feature/eva/remove-redundant-alarms-default · ef3641da
  Boris Yakobowski authored 8 years ago
  
  ef3641da
Mar 28, 2017
- Fix failed test · 2ac4afb3
  Kostyantyn Vorobyov authored 8 years ago
  
  2ac4afb3
- Fix undefined behaviour in valid_block.c test case · 0709f38a
  Kostyantyn Vorobyov authored 8 years ago
  
  0709f38a
- changelog · 1a1b0df2
  Julien Signoles authored 8 years ago
  
  1a1b0df2
- Merge branch 'kostyantyn/feature/segment-update' into 'master' · 180dfda4
  Julien Signoles authored 8 years ago
  
  Segment-model update See merge request !107
  180dfda4
- Merge branch 'feature/andre/val-builtins-auto-default' into 'master' · c5d29fa4
  Boris Yakobowski authored 8 years ago
  
  synchronize with frama-c/frama-c!1214 See merge request !128
  c5d29fa4
- Changes as per MR review · 92c096e9
  Kostyantyn Vorobyov authored 8 years ago
  
  92c096e9
- changelog · 7d9c4380
  Julien Signoles authored 8 years ago
  
  7d9c4380
- Merge branch 'kostyantyn/bugfix/backtrace' into 'master' · 315fe00d
  Julien Signoles authored 8 years ago
  
  Fix for backtrace See merge request !127
  315fe00d
Mar 27, 2017
- synchronize with frama-c/frama-c!1214 · b7cda160
  Andre Maroneze authored 8 years ago
  
  b7cda160
- Fix test oracles · e16d250e
  Kostyantyn Vorobyov authored 8 years ago
  
  e16d250e
- Replace RTL linking via source compilation · 2e5b209a
  Kostyantyn Vorobyov authored 8 years ago
  
  2e5b209a
- Fix test failures · 30b6e885
  Kostyantyn Vorobyov authored 8 years ago
  
  30b6e885
- New functionslity in misc · 7c16aee7
  Kostyantyn Vorobyov authored 8 years ago
  
  7c16aee7
- Update translate.ml to handle constants in expressions when generating addresses · 85b26def
  Kostyantyn Vorobyov authored 8 years ago
  
  85b26def