Commits · 6ba21d1508a9602a9aab8d619d354ce0fde0a10e · pub / frama-c · GitLab

Snippets Groups Projects

Aug 02, 2017
- Initial RTL implementation of temporal analysis · 6ba21d15
  Kostyantyn Vorobyov authored 7 years ago
  
  6ba21d15
- Initial import of temporal analysis · c3b750ca
  Kostyantyn Vorobyov authored 7 years ago
  
  c3b750ca
- Move out handling initializers from vinit to vstmt. · 48635754
  Kostyantyn Vorobyov authored 7 years ago
  
  48635754
- Aligning small blocks during temporal analysis · 9339c414
  Kostyantyn Vorobyov authored 7 years ago
  
  9339c414
- Dummy temporal analysis · 0f4734e9
  Kostyantyn Vorobyov authored 7 years ago
  
  0f4734e9
- Add -e-acsl-temporal option · 979760f8
  Kostyantyn Vorobyov authored 7 years ago
  
  979760f8
- Refactor in mmodel_analysis + check whether expressions should be monitored · a844fff1
  Kostyantyn Vorobyov authored 7 years ago
  
  a844fff1
- Remove CRV'14 competition data: it has its own repository · d929a865
  Kostyantyn Vorobyov authored 7 years ago
  
  d929a865
- Remove obsolete tests for bittree · e6ee6182
  Kostyantyn Vorobyov authored 7 years ago
  
  e6ee6182
- Minor fixes and updates as per: · ad59fe1d
  Kostyantyn Vorobyov authored 7 years ago
  
  - Removal of manuals from standard distribution - Removal of jemalloc - Removal of full gmp library
  ad59fe1d
- Static modifiers · 33945798
  Kostyantyn Vorobyov authored 7 years ago
  
  33945798
- Remove jemalloc sources · c6f43be0
  Kostyantyn Vorobyov authored 7 years ago
  
  c6f43be0
- Fix initialization bug due to incorrectly computed mspace bounds · b32e0761
  Kostyantyn Vorobyov authored 7 years ago
  
  b32e0761
- Track main function · 2727be6c
  Kostyantyn Vorobyov authored 7 years ago
  
  2727be6c
- Prevent failures due to allocations exceeding the size of mspaces · 3ca721e9
  Kostyantyn Vorobyov authored 7 years ago
  
  3ca721e9
- Fix cleaning shadow layout · ad69f062
  Kostyantyn Vorobyov authored 7 years ago
  
  ad69f062
- dlmalloc compatible with segment model · 542c3b7c
  Kostyantyn Vorobyov authored 7 years ago
  
  542c3b7c
- Test oracles update · f88e29ce
  Kostyantyn Vorobyov authored 7 years ago
  
  f88e29ce
- Enable mspace allocations in bittree model · 99248aeb
  Kostyantyn Vorobyov authored 7 years ago
  
  99248aeb
- Partial integration of dlmalloc to the point generated programs are · 2ec8fd0b
  Kostyantyn Vorobyov authored 7 years ago
  
  compiled
  2ec8fd0b
- posix_memalign in dlmalloc · f4c041f9
  Kostyantyn Vorobyov authored 7 years ago
  
  f4c041f9
- Aligned alloc in dlmalloc · cade53a5
  Kostyantyn Vorobyov authored 7 years ago
  
  cade53a5
- dlmalloc with enhanced mspaces · 0d25c8c1
  Kostyantyn Vorobyov authored 7 years ago
  
  0d25c8c1
- Pristine version of dlmalloc · 010b1de3
  Kostyantyn Vorobyov authored 7 years ago
  
  010b1de3
- Renaming · a9af38b5
  Kostyantyn Vorobyov authored 7 years ago
  
  a9af38b5
- Rename memory_layout to shadow_layout as that's what it is · 879532b5
  Kostyantyn Vorobyov authored 7 years ago
  
  879532b5
- Separate function aliases into their own header · 7c0a6b37
  Kostyantyn Vorobyov authored 7 years ago
  
  7c0a6b37
- Track offset in global vars (prereq. to temporal analysis) · 6b73d17c
  Kostyantyn Vorobyov authored 7 years ago
  
  6b73d17c
- Add ability to add statements after statements in env · 711a3ed0
  Kostyantyn Vorobyov authored 7 years ago
  
  711a3ed0
- Several new options in e-acsl-gcc · d1ccca6d
  Kostyantyn Vorobyov authored 7 years ago
  
  d1ccca6d
- Weak validity in segment model · 548a008c
  Kostyantyn Vorobyov authored 7 years ago
  
  548a008c
- Comments · 7e3b240f
  Kostyantyn Vorobyov authored 7 years ago
  
  7e3b240f
- Initialize program arguments from within RTL · d5013fc0
  Kostyantyn Vorobyov authored 7 years ago
  
  d5013fc0
- Updated runtime reports · dcb26740
  Kostyantyn Vorobyov authored 7 years ago
  
  dcb26740
- Comments · faa0377b
  Kostyantyn Vorobyov authored 7 years ago
  
  faa0377b
- Set heap/stack shadow size via macros + debug macros · 195e1b45
  Kostyantyn Vorobyov authored 7 years ago
  
  195e1b45
- Minor refactoring in bittree model · 1e14663a
  Kostyantyn Vorobyov authored 7 years ago
  
  1e14663a
- Extra assertions in bittree · 53a3dd0e
  Kostyantyn Vorobyov authored 7 years ago
  
  53a3dd0e
Jul 25, 2017
- Merge branch 'feature/andre/snprintf-check-valid' into 'master' · 2d6a53e8
  Andre Maroneze authored 7 years ago
  
  sync with frama-c/frama-c!1344 See merge request !155
  2d6a53e8
Jul 12, 2017
- sync with frama-c/frama-c!1344 · 13dcbfaa
  Andre Maroneze authored 7 years ago
  
  13dcbfaa