Commits · eaa0741d9cb54cd0c309c48e205e15fec04b469f · pub / frama-c

Jan 06, 2022
- [tests] execution from result directories: oracle updates · f7d8e1c6
  Patrick Baudin authored 3 years ago
  
  f7d8e1c6
Feb 08, 2021
- [tests] add non-regression test for macro with % in cpp extra args · 9170a765
  Andre Maroneze authored 4 years ago
  
  also avoid accidental `*/` in FILTER command
  9170a765
- [Kernel] separate preprocessing command and extra args; fixes #@1003 · 51c067ea
  Andre Maroneze authored 4 years ago
  
  51c067ea
Sep 15, 2020
- [eacsl] Update tests · d3a6265c
  Basile Desloges authored 4 years ago
  
  d3a6265c
Mar 19, 2020
- [eacsl:codegen] Update all e-acsl tests · 570027f2
  Basile Desloges authored 5 years ago
  
  570027f2
Dec 17, 2019
- [e-acsl:archi] restore correct behavior of ghost parameters · 404c8c60
  Julien Signoles authored 5 years ago and Michele Alberti committed 5 years ago
  
  404c8c60
Dec 16, 2019
- [e-acsl:tests] update tests wrt kernel changes · 8573c6ad
  Julien Signoles authored 5 years ago
  
  8573c6ad
Sep 09, 2019
- [Tests] Adds tests related to the handling of ghost parameters · e4fc7636
  Allan Blanchard authored 5 years ago
  
  e4fc7636
Aug 30, 2019
- [tests] rename language_constructs to constructs · de13faaf
  Julien Signoles authored 5 years ago
  
  de13faaf
- [tests] config ci · 75d20451
  Julien Signoles authored 5 years ago
  
  75d20451
- [tests] improve test organization · 2a0e80ad
  Julien Signoles authored 5 years ago
  
  2a0e80ad
- [tests] rename gmp to arith and runtime to memory · c1e98626
  Julien Signoles authored 5 years ago
  
  c1e98626
Feb 20, 2018
- Test oracle updates · 73c33a2e
  Kostyantyn Vorobyov authored 7 years ago and Julien Signoles committed 7 years ago
  
  73c33a2e
Aug 02, 2017
- Test oracles update · f88e29ce
  Kostyantyn Vorobyov authored 7 years ago
  
  f88e29ce
Mar 09, 2017
- update oracles · e61e4cee
  Virgile Prevosto authored 8 years ago
  
  e61e4cee
Jan 25, 2017
- synchronize with frama-c/frama-c!1112 · 7dcc51f9
  Andre Maroneze authored 8 years ago
  
  7dcc51f9
Jul 19, 2016
- [Makefile] Renamed e-acsl-runtime and e-acsl-reject test directories to... · 19e1ce3f
  Kostyantyn Vorobyov authored 8 years ago
  
  [Makefile] Renamed e-acsl-runtime and e-acsl-reject test directories to runtime and reject respectively
  19e1ce3f
Mar 15, 2016
- [RTL] e_acsl_assert renamed to __e_acsl_assert · 4d741cfd
  Kostyantyn Vorobyov authored 9 years ago
  
  4d741cfd
Mar 11, 2016
- [RTL] e_acsl_assert renamed to __e_acsl_assert · 0ee2b795
  Kostyantyn Vorobyov authored 9 years ago and Julien Signoles committed 9 years ago
  
  0ee2b795
Feb 10, 2016
- [tests] remove 'COMMENT: no diff' lines from bts and e-acsl-runtime tests · 557a5af3
  Julien Signoles authored 9 years ago
  
  557a5af3
- [tests] only print the output coming from the input file (but no more the libc) · cf5b90ec
  Julien Signoles authored 9 years ago
  
  cf5b90ec
- [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] cherry-picked hack for fopen · 0bf19f5e
  Julien Signoles authored 9 years ago
  
  0bf19f5e
Apr 28, 2015
- hack for fixing issue with fopen · 5ceb9812
  Julien Signoles authored 9 years ago
  
  5ceb9812
Nov 12, 2014
- [tests] update according to libc changes · 7556ef08
  Julien Signoles authored 10 years ago
  
  7556ef08
Jul 20, 2014
- patch the fix of bug #1715 in a way that __memory_size is still usable (no more ghost) · a705f9e9
  Julien Signoles authored 10 years ago
  
  a705f9e9
- patch the fix of bug #1715 in a way that __memory_size is still usable (no more ghost) · 56a7f14e
  Julien Signoles authored 10 years ago
  
  56a7f14e
Jul 08, 2014
- fix bug when using Frama-C-specific names of the libc which prevent linking the generated code · bc153f5c
  Julien Signoles authored 10 years ago
  
  bc153f5c
- fix bug when using Frama-C-specific names of the libc which prevent linking the generated code · 361a4fa8
  Julien Signoles authored 10 years ago
  
  361a4fa8
Jun 30, 2014
- [tests] updated according to pretty printer changes · 3384b7f8
  Julien Signoles authored 10 years ago
  
  [quantif] updated according to AST changes: && is now left-associative
  3384b7f8
Mar 25, 2014
- [memory-model] fix bug #1715 occuring because __memory_size was not declared ghost · 6f31302c
  Julien Signoles authored 11 years ago
  
  6f31302c
- [memory-model] fix bug #1715 occuring because __memory_size was not declared ghost · e873c591
  Julien Signoles authored 11 years ago
  
  e873c591
Sep 25, 2013
- [E-ACSL] again compatible with the trunk and no more with Fluorine · aa5f7cf6
  Julien Signoles authored 11 years ago
  
  aa5f7cf6
Sep 23, 2013
- [E-ACSL] ready for v0_3 · 565aff54
  Julien Signoles authored 11 years ago
  
  565aff54
Sep 19, 2013
- [E-ACSL] __memory_size is not ghost · 249387ad
  Julien Signoles authored 11 years ago
  
  249387ad
Sep 10, 2013

[E-ACSL] update oracles according to Value changes · 8aa4fa00

Julien Signoles authored 11 years ago

[E-ACSL] improve ACSL contracts of its libraries
[E-ACSL] no more unknow locations in translation of quantifications

8aa4fa00

May 21, 2013
- [E-ACSL] fixed imprecise location on RTE generation + update oracles · e4360835
  Julien Signoles authored 11 years ago
  
  e4360835
May 17, 2013
- [E-ACSL] do not call __clean when not required + ongoing manual · 885730d0
  Julien Signoles authored 11 years ago
  
  885730d0
May 07, 2013
- [E-ACSL] fixed issue with extern ghost variable (definitively (?) fixed issue #1392 · 2490ce6d
  Julien Signoles authored 11 years ago
  
  2490ce6d
Apr 23, 2013

[E-ACSL] faster initialization of the dataflow analysis · a1a09d0a

Julien Signoles authored 11 years ago

[E-ACSL] fixed bug with global declarations involved in the memory model (btw fixed but #1392)
[E-ACSL] additional feedback messages

a1a09d0a