Commits · 4cd013c9ab68b448bf0a5aa051b1ad93d6eee686 · pub / frama-c

Jun 19, 2020
- [eacsl] Update tests · 4cd013c9
  Basile Desloges authored 4 years ago
  
  4cd013c9
Aug 30, 2019
- [tests] gmp-only · 31ef7f84
  Julien Signoles authored 5 years ago
  
  31ef7f84
- [tests] rename gmp to arith and runtime to memory · c1e98626
  Julien Signoles authored 5 years ago
  
  c1e98626
Jan 25, 2017
- fix bug with typing of unary and binary operators (fix git issue #37) · 03cd4cee
  Julien Signoles authored 8 years ago
  
  03cd4cee
Jun 09, 2016
- [tests] add JFLA'15 example · 824bee47
  Julien Signoles authored 8 years ago
  
  824bee47
Feb 10, 2016
- [tests] remove 'COMMENT: no diff' from gmp test cases · 7e0d4d05
  Julien Signoles authored 9 years ago
  
  7e0d4d05
- [tests] grow up constant value because of previous change from 32-bit to 64-bit test · 5e995f77
  Julien Signoles authored 9 years ago
  
  5e995f77
- [tests] simplify run of gmp tests · b483da32
  Julien Signoles authored 9 years ago
  
  b483da32
- [tests] moving GMP-specific test files · d97c6f2f
  Julien Signoles authored 9 years ago
  
  d97c6f2f
- [tests] Compare the generated code just after running Value. Use gcc_x86_64 as... · f223a74e
  Julien Signoles authored 9 years ago
  
  [tests] Compare the generated code just after running Value. Use gcc_x86_64 as machdep for all these tests. [tests] call testrun.sh in test_config in order to compile and run the generated code. This code is no more the one being compared with the oracle (see above item).
  f223a74e
May 28, 2015
- [tests] fix tests broken when directory 'tests/bts' has been introduced · fbe8d368
  Julien Signoles authored 10 years ago
  
  fbe8d368
Mar 06, 2015
- [tests] fix tests broken when directory 'tests/bts' has been introduced · 1b054cc9
  Julien Signoles authored 10 years ago
  
  1b054cc9
Nov 23, 2012
- [E-ACSL] use RTE to prevent arithmetic runtime errors in the generated code for non GMP expressions · 7c8a2a8b
  Julien Signoles authored 12 years ago
  
  7c8a2a8b
Oct 25, 2012
- [e-acsl] merging the e-acsl-mmodel branch into the main branch · 2821b923
  Julien Signoles authored 12 years ago
  
  2821b923
Apr 12, 2012
- [E-ACSL] tests ok again thanks to -e-acsl-share · 233eb82a
  Julien Signoles authored 12 years ago
  
  233eb82a
Jan 23, 2012
- [e-acsl] new option -e-acsl-gmp-only: used in tests to check the GMP translation · 478d31d3
  Julien Signoles authored 13 years ago
  
  478d31d3
Jan 19, 2012
- [e-acsl] the type system is now working: no more GMP in practice :-D · 76c70a33
  Julien Signoles authored 13 years ago
  
  76c70a33
Nov 25, 2011
- [e-acsl] new option -e-acsl to run the plug-in · f18cfe09
  Julien Signoles authored 13 years ago
  
  f18cfe09
- [e-acsl] remove option -e-acsl-include-headers · d8fea386
  Julien Signoles authored 13 years ago
  
  [e-acsl] tests now independent of GMP version (but GMP still required)
  d8fea386
Nov 23, 2011
- [e-acsl] additional tests for modulo · 4b541ebd
  Julien Signoles authored 13 years ago
  
  4b541ebd
- [e-acsl] tests compatible with strange behavior of gcc 4.6 (linking order) · f6ac1ca9
  Julien Signoles authored 13 years ago
  
  [e-acsl] all tests are now executed with gcc [e-acsl] fix bug with integer division and modulo [e-acsl] untested support of most logic labels [e-acsl]
  f6ac1ca9
Jul 01, 2011
- [e-acsl] improve handling of integer division and modulo · 6cb99627
  Julien Signoles authored 13 years ago
  
  6cb99627
May 12, 2011

[e-acsl] fixed bug for ! (not) · 678a99c8

Julien Signoles authored 13 years ago

[e-acsl] fixed bug for negative modulos
[e-acsl] full reimplementation of environments (only one now, and it is persistent)
[e-acsl] support of lazy operators &&, || and ==>
[e-acsl] tests now execute the generated C code and check that no runtime assertion is raised

678a99c8

Apr 06, 2011
- in tests, use @frama-c@, not a direct call to frama-c · 8dbbd674
  Virgile Prevosto authored 13 years ago
  
  8dbbd674
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 11, 2011
- upgrading oracles according to bug fixed #744 · 23825e33
  Julien Signoles authored 14 years ago
  
  23825e33
Mar 10, 2011
- 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