Commits · 40d0adc3b1fe401ec24fe3f2523b8a5929ff92ac · pub / frama-c

May 11, 2011
- [e-acsl] fixed broken previous commit · 40d0adc3
  Julien Signoles authored 13 years ago
  
  [e-acsl] add guard before divisions and modulos
  40d0adc3
- comment API of internal module Visit.New_vars + factorize code for CInt64 · 2552cff1
  Julien Signoles authored 13 years ago
  
  2552cff1
- [e-acsl] shorter name for generated variable · ea4fd21a
  Julien Signoles authored 13 years ago
  
  ea4fd21a
May 05, 2011
- update oracles according to changes of kernel message · 96fd47bd
  Julien Signoles authored 13 years ago
  
  96fd47bd
May 04, 2011
- svnignore ok again · 0ca5c947
  Julien Signoles authored 13 years ago
  
  0ca5c947
- global svn:ignore · 01dd3ae8
  Benjamin Monate authored 13 years ago
  
  01dd3ae8
May 03, 2011
- upgrade to new kernel API · 61b08f91
  Virgile Prevosto authored 13 years ago
  
  61b08f91
Apr 28, 2011
- updating oracles according to kernel changes · 0c776cdd
  Julien Signoles authored 13 years ago
  
  0c776cdd
Apr 22, 2011

- update tests according to new messages of Value · b76e04d6

Julien Signoles authored 13 years ago

- update TODO-list
- location for new constructs whenever possible
- additional warnings when guards are missing

b76e04d6

Apr 13, 2011
- \valid* now not implemented, update TODO · 4605b83e
  Julien Signoles authored 13 years ago
  
  4605b83e
Apr 06, 2011
- in tests, use @frama-c@, not a direct call to frama-c · 8dbbd674
  Virgile Prevosto authored 13 years ago
  
  8dbbd674
Apr 05, 2011
- [e-acsl] updating oracle according to kernel changes · d1b21266
  Julien Signoles authored 13 years ago
  
  d1b21266
Apr 04, 2011
- ptests works better when it has a result directory where it can put files · 6630a082
  Virgile Prevosto authored 13 years ago
  
  6630a082
Mar 30, 2011
- fix install target for use as internal plugin · 1ab0e818
  Virgile Prevosto authored 14 years ago
  
  1ab0e818
Mar 25, 2011
- updating according to changes in Frama-C kernel · edb12060
  Julien Signoles authored 14 years ago
  
  edb12060
Mar 24, 2011
- more readable Makefile · ef077987
  Julien Signoles authored 14 years ago
  
  ef077987
- posix 'make install' + make uninstall · 62c0e613
  Julien Signoles authored 14 years ago
  
  62c0e613
- fix install issue in internal plugin mode · 6946b797
  Virgile Prevosto authored 14 years ago
  
  6946b797
Mar 22, 2011

[e-acsl] implement options for direct linking with GMP · 3ec70885

Julien Signoles authored 14 years ago

[e-acsl] Makefile's target 'install'
[e-acsl] test GMP linkage in non-regression suite ('make tests' now requires GMP >= 4.3.2)
[e-acsl] fixed bugs of GMP compatibility

3ec70885

Mar 17, 2011
- fixed bug · d518b849
  Julien Signoles authored 14 years ago
  
  d518b849
- - [configure] search GMP sources · 1d86aa12
  Julien Signoles authored 14 years ago
  
  - [Makefile] better generation of local_config.ml - [Options] new options for customized code generation (unused yet)
  1d86aa12
- check c libraries in configure · 1296a4e4
  Julien Signoles authored 14 years ago
  
  1296a4e4
- fixing typing in e_acsl.h · d4947ac1
  Julien Signoles authored 14 years ago
  
  d4947ac1
Mar 15, 2011

[E-ACSL] UseUnicode --> Unicode · bf8d5cb5

Julien Signoles authored 14 years ago

[E-ACSL] use -e-acsl-check for all tests
[E-ACSL] prepare guarding division and module (commented code yet)

bf8d5cb5

Mar 11, 2011
- upgrading oracles according to bug fixed #744 · 23825e33
  Julien Signoles authored 14 years ago
  
  23825e33
Mar 10, 2011
- update TODO-list · a73ef1f1
  Julien Signoles authored 14 years ago
  
  a73ef1f1
- updating tests according to improved pretty printer + tests of boolean binop · 9eb4abca
  Julien Signoles authored 14 years ago
  
  9eb4abca
Mar 08, 2011
- - unary/binary relation over terms. However: · 54d5d239
  Julien Signoles authored 14 years ago
  
  o logical operators still don't work o pointer operators untested - bug fixed with type of int64 constants
  54d5d239
- - use function mpz_init_set when possible · b14e5d02
  Julien Signoles authored 14 years ago
  
  - improve efficiency of mpz_clear generation - don't run cast.i anymore (waiting for fixing issue #744) - refactoring generation of new variables with their related stmts
  b14e5d02
- removing argument is_global which was actuelly useless · 1aad1f95
  Julien Signoles authored 14 years ago
  
  1aad1f95
Mar 07, 2011
- archiving TODO-list + no more constructor Before in the Frama-C kernel · f3e8818c
  Julien Signoles authored 14 years ago
  
  f3e8818c
Mar 04, 2011
- refactoring (new module Mpz) · 4c84b94f
  Julien Signoles authored 14 years ago
  
  4c84b94f
- some easy constructs (cast*, align*, addrOf) · d7ad60ea
  Julien Signoles authored 14 years ago
  
  d7ad60ea
- valid_range + valid_index · 5252820a
  Julien Signoles authored 14 years ago
  
  5252820a
- fix generation of big integer constants (in the limit of issue #745) · 56ccac56
  Julien Signoles authored 14 years ago
  
  56ccac56
- handling C variables in terms (will be improved when fixing issue #744) + good test for Pnot · 889fe582
  Julien Signoles authored 14 years ago
  
  889fe582
- - support of -e-acsl-check · 1a689817
  Julien Signoles authored 14 years ago
  
  - reject \valid - improve efficiency for vstmt_aux
  1a689817
- no more utf8 in generated C code · 5510359d
  Julien Signoles authored 14 years ago
  
  5510359d
- testing relations · b17aeb16
  Julien Signoles authored 14 years ago
  
  b17aeb16
- little memoisation for integer constants · df697e32
  Julien Signoles authored 14 years ago
  
  df697e32