Commits · fd5de66abb71b6183f3924960ff6d564b816a79e · pub / frama-c

Mar 13, 2013
- [E-ACSL] update according to kernel changes · fd5de66a
  Julien Signoles authored 12 years ago
  
  fd5de66a
Mar 07, 2013
- + get_sub · 01c55716
  Guillaume Petiot authored 12 years ago
  
  01c55716
Mar 04, 2013
- No commit message · 053d885d
  Guillaume Petiot authored 12 years ago
  
  No commit message
  053d885d
Feb 26, 2013
- [e-acsl] article in progress · 2baff9ce
  Guillaume Petiot authored 12 years ago
  
  2baff9ce
- [e-acsl] article in progress · c7f54cde
  Guillaume Petiot authored 12 years ago
  
  c7f54cde
- [e-acsl] __get_cont fixed · 43a06ae5
  Guillaume Petiot authored 12 years ago
  
  43a06ae5
Feb 22, 2013
- [e-acsl] + matmult example for experiments · 5fd78d4f
  Guillaume Petiot authored 12 years ago
  
  5fd78d4f
- [e-acsl] article in progress · dd6cf3a5
  Guillaume Petiot authored 12 years ago
  
  dd6cf3a5
Feb 21, 2013
- [e-acsl] article on progress · 2951fca9
  Guillaume Petiot authored 12 years ago
  
  2951fca9
Feb 20, 2013
- [e-acsl] article in progress · 088ac9a8
  Guillaume Petiot authored 12 years ago
  
  088ac9a8
- [e-acsl] memory-model article in progress · 7fc53e95
  Guillaume Petiot authored 12 years ago
  
  7fc53e95
Feb 19, 2013
- [e-acsl] memory-model article in progress · 0096fe19
  Guillaume Petiot authored 12 years ago
  
  0096fe19
Feb 08, 2013
- [E-acsl] Fix wrt change in Machdep · 03161035
  Boris Yakobowski authored 12 years ago
  
  03161035
Feb 04, 2013
- [e-acsl] bugfix 32 bits · 6c5d037b
  Guillaume Petiot authored 12 years ago
  
  6c5d037b
- [e-acsl] bugfix add_element · 662a5886
  Guillaume Petiot authored 12 years ago
  
  662a5886
- [e-acsl] father's mask recomputed after remove_element · a392ef02
  Guillaume Petiot authored 12 years ago
  
  a392ef02
- [e-acsl] Renamed function Cil.alignOf_int into Cil.bytesAlignOf · 5141907f
  Guillaume Petiot authored 12 years ago
  
  5141907f
Feb 01, 2013
- [e-acsl] algos are now correct · be25b486
  Guillaume Petiot authored 12 years ago
  
  be25b486
- [E-ACSL] update oracles according to kernel's and Value's changes · 675f630f
  Julien Signoles authored 12 years ago
  
  675f630f
- [e-acsl] - unused functions · e4544e85
  Guillaume Petiot authored 12 years ago
  
  e4544e85
Jan 31, 2013
- [E-ACSL] update oracles according to Value's changes (again) · 650812a4
  Julien Signoles authored 12 years ago
  
  650812a4
- [e-acsl] now using size_t instead of ulong · e9f65994
  Guillaume Petiot authored 12 years ago
  
  e9f65994
- [E-ACSL] update oracles according to Value's changes · 3fcc928e
  Julien Signoles authored 12 years ago
  
  3fcc928e
- [e-acsl] fix _get_exact · 01531700
  Guillaume Petiot authored 12 years ago
  
  01531700
- [e-acsl] better __debug function · 084bf338
  Guillaume Petiot authored 12 years ago
  
  084bf338
Jan 30, 2013
- [E-ACSL] headers 2013 · 9a68d8fe
  Julien Signoles authored 12 years ago
  
  9a68d8fe
Jan 25, 2013
- [E-ACSL] configure the memory model's C library with the Frama-C's machdep · 4308b243
  Julien Signoles authored 12 years ago
  
  4308b243
- [E-ACSL] + machdep 16/32/64 · 1ff9db31
  Guillaume Petiot authored 12 years ago
  
  1ff9db31
Jan 24, 2013
- [E-ACSL] install share/e_acsl.c · 44356c4f
  Julien Signoles authored 12 years ago
  
  [E-ACSL] e_acsl_assert now takes the crashing function in argument
  44356c4f
Jan 21, 2013
- [E-ACSL] better handling of already-proven properties · bc0f175b
  Julien Signoles authored 12 years ago
  
  bc0f175b
- [E-ACSL] remove debugging stuff + update oracles according to Value's change · 47dd0895
  Julien Signoles authored 12 years ago
  
  47dd0895
Jan 18, 2013
- [E-ACSL] new option -e-acsl-valid. Valid annotations are not translated by default anymore. · cde9885a
  Julien Signoles authored 12 years ago
  
  [E-ACSL] code of e_acsl_assert put in e_acsl.c (no more in e_acsl.h)
  cde9885a
Jan 09, 2013

[E-ACSL] handle specified function without code. BTW that fixes bugs #1300 and #1340. · f7a1cd74

Julien Signoles authored 12 years ago

[E-ACSL] convert postcondition even in presence of untranslated assigns clause
[E-ACSL] fix bug when the translation of a predicate containing \at is abruptely stopped because of a not-yet-implemented construct (the generated code contained undeclared __e_acsl_at variables)

f7a1cd74

Jan 04, 2013
- [E-ACSL] fixed bugs when calling 'generate_code' dynamically. BTW change the... · 950e347b
  Julien Signoles authored 12 years ago
  
  [E-ACSL] fixed bugs when calling 'generate_code' dynamically. BTW change the plug-in name of dynamic function
  950e347b
- [E-ACSL] comments · c3ed4c2e
  Julien Signoles authored 12 years ago
  
  c3ed4c2e
Dec 20, 2012
- [E-ACSL] support of ghost variables and statements · f22c9a75
  Julien Signoles authored 12 years ago
  
  f22c9a75
Dec 19, 2012
- [E-ACSL] update according to kenel's changes · 33e5c8b7
  Julien Signoles authored 12 years ago
  
  33e5c8b7
Dec 18, 2012
- [E-ACSL] update oracles with few less warnings · 1e07cc02
  Julien Signoles authored 12 years ago
  
  1e07cc02
Dec 17, 2012
- [E-ACSL] fixed bug #1333 about handling of unsupported constructs occurring during pre-analysis · 251fe58c
  Julien Signoles authored 12 years ago
  
  251fe58c
- [E-ACSL] fixed bug #1331 in presence of floats/reals in divisions or modulos · 582b7654
  Julien Signoles authored 12 years ago
  
  582b7654