Commits · 0e0e6451d34d7fd2b0d63100307b752036362faf · pub / frama-c · GitLab

Snippets Groups Projects

Mar 27, 2017
- Changed signature of valid to capture the address of the base pointer · 0e0e6451
  Kostyantyn Vorobyov authored 8 years ago
  
  Forward requirement for temporal analysis so referent number of a pointer can be accessed
  0e0e6451
- Fix Misc.mk_call so it can generate calls with no arguments · fd14faff
  Kostyantyn Vorobyov authored 8 years ago
  
  fd14faff
- Fixed related to a rebase against the master branch · e102f59d
  Kostyantyn Vorobyov authored 8 years ago
  
  e102f59d
- Fix small issue in misc.ml · 2d7f8bbf
  Kostyantyn Vorobyov authored 8 years ago
  
  2d7f8bbf
- Remane readonly to mark_readonly and More defensive macros · 38dd0000
  Kostyantyn Vorobyov authored 8 years ago
  
  38dd0000
- Stylistic updates and minor refactoring using allocated function · a8666eb0
  Kostyantyn Vorobyov authored 8 years ago
  
  a8666eb0
- General allocation function. · 0f72cf0b
  Kostyantyn Vorobyov authored 8 years ago
  
  For the time being it is very similar to valid read, but it should take over because valid is to be extended with temporal problems, so this is a way to check against blocks being allocated solely
  0f72cf0b
- Refactoring and bugfixes brought forward from temporal patch · eaadad8a
  Kostyantyn Vorobyov authored 8 years ago
  
  eaadad8a
- Stylistic updates · d7190e1d
  Kostyantyn Vorobyov authored 8 years ago
  
  d7190e1d
- Stylistic fixes in misc.ml and located in ptr_index · 31942261
  Kostyantyn Vorobyov authored 8 years ago
  
  31942261
- Comments · 7e8028ae
  Kostyantyn Vorobyov authored 8 years ago
  
  7e8028ae
- Remove obsolete debug code · c278a2bd
  Kostyantyn Vorobyov authored 8 years ago
  
  c278a2bd
- Added a new test case for checking detection of block-level accessses · 08a5f4ca
  Kostyantyn Vorobyov authored 8 years ago
  
  08a5f4ca
- Detect illegal accesses to allocated memory. · 6cb5d379
  Kostyantyn Vorobyov authored 8 years ago
  
  \valid(p+i) now additionally checks whether p and p+i point to the same block
  6cb5d379
- Segment-model: remove meta-segments and use larger block segments · 2118ef54
  Kostyantyn Vorobyov authored 8 years ago
  
  2118ef54
- Updates to bit-level manipulation header · b2353a2b
  Kostyantyn Vorobyov authored 8 years ago
  
  b2353a2b
Mar 23, 2017
- Merge branch 'feature/andre/calloc-spec' into 'master' · 75d22798
  Boris Yakobowski authored 7 years ago
  
  synchronize with frama-c!1187 See merge request !125
  75d22798
- synchronize with frama-c!1187 · 289eb7ff
  Andre Maroneze authored 7 years ago
  
  289eb7ff
Mar 22, 2017
- Fix oracles broken by merge · ab28bf15
  Boris Yakobowski authored 7 years ago
  
  ab28bf15
- Merge branch 'feature/virgile/fix-vla' into 'master' · 1ba762d9
  Boris Yakobowski authored 7 years ago
  
  More consistent handling of blocks and Local_init See merge request !123
  1ba762d9
Mar 21, 2017
- Update to new kernel API · ef72520a
  Virgile Prevosto authored 7 years ago
  
  ef72520a
- Merge branch 'kostyantyn/feature/check-option' into 'master' · d08751a6
  Kostyantyn Vorobyov authored 7 years ago
  
  Add --check option to e-acsl-gcc.sh + minior updates See merge request !124
  d08751a6
- Enable check option by default when --rt-debug flag is specified · 1e7c1f46
  Kostyantyn Vorobyov authored 7 years ago
  
  1e7c1f46
- Add --check option to e-acsl-gcc.sh + minior updates · ebc8e11b
  Kostyantyn Vorobyov authored 8 years ago
  
  ebc8e11b
- Merge branch 'kostyantyn/bugfix/local-init-goto' into 'master' · d57c3806
  Julien Signoles authored 7 years ago
  
  Fix incorrect tracking of local variables when processing goto statements See merge request !122
  d57c3806
- Small changes as per Julien's review · e0e7c027
  Kostyantyn Vorobyov authored 7 years ago
  
  e0e7c027
- [changelog] fix typo · 3336c49e
  Julien Signoles authored 7 years ago
  
  3336c49e
Mar 17, 2017
- Fix a bug resulting in deletion of undeclared variables via a goto jump · 6053f855
  Kostyantyn Vorobyov authored 8 years ago
  
  6053f855
- More consistent handling of blocks and Local_init · 23bc8836
  Virgile Prevosto authored 8 years ago
  
  23bc8836
Mar 10, 2017
- Merge branch 'feature/vla' into 'master' · 137df6ee
  Andre Maroneze authored 8 years ago
  
  Feature/vla See merge request !120
  137df6ee
Mar 09, 2017
- update oracles against kernel changes · 112f61b5
  Virgile Prevosto authored 8 years ago
  
  112f61b5
- upgrade to new kernel API · 2ca2889b
  Virgile Prevosto authored 8 years ago
  
  2ca2889b
- Better handling of local initializers · 9e004f71
  Virgile Prevosto authored 8 years ago
  
  9e004f71
- update oracles · e61e4cee
  Virgile Prevosto authored 8 years ago
  
  e61e4cee
- fixes fragile pattern-matchings · 8eaf1413
  Virgile Prevosto authored 8 years ago
  
  8eaf1413
- Add support for local var initialization · 4afbb998
  Virgile Prevosto authored 8 years ago
  
  4afbb998
Mar 08, 2017
- Merge branch 'feature/variadic/rename-command-line-arguments' into 'master' · 2a47b7bd
  Andre Maroneze authored 8 years ago
  
  Use the new arguments name for the variadic plugin. See merge request !121
  2a47b7bd
- Use the new arguments name for the variadic plugin. · f55bf386
  Valentin Perrelle authored 8 years ago
  
  f55bf386
- Merge branch 'feature/eva/rm-value' into 'master' · f5bd26cf
  Julien Signoles authored 8 years ago
  
  Synchronize with Frama-C branch feature/eva/rm-value Closes #41 See merge request !119
  f5bd26cf
Mar 07, 2017
- Update test to use Eva · f99a0945
  Boris Yakobowski authored 8 years ago
  
  f99a0945