From 6a76346972276dd1d2e622f5cb7182a857cd2f39 Mon Sep 17 00:00:00 2001
From: Titouan BOUETE-GIRAUD <titouan.bouete-giraud@artal.fr>
Date: Mon, 6 Nov 2023 11:41:48 +0100
Subject: [PATCH] Squashed commit of the following:
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
commit be323fb01e151bfb6b0bb6a8500de712a5b55dd5
Merge: bb446348ba 931dd76edb
Author: Loïc Correnson <loic.correnson@cea.fr>
Date: Mon Nov 6 10:29:29 2023 +0000
Merge branch 'feature/tests/framework' into 'master'
E2E and Monkey Tests Framework
See merge request frama-c/frama-c!4274
commit 931dd76edb8ca49a28542d6a443dd8f4a7e46cc9
Author: Damien IRIBERRY <damien.iriberry@artal.fr>
Date: Mon Nov 6 10:29:28 2023 +0000
E2E and Monkey Tests Framework
commit bb446348baaf3ed8b0a07a8216eae4f08bd2d606
Merge: d14e46bf1a edaa7275e0
Author: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon Nov 6 11:13:12 2023 +0100
Merge branch 'stable/nickel'
commit edaa7275e0846b56930a82904b7b1f14d5e153dc
Merge: 3bf6baa2e6 89c591e14c
Author: Virgile Prevosto <virgile.prevosto@cea.fr>
Date: Mon Nov 6 10:06:17 2023 +0000
Merge branch 'rma-master-patch-17294' into 'stable/nickel'
Update acknowledgement for Roma Maliach-Auguste
See merge request frama-c/frama-c!4392
commit 89c591e14c142a2522757ce69d333c85a4f4cfed
Author: Roma Maliach-Auguste <romain.maliach-auguste@cea.fr>
Date: Fri Nov 3 19:39:10 2023 +0000
Update acknowledgement for Roma Maliach-Auguste
commit d14e46bf1a4a53d8f3500eaec5992430ea4cd973
Merge: 81563c24f6 eee031c721
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon Nov 6 07:19:00 2023 +0000
Merge branch 'feature/martin/tests/replace-dir-coverage-script-with-option' into 'master'
Remove compute dir coverage script and use --tree for bisect html report instead
See merge request frama-c/frama-c!4391
commit eee031c721af6a66c8ac8008a46a6bc3db2b37a1
Author: Thibault Martin <thi.martin.pro@pm.me>
Date: Tue Oct 31 16:33:38 2023 +0100
Remove script and use --tree for bisect html report
commit 81563c24f652c9eb575708acb842e19b2a79846d
Merge: 4f6897b4fe 0eaacb252a
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon Oct 30 13:37:19 2023 +0000
Merge branch 'bugfix/julien/userman-foreword' into 'master'
[e-acsl] fix userman's foreword
See merge request frama-c/frama-c!4385
commit 4f6897b4fedf108999847944b65b081c418e143b
Merge: 7ced1ed8ef 141d24d4d1
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon Oct 30 12:11:11 2023 +0000
Merge branch 'feature/blanchard/ci/simpl-constrains' into 'master'
[ci] reorganizes schedules and release pipelines
See merge request frama-c/frama-c!4390
commit 141d24d4d115bb6aaa4a34440e0521973e79a691
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri Jun 16 17:13:31 2023 +0200
[ci] reorganizes schedules and release pipelines
commit 7ced1ed8efb715b2837b2c5af22320dc9bde5cbc
Merge: 25fb48d36a d26fe9df27
Author: Thibault Martin <thi.martin.pro@pm.me>
Date: Fri Oct 27 13:22:22 2023 +0000
Merge branch 'feature/eva/simplify-widen-hints' into 'master'
[Eva] Changes the signature of the widening in most cvalue modules
See merge request frama-c/frama-c!4384
commit 25fb48d36afb2b55b45d931eb1ac199d77c9183a
Merge: 9ac7e685f8 4b3f48e5b7
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri Oct 27 11:49:16 2023 +0000
Merge branch 'feature/dev/make-distrib-help' into 'master'
[dev]Â make-distrib options
See merge request frama-c/frama-c!4373
commit 3bf6baa2e60a0ff3a69d50bdb5fcf7182328be04
Author: David Bühler <david.buhler@cea.fr>
Date: Fri Oct 27 13:34:56 2023 +0200
Updates Changelog for MR !4259.
commit d26fe9df2770e60549f68755af1e5b943c923595
Author: David Bühler <david.buhler@cea.fr>
Date: Thu Oct 26 10:19:41 2023 +0200
[Eva] Offsetmap and lmap: [widen] takes hints as optional named arguments.
commit d3a404d14ec181300e0dab82329c75e975b5754e
Author: David Bühler <david.buhler@cea.fr>
Date: Wed Oct 25 19:30:04 2023 +0200
[Eva] Fval: uses sets of float as widen_hint instead of logic_real.
Removes module Fc_float.Widen_hint, and uses Datatype.Float.Set instead.
commit 793cb8a9fa3cfae3b779ebd0819d4efcf70255d0
Author: David Bühler <david.buhler@cea.fr>
Date: Wed Oct 25 17:58:29 2023 +0200
[Eva] Computes widening thresholds according to bases validity in Locations.
commit b0b5ce920ad6af23f19d1464ab1691cba289a210
Author: David Bühler <david.buhler@cea.fr>
Date: Wed Oct 25 16:08:49 2023 +0200
[Eva] Changes the signature of the widening in most cvalue modules.
- In int_interval, int_val, ival, locations and cvalue: [widen] now takes
optional named arguments [size] and [hint].
- Updates Offsetmap functor accordingly.
- Removes types [numerical_widen_hint] and [size_widen_hint]:
modules only declare one [widen_hint] type.
- Removes module Ival.Widen_hints, and uses Integer.Set directly instead.
commit 57de6adf1ccbadb47b323c40f44b706ea122cb80
Author: David Bühler <david.buhler@cea.fr>
Date: Wed Oct 25 16:14:12 2023 +0200
[Eva] Uses Integer.Set instead of Ival.Widen_Hints in widen files.
commit 16a111a5b8f4c5a6e7cf3d91dc7a3a53fbe1dae1
Author: David Bühler <david.buhler@cea.fr>
Date: Wed Oct 25 16:00:55 2023 +0200
[Eva] Removes widening from lattice types.
commit 9ac7e685f8dcb99f65e60fccedd4c4b7dc31cb6a
Merge: ce374b15a1 c12f874e17
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu Oct 26 19:31:52 2023 +0000
Merge branch 'merge-stable-nickel' into 'master'
merge stable/nickel into master and update VERSION
See merge request frama-c/frama-c!4382
commit c12f874e177783c0907e8f89d921cc91137ed015
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu Oct 26 20:56:58 2023 +0200
update version for dev branch
commit 009f960253738602d6b4269a2ad660311563d44b
Merge: ce374b15a1 22713a7cc3
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu Oct 26 20:54:59 2023 +0200
Merge stable/nickel into master
commit 22713a7cc3b97ed4fcb4ae991c4eec7f7aa793a7
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu Oct 26 16:02:33 2023 +0200
[release] add main changes for 28.0
commit 0eaacb252a28a1e3519cf63c213771450235111d
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu Oct 26 15:49:23 2023 +0200
[e-acsl/doc] on clean, remove eacslversion
commit ce374b15a178aa303c627b93749c0d01c79d45c0
Merge: 101a5fb8fd d21266076c
Author: Thibault Martin <thi.martin.pro@pm.me>
Date: Thu Oct 26 13:27:13 2023 +0000
Merge branch 'feature/blanchard/ci/manuals' into 'master'
[ci] improved manuals target
Closes #1323
See merge request frama-c/frama-c!4383
commit 758ba4a514c7ab75f7010e1a70c6508e62b60cd3
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu Oct 26 15:21:40 2023 +0200
[e-acsl/doc] fix Frama-C version
commit 021b2939252759be16ca4ac511f2416ee4628cd5
Author: Julien Signoles <julien.signoles@cea.fr>
Date: Thu Oct 26 15:02:16 2023 +0200
[e-acsl] fix userman's foreword
commit 078bff527d02793483219cff20335cd9dc04ae6d
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu Oct 26 15:21:40 2023 +0200
[e-acsl/doc] fix Frama-C version
commit 2e4481077931ce9de005720d34cd6cf914d6058d
Author: Julien Signoles <julien.signoles@cea.fr>
Date: Thu Oct 26 15:02:16 2023 +0200
[e-acsl] fix userman's foreword
commit 858647e8333a5fc38a2d13b3f0a24ee11625a671
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu Oct 26 14:56:33 2023 +0200
[doc] fix typos in a few manuals
commit 9ad4f6851a6897c2f1efe302b0c6565f11754a74
Merge: 1beda363b3 9d9faf75a4
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu Oct 26 07:39:55 2023 +0000
Merge branch 'prepare-release-update-version' into 'stable/nickel'
Prepare release update version
See merge request frama-c/frama-c!4381
commit d21266076cd113a5368a755abb3cfbc351ac1e8b
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu Oct 26 09:34:42 2023 +0200
[ci] improved manuals target
- executed nightly (allowed to fail)
- excuted on changes
commit 9d9faf75a43d24f7d845b403d77c09d4306b7325
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu Oct 26 09:06:25 2023 +0200
[dev] fix usage of 'dev' after a beta release
commit 3e889241d19623fc86b346508ae5b5568b0076b3
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed Oct 25 22:51:09 2023 +0200
update copyright year in forgotten files
commit 0aaf54b16a6af0d64614975b81d466690ef00382
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed Oct 25 22:43:18 2023 +0200
update version for 28.0~beta
commit 1e4612c5d73f09d568255861a1537d612fb9e17c
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed Oct 25 16:11:17 2023 +0200
[dev] extend set-version.sh and update release manual
commit 101a5fb8fd8182f3e46242592bb3fc0912acf8a6
Merge: 7129e55b04 7afe0cc228
Author: Thibault Martin <thi.martin.pro@pm.me>
Date: Wed Oct 25 15:44:19 2023 +0000
Merge branch 'feature/eva/clean-abstract-interp' into 'master'
[Eva] Removes unused code from Abstract_interp
See merge request frama-c/frama-c!4379
commit 7afe0cc2285e0d626c6caabd2b0065e1bcbd454f
Author: David Bühler <david.buhler@cea.fr>
Date: Wed Oct 25 15:08:16 2023 +0200
[Eva] Removes unused module [Bool] from Abstract_interp.
commit 8467dbcbe0404310beaa75df1ff3b24828851d6c
Author: David Bühler <david.buhler@cea.fr>
Date: Wed Oct 25 14:19:01 2023 +0200
[Eva] Removes unused functors from abstract_interp.
commit 1305bbfbaf6b6e5ccfc41ad1bffe3d842d823fd1
Author: David Bühler <david.buhler@cea.fr>
Date: Wed Oct 25 14:53:42 2023 +0200
[Eva] Garbled mix origin: removes use of Abstract_interp.Make_Lattice_Base.
Defines datatype and lattice of LocationLattice in origin.ml.
commit 21641125beaec3405cd02fac05060ac5680f6f42
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed Oct 25 16:00:28 2023 +0200
[doc] avoid references to specific Frama-C versions
commit 1beda363b3d329f60e7ea5daf9eb70a1811ed301
Merge: b0770ad3eb 4bf59c78bf
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed Oct 25 13:18:01 2023 +0000
Merge branch 'fix/blanchard/dev/set-version-update' into 'stable/nickel'
[dev] extend set-version.sh for build script
See merge request frama-c/frama-c!4366
commit 7129e55b04003f5ee7a9c745af6120240a0c8f66
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed Oct 25 08:31:25 2023 +0000
Reset default branch
commit b0770ad3eb4fb8a4913a4041a70b9049dc93b977
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed Oct 25 08:31:25 2023 +0000
Change default branch
commit 5049d6b9a1ac348af1cc217fb24eb7de32454c17
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed Oct 25 08:27:09 2023 +0000
Reset default branch
commit 91cba9d8fe1e3e8dcd5b36595a440e724dd72044
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed Oct 25 08:27:08 2023 +0000
Change default branch
commit 66662ebd48da99706976611154062d9671b68900
Merge: 2670b18154 ce91403b51
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed Oct 25 06:55:19 2023 +0000
Merge branch 'fix/wp/strategies' into 'master'
[wp] fix non-terminating strategies
See merge request frama-c/frama-c!4376
commit 2670b1815404fd38b5b764f761dcb039df819a0f
Merge: 2fe33b18e3 3ec37752fd
Author: Loïc Correnson <loic.correnson@cea.fr>
Date: Tue Oct 24 19:05:03 2023 +0000
Merge branch 'jan/fix/issue2666' into 'master'
[alias] correctly expose Abstract_state including graph
See merge request frama-c/frama-c!4375
commit 3ec37752fd089b1aff76fb2146fce46047e1a1d4
Author: Loïc Correnson <loic.correnson@cea.fr>
Date: Tue Oct 24 20:31:06 2023 +0200
[alias] expose vertex id as int
commit ce91403b51ada88fa006f4239595518f03cd0e01
Author: Loïc Correnson <loic.correnson@cea.fr>
Date: Mon Oct 23 17:53:17 2023 +0200
[wp] test for logical patterns
commit 0b07515d57cad6ed62df00aa9ddc5d80a2e1bf4e
Author: Loïc Correnson <loic.correnson@cea.fr>
Date: Mon Oct 23 17:42:08 2023 +0200
[wp] logical patterns
commit 2fe33b18e314ec8a7e1dc46b6882ebe1c09aa8d4
Merge: a1c78b461e a4fc83c563
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon Oct 23 15:06:25 2023 +0000
Merge branch 'fix/macOS-args' into 'master'
[ivette] Fix/mac os args
See merge request frama-c/frama-c!4368
commit 078669faf7a0f14c2dadedbde3db83070802a75d
Author: Loïc Correnson <loic.correnson@cea.fr>
Date: Mon Oct 23 16:55:21 2023 +0200
[wp] split conjunctions only when looking in hyps
commit 75d3f50522a5ca6569a247daf4371ec5846ee9e1
Author: Jan Rochel <jan.rochel@cea.fr>
Date: Mon Oct 23 16:08:39 2023 +0200
[alias] correctly expose Abstract_state including graph
commit 1a11dfa87ef83be842ccdef663d6a2afa6cd4623
Author: Loïc Correnson <loic.correnson@cea.fr>
Date: Mon Oct 23 16:17:24 2023 +0200
[wp] test for fixed non-terminating strategy
commit 679edcaf0ac8c6246278c96e29af89d97235f3d2
Author: Loïc Correnson <loic.correnson@cea.fr>
Date: Mon Oct 23 16:08:58 2023 +0200
[wp] progressing check after tactic
commit 49439a79c719c867bb19c6358b60c7fcbbc0e39b
Author: Loïc Correnson <loic.correnson@cea.fr>
Date: Mon Oct 23 15:43:47 2023 +0200
[wp] limit depth of exploration with strategies
commit 4b3f48e5b786e43348bb72ea7f0b09fe12351420
Author: Loïc Correnson <loic.correnson@cea.fr>
Date: Mon Oct 23 14:39:02 2023 +0200
[dev] remove --version
commit 293ae307de3b994578f1529fc3f582ee9f3dfdb1
Author: Loïc Correnson <loic.correnson@cea.fr>
Date: Mon Oct 23 12:21:21 2023 +0200
[dev]Â make-distrib options
commit a1c78b461ef408a0112d5ba3d8dbf32a68e30671
Merge: 624a66671a 095954d9e5
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu Oct 19 14:33:41 2023 +0000
Merge branch 'feature/blanchard/wp/default-spec' into 'master'
WP populate spec
Closes #1303
See merge request frama-c/frama-c!4362
commit 624a66671a05eb58f788184306fc2cf6e605fd1c
Merge: 7dd5bd7637 a4c723c67f
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu Oct 19 14:07:53 2023 +0000
Merge branch 'feature/martin/doc/1310-document-properly-the-behavior-of-the-default-spec-generator' into 'master'
Resolve "Document properly the behavior of the default spec generator"
Closes #1310
See merge request frama-c/frama-c!4339
commit 095954d9e53df56f034a5afcf3b0afee7c438821
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu Oct 19 15:58:45 2023 +0200
[wp] ChangeLog
commit 29c8f3259de498ba1d548b0ddde33c8e4300b531
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu Oct 19 15:20:05 2023 +0200
[wp] fix test after rebase
commit a4c723c67f6be4dc9d954f65eecdeb541092a16e
Author: Thibault Martin <thi.martin.pro@pm.me>
Date: Thu Oct 19 15:11:05 2023 +0200
[doc] Add details about warnings + minors changes
commit 7b749a3faa4992bb1bb44e9907438627ed0ac5d8
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu Oct 19 14:05:33 2023 +0200
[wp/doc] Add generated and verified clauses to the manual
commit 3d892e48d2d3efb21b995d046851521b76a9bdbe
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu Oct 19 11:27:37 2023 +0200
[wp] warn on missing default assigns
commit 118721aded1076d10380315a780865ccc5f9bcd0
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu Oct 19 10:32:31 2023 +0200
[wp] changes strategy for callees assigns
commit 205cc850ede6bd0fa02dac17f23b3db562cc203c
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed Oct 18 10:39:45 2023 +0200
[wp] lint
commit bf3fcc8e0c35dff7c0391b7142e2b47e5c4b3baa
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri Oct 13 16:58:25 2023 +0200
[wp] update oracles
commit 14293eabeb7f3d37a5cdfe171ee30d6e72040a44
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri Oct 13 16:58:11 2023 +0200
[wp] add spec populate for API calls
commit 15d6aa284d49f0e030bec6da9d8c3cf2ba3e51df
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu Oct 12 14:27:42 2023 +0200
[wp] temporarily disabled stmtcompiler test
commit fcd4fe75e5bbd1919c9fbb633a09cb6f1af488a6
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu Oct 12 14:27:20 2023 +0200
[wp] update test
commit c75a5946c59feaffe88b87a4ac04ac407e7ce2e7
Author: Loïc Correnson <loic.correnson@cea.fr>
Date: Thu Oct 12 10:51:57 2023 +0200
[wp] reformat cfg status
commit 5cfa60c8c53a8bf8d7ae2170ce6a821f06575db2
Author: Loïc Correnson <loic.correnson@cea.fr>
Date: Thu Oct 12 10:37:52 2023 +0200
[wp] update test
commit c1701cedca3ff3c1e194ccfb856f19ba4cf94964
Author: Loïc Correnson <loic.correnson@cea.fr>
Date: Thu Oct 12 10:25:51 2023 +0200
[wp] update test
commit 0552c3c221285c8c56ec3ad59139e4f0182f2325
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed Oct 11 14:32:55 2023 +0200
[wp] remove options related to terminates generation
commit d1abe35ddd1afeaea4fd67103c1b603d3c673b37
Author: Thibault Martin <thi.martin.pro@pm.me>
Date: Tue Aug 8 16:35:13 2023 +0200
Update WP oracles
commit 05358a06af2e08dea32d90b635d6d5acb2adc988
Author: Thibault Martin <thi.martin.pro@pm.me>
Date: Tue Aug 8 15:30:00 2023 +0200
Update aorai oracles
commit 85b4cf27d9cc403a3f4d3fd393b5e17c789d2f14
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu Sep 28 14:37:49 2023 +0200
[wp] use kernel default spec populate
- deprecate parameters related to populate
- do not populate when finding missing terminates
commit 770ec85b4830ba0c7c1c662756807e962a182cff
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed Oct 11 13:51:36 2023 +0200
[wp] fix WP target for main function
commit 9055efa3619b92d998340e5571c7d50a451a8c58
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu Oct 19 14:43:36 2023 +0200
[doc] typos
commit f156a6c5c0913f4c6ecb3bfcc631304dd4b6f767
Author: Thibault Martin <thi.martin.pro@pm.me>
Date: Tue Oct 17 10:01:10 2023 +0200
[doc] Details about combining clauses from behaviors
commit 550dd45842ed345da0b77022a1e84f1bd5e46b3e
Author: Thibault Martin <thi.martin.pro@pm.me>
Date: Mon Oct 9 15:02:34 2023 +0200
[doc] Describe populate_spec modes in userman
commit eef7f40c71a62c9a0aae7006e733530ccce743f3
Author: Thibault Martin <thi.martin.pro@pm.me>
Date: Mon Oct 9 14:56:50 2023 +0200
[doc] Add tables in devman for custom mode example
commit 7f46efab2c6443b277ea50300eec72e96e048de0
Author: Thibault Martin <thi.martin.pro@pm.me>
Date: Mon Oct 9 14:52:06 2023 +0200
[doc] Fix mode description in populate_spec
commit 96b4427e0d2e4d26bb1465376ec374c79e2ff071
Author: Thibault Martin <thi.martin.pro@pm.me>
Date: Mon Oct 9 10:09:51 2023 +0200
[doc] devman: rewrite / fix typo
commit 827ea463fd6b2f88a6349e74e984108e4b75185c
Author: Thibault Martin <thi.martin.pro@pm.me>
Date: Wed Oct 4 14:27:00 2023 +0200
[doc] populate_funspec now can take an optionnal location
commit 89b2eba7327644f43d95105266ce077073f116af
Author: Thibault Martin <thi.martin.pro@pm.me>
Date: Tue Oct 3 16:57:19 2023 +0200
[doc] Fix some typos, indent code
commit e32b56f357384741298b7b0eecad40c29e1dade7
Author: Thibault Martin <thi.martin.pro@pm.me>
Date: Tue Oct 3 16:12:05 2023 +0200
[tests] Fix and update Populate_spec example
commit f9ca7016b5c7a17d7465fe3c0935d301a90c91bd
Author: Thibault Martin <thi.martin.pro@pm.me>
Date: Tue Oct 3 11:45:30 2023 +0200
[doc] Populate_spec explanation for plug-in developpers
commit 7dd5bd76373fc6c1196e3f693d57b54496e26c2b
Merge: 517cc90bce 5b924beaa6
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu Oct 19 12:20:43 2023 +0000
Merge branch 'fix/martin/kernel/do-not-add-empty-default-behavior' into 'master'
Add the newly created behavior only if it is not empty
See merge request frama-c/frama-c!4370
commit 5b924beaa67ab56cc93a8e8b1ac1e0f45c3ceca2
Author: Thibault Martin <thi.martin.pro@pm.me>
Date: Wed Oct 18 10:18:26 2023 +0200
Update test oracles
commit bbec67abc9285b2b4ab3c0e3327bf9d12a7ee858
Author: Thibault Martin <thi.martin.pro@pm.me>
Date: Tue Oct 17 14:17:32 2023 +0200
Add the new behavior only if it is not empty
commit a4fc83c56394aea99354a9d57adf9cbdb142d389
Author: Loïc Correnson <loic.correnson@cea.fr>
Date: Mon Oct 16 15:36:14 2023 +0200
[ivette] fix macOS script
commit 4bf59c78bf4f52bf38d8a40729bf185e2de4b7fd
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon Oct 16 10:26:41 2023 +0200
[doc] release manual
- update what the set-version script does
commit 477d5b5e4b45811ee97eb5f9c6b115acf66b16cf
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon Oct 16 10:24:20 2023 +0200
[dev] extend set-version.sh
- also update Frama-C build script
---
Changelog | 1 +
bin/test.sh | 2 +-
dev/compute_dir_coverage.py | 214 ------------------------------------
doc/developer/developer.tex | 2 +-
4 files changed, 3 insertions(+), 216 deletions(-)
delete mode 100755 dev/compute_dir_coverage.py
diff --git a/Changelog b/Changelog
index 78726f151f9..de9f173fc0c 100644
--- a/Changelog
+++ b/Changelog
@@ -22,6 +22,7 @@ Open Source Release <next-release>
Open Source Release 28.0 (Nickel)
###############################################################################
+- Eva [2023-10-11] Optimization of the multidim domain.
-! Kernel [2023-10-09] Remove options -no-type and -no-obj and related
functions.
o! Kernel [2023-10-03] New mechanism for generating default specifications
diff --git a/bin/test.sh b/bin/test.sh
index 3e78b725d5f..adfc3e9ea90 100755
--- a/bin/test.sh
+++ b/bin/test.sh
@@ -312,7 +312,7 @@ function GenerateCoverage
Head "Generating coverage in _coverage ..."
if [ "$HTML" = "yes" ] ;
then
- Cmd bisect-ppx-report html --coverage-path=_bisect
+ Cmd bisect-ppx-report html --coverage-path=_bisect --tree
fi
if [ "$XML" = "yes" ] ;
then
diff --git a/dev/compute_dir_coverage.py b/dev/compute_dir_coverage.py
deleted file mode 100755
index 757e9d21423..00000000000
--- a/dev/compute_dir_coverage.py
+++ /dev/null
@@ -1,214 +0,0 @@
-##########################################################################
-# #
-# This file is part of Frama-C. #
-# #
-# Copyright (C) 2007-2023 #
-# CEA (Commissariat à l'énergie atomique et aux énergies #
-# alternatives) #
-# #
-# you can redistribute it and/or modify it under the terms of the GNU #
-# Lesser General Public License as published by the Free Software #
-# Foundation, version 2.1. #
-# #
-# It is distributed in the hope that it will be useful, #
-# but WITHOUT ANY WARRANTY; without even the implied warranty of #
-# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
-# GNU Lesser General Public License for more details. #
-# #
-# See the GNU Lesser General Public License version 2.1 #
-# for more details (enclosed in the file licenses/LGPLv2.1). #
-# #
-##########################################################################
-
-# usage: compute_dir_coverage.py [-h] [-f] [-r] [-b] filepath
-#
-# positional arguments:
-# filepath path to frama-c/_coverage/index.html file
-#
-# options:
-# -h, --help show this help message and exit
-# -f, --files display files coverage
-# -r, --ratio display ratio (covered lines / total lines)
-# -b, --bar display % bars
-
-import re, sys, os.path
-from bs4 import BeautifulSoup
-import argparse
-
-FILE_MARKER = "<files>"
-DISPLAY_FILES = False
-DISPLAY_RATIO = False
-DISPLAY_BAR = False
-root = {FILE_MARKER: []}
-coverage = {}
-
-
-# Generate command line arguments and format
-def options():
- argparser = argparse.ArgumentParser()
- argparser.add_argument("filepath", help="path to frama-c/_coverage/index.html file")
- argparser.add_argument("-f", "--files", action="store_true", help="display files coverage")
- argparser.add_argument(
- "-r", "--ratio", action="store_true", help="display ratio (covered lines / total lines)"
- )
- argparser.add_argument("-b", "--bar", action="store_true", help="display %% bars")
- args = argparser.parse_args()
- return args
-
-
-# Open the html file and create the structure to navigate inside
-def parse(filename):
- if not os.path.exists(filename):
- print("No such file or directory: " + filename)
- exit()
- with open(filename) as fp:
- return BeautifulSoup(fp, "html.parser")
-
-
-# From our html structure, extract files informations
-# Return a list of nuples (file_path, covered_lines, total_lines)
-def extract(html_parser):
- # This div contains all files data
- all_files = html_parser.find(id="files")
-
- file_list = list()
- for file in all_files.find_all("div"):
- # Access to covered/total lines data
- data = file.contents[3].contents[1].text.split("/", 1)
- covered_lines = int(re.sub(r"[^\d]+", "", data[0]))
- total_lines = int(re.sub(r"[^\d]+", "", data[1]))
- # Access to file path
- path_to_file = file.contents[5].text.strip()
- file_list.append((path_to_file, covered_lines, total_lines))
- return file_list
-
-
-# Build file directory tree
-# Each folder is a dictionnary containing a list of files marked with FILE_MARKER
-# Other entries are folder
-# We store each files with it's coverage data
-def build_tree(path, covered_lines, total_lines, current_dir):
- parts = path.split("/", 1) # Perform only 1 split
- if len(parts) == 1: # path contains only a filename
- current_dir[FILE_MARKER].append((parts[0], covered_lines, total_lines))
- else:
- directory, remaining_path = parts
- if directory not in current_dir:
- current_dir[directory] = {FILE_MARKER: []}
- build_tree(remaining_path, covered_lines, total_lines, current_dir[directory])
-
-
-def concat_path(path, file):
- if path == "":
- return file
- else:
- return path + "/" + file
-
-
-def dir_coverage(d, path=""):
- acc_coverage, acc_total = 0, 0
- for key, value in d.items():
- if key == FILE_MARKER: # Files
- # Add files stats to current dir
- for file, covered_lines, total_lines in value:
- acc_coverage = acc_coverage + covered_lines
- acc_total = acc_total + total_lines
- else: # Directory
- currpath = concat_path(path, key)
- # Compute subdir stats
- covered_lines, total_lines = dir_coverage(value, currpath)
- coverage[currpath] = covered_lines, total_lines
- # Add subdir stats to current dir
- acc_coverage = acc_coverage + covered_lines
- acc_total = acc_total + total_lines
- return acc_coverage, acc_total
-
-
-def percentage(covered_lines, total_lines):
- if total_lines != 0:
- return covered_lines / total_lines * 100
- else:
- return 0.0
-
-
-###################
-# Print functions #
-###################
-
-
-def str_per(per):
- return "{:>6.2f}".format(per)
-
-
-def str_bar(per):
- if DISPLAY_BAR:
- nb = round(per / 5)
- return "|" + nb * "#" + (20 - nb) * "-" + "| "
- else:
- return ""
-
-
-def str_ratio(covered_lines, total_lines):
- if DISPLAY_RATIO:
- return " : (" + str(covered_lines) + " / " + str(total_lines) + ")"
- else:
- return ""
-
-
-def print_line(name, covered_lines, total_lines, indent):
- per = percentage(covered_lines, total_lines)
-
- bar = str_bar(per)
- p = str_per(per)
- ratio = str_ratio(covered_lines, total_lines)
-
- if indent != "":
- indent = indent + " "
-
- print(bar + p + "% " + indent + name + ratio)
-
-
-def print_files(files, indent):
- for file, covered_lines, total_lines in files:
- print_line(file, covered_lines, total_lines, "---" + indent)
-
-
-def print_dir(directory, children, path, indent):
- currpath = concat_path(path, directory)
- covered_lines, total_lines = coverage[currpath]
- print_line(directory, covered_lines, total_lines, indent)
- print_tree(children, "---" + indent, currpath)
-
-
-# !!! dir_coverage must be called before !!!
-def print_tree(d, indent="", path=""):
- for key, value in d.items():
- if key != FILE_MARKER: # Direcory
- print_dir(key, value, path, indent)
- elif DISPLAY_FILES: # Files
- print_files(value, indent)
-
-
-def main():
- args = options()
-
- # Set options booleans
- global DISPLAY_FILES
- DISPLAY_FILES = args.files
- global DISPLAY_RATIO
- DISPLAY_RATIO = args.ratio
- global DISPLAY_BAR
- DISPLAY_BAR = args.bar
-
- html_parser = parse(args.filepath)
- files = extract(html_parser)
-
- for path_to_file, cov, tot in files:
- build_tree(path_to_file, cov, tot, root)
-
- dir_coverage(root)
- print_tree(root)
-
-
-if __name__ == "__main__":
- main()
diff --git a/doc/developer/developer.tex b/doc/developer/developer.tex
index a9dfcd8ab63..bed8b185e18 100644
--- a/doc/developer/developer.tex
+++ b/doc/developer/developer.tex
@@ -53,7 +53,7 @@ and Virgile~Prevosto}
\acknowledge{Boris Hollas}
\acknowledge{Nikolaï Kosmatov}
\acknowledge{Jean-Christophe Léchenet}
-\acknowledge{Romain Maliach-Auguste}
+\acknowledge{Roma Maliach-Auguste}
\acknowledge{André Maroneze}
\acknowledge{Benjamin Monate}
\acknowledge{Yannick Moy}
--
GitLab