pub issueshttps://git.frama-c.com/groups/pub/-/issues2024-03-28T17:22:41Zhttps://git.frama-c.com/pub/cabrnet/-/issues/38Fix ProtoPNet pruning2024-03-28T17:22:41ZRomain Xu-DarmeFix ProtoPNet pruningProtoPNet pruning should be followed by a fine-tuning step on the last (linear) layer. In the current code version, the drop in accuracy after pruning is almost 8% on CUB200.ProtoPNet pruning should be followed by a fine-tuning step on the last (linear) layer. In the current code version, the drop in accuracy after pruning is almost 8% on CUB200.Aymeric VarasseAymeric Varassehttps://git.frama-c.com/pub/colibrics/-/issues/15Follow-up from "Add tracing information"2024-03-26T09:28:28ZFrançois BobotFollow-up from "Add tracing information"The following discussion from !54 should be addressed:
- [ ] @bobot started a [discussion](https://git.frama-c.com/pub/colibrics/-/merge_requests/54#note_229014): (+1 comment)
> Do we have a test case that shows the need for that?The following discussion from !54 should be addressed:
- [ ] @bobot started a [discussion](https://git.frama-c.com/pub/colibrics/-/merge_requests/54#note_229014): (+1 comment)
> Do we have a test case that shows the need for that?https://git.frama-c.com/pub/cabrnet/-/issues/37Inconsistent docstring capitalization and use of third person2024-03-14T10:08:40ZAymeric VarasseInconsistent docstring capitalization and use of third personAlban GrastienAlban Grastienhttps://git.frama-c.com/pub/frama-c/-/issues/2692[alias] expose more functions2024-03-14T10:51:28ZJan Rochel[alias] expose more functionsCopied from https://git.frama-c.com/pub/frama-c/-/issues/2677#note_229339 by @bclement-ocp
Some additional functions need to be exposed in the `Abstract_state` for programmatic use if access to the underlying graph is needed (I need to ...Copied from https://git.frama-c.com/pub/frama-c/-/issues/2677#note_229339 by @bclement-ocp
Some additional functions need to be exposed in the `Abstract_state` for programmatic use if access to the underlying graph is needed (I need to iterate over all equivalence classes, and I think only raw access to the graph allows this).
More precisely:
* `get_lval` / `find_aliases` now only returns variable aliases; there is `reconstruct_lvals` internally to compute all the aliases but it is not exposed (it is used by find_all_aliases, but that also brings aliases from other equivalence classes);
* edge labels are not exposed, so it is not possible to distinguish between pointer and field edges from outside the plugin, making raw access to the graph impossible to do correctly
Would it be possible to expose `EdgeLabel `and (an equivalent of) `reconstruct_lvals` from the plugin's API?Jan RochelJan Rochelhttps://git.frama-c.com/pub/cabrnet/-/issues/36Save projection database2024-03-08T10:56:39ZRomain Xu-DarmeSave projection databaseRomain Xu-DarmeRomain Xu-Darmehttps://git.frama-c.com/pub/cabrnet/-/issues/35Implement perturbation-based benchmark to understand the nature of the visual...2024-03-07T10:57:30ZRomain Xu-DarmeImplement perturbation-based benchmark to understand the nature of the visual similaritySee the work of [https://arxiv.org/abs/2011.02863](https://arxiv.org/abs/2011.02863)See the work of [https://arxiv.org/abs/2011.02863](https://arxiv.org/abs/2011.02863)Romain Xu-DarmeRomain Xu-Darmehttps://git.frama-c.com/pub/cabrnet/-/issues/34Catch errors in the main while collecting the apps2024-03-05T08:15:52ZAlban GrastienCatch errors in the main while collecting the appsIf an app is buggy (e.g., its import list is incorrect), it is impossible to call another app. It'd be good to catch this kind of errors and maybe print a warning.If an app is buggy (e.g., its import list is incorrect), it is impossible to call another app. It'd be good to catch this kind of errors and maybe print a warning.Alban GrastienAlban Grastienhttps://git.frama-c.com/pub/cabrnet/-/issues/33Use Captum for Smoothgrads2024-03-07T10:20:44ZRomain Xu-DarmeUse Captum for SmoothgradsRomain Xu-DarmeRomain Xu-Darmehttps://git.frama-c.com/pub/cabrnet/-/issues/32Constants for common filenames2024-03-04T17:09:41ZAlban GrastienConstants for common filenamesTo retrieve the config file of a model in a folder `checkpoint`, we currently use the command
```model_config = os.path.join(checkpoint, "model_config.yml")```
It would be good to have a constant that records what the standard name for...To retrieve the config file of a model in a folder `checkpoint`, we currently use the command
```model_config = os.path.join(checkpoint, "model_config.yml")```
It would be good to have a constant that records what the standard name for this type of file is:
```model_config = os.path.join(checkpoint, CaBRNet.MODEL_CONFIG_FILENAME)```
(or similar). Also applies to `"model_state.pth"`, `"dataset.yml"`, `"training.yml"`, `"visualization.yml"`, and the `"final"` and `"best"` checkpoint folders.Romain Xu-DarmeRomain Xu-Darmehttps://git.frama-c.com/pub/cabrnet/-/issues/31Move visualisation directory to visualization2024-03-04T10:03:27ZRomain Xu-DarmeMove visualisation directory to visualizationhttps://git.frama-c.com/pub/cabrnet/-/issues/30Add support for file logging instead of std output2024-03-04T17:09:56ZRomain Xu-DarmeAdd support for file logging instead of std outputRomain Xu-DarmeRomain Xu-Darmehttps://git.frama-c.com/pub/cabrnet/-/issues/29Clean files under versioning in docs/2024-03-01T10:53:01ZRomain Xu-DarmeClean files under versioning in docs/Some files under versioning located in docs/ are generated by pydoc and therefore can change whenever there is a API modification. Therefore, it would be better to remove them from versioning.Some files under versioning located in docs/ are generated by pydoc and therefore can change whenever there is a API modification. Therefore, it would be better to remove them from versioning.Julien Girard-SatabinJulien Girard-Satabinhttps://git.frama-c.com/pub/cabrnet/-/issues/28Copy the visualizer config file in the checkpoints so that they are easy to r...2024-03-04T09:05:13ZAlban GrastienCopy the visualizer config file in the checkpoints so that they are easy to retrieve when we restart a trainingRomain Xu-DarmeRomain Xu-Darmehttps://git.frama-c.com/pub/frama-c/-/issues/2691Cannot use ppx_inline_test in a Frama-C plugin2024-02-28T22:02:33Zpepega007xdCannot use ppx_inline_test in a Frama-C plugin<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
Setup a minimal Frama-C plugin which uses the `ppx_inline_tests` test runner, and run tests using `dune runtest`.
The test runner is configured according to this documentation: https://dune.readthedocs.io/en/stable/tests.html#inline-tests
Project structure:
```
hello/
├── dune
├── dune-project
└── hello.ml
```
dune-project:
```
(lang dune 3.2)
(using dune_site 0.1)
(name frama-c-hello)
(package (name frama-c-hello))
```
dune:
```
(library
(name hello)
(public_name frama-c-hello.core)
(libraries frama-c.kernel)
(preprocess (pps ppx_inline_test))
(inline_tests)
)
(plugin
(optional)
(name hello)
(libraries frama-c-hello.core)
(site (frama-c plugins))
)
```
hello.ml:
```ml
let%test "should fail" = 1 = 2
```
### Expected behaviour
The test inside `hello.ml` executes and prints an assertion error.
### Actual behaviour
Building the test fails with the following error:
```
Error: No implementation found for virtual library "frama-c.init" in
/home/tb/.opam/default/lib/frama-c/init.
-> required by library "frama-c.kernel" in
/home/tb/.opam/default/lib/frama-c/kernel
-> required by library "frama-c-hello.core" in _build/default
-> required by
_build/default/.hello.inline-tests/inline_test_runner_hello.exe
-> required by _build/default/.hello.inline-tests/partitions-best
-> required by alias runtest in dune:6
```
### Contextual information
- Frama-C installation mode: installed using `opam install frama-c`
- Frama-C version: 28.0 (Nickel)
- Plug-in used: minimal plugin
- OS name: Fedora Linux
- OS version: 38 (Workstation Edition)
### Additional information (optional)
The project build just fine using `dune build`, only the `@runtest` target fails to build.https://git.frama-c.com/pub/frama-c/-/issues/2690[WP] Frama-C/WP 28.0 does not work with Isabelle/HOL2024-03-06T11:53:41Zkwaxer[WP] Frama-C/WP 28.0 does not work with Isabelle/HOL### Steps to reproduce the issue
1. Make sure Isabelle/HOL is installed and `why3` is configured to use it.
2. Create file `test.h` with the following code:
```
/*@
logic \list<integer> enumeration (integer n) = n == 0 ? \Nil : enu...### Steps to reproduce the issue
1. Make sure Isabelle/HOL is installed and `why3` is configured to use it.
2. Create file `test.h` with the following code:
```
/*@
logic \list<integer> enumeration (integer n) = n == 0 ? \Nil : enumeration (n - 1) ^ [|n - 1|];
lemma enumeration_length: \forall integer n; 0 <= n ==> \length (enumeration (n)) == n;
*/
```
3. Run WP plugin selecting Isabelle/HOL as a backend: `frama-c -wp -wp-prover=why3:isabelle -wp-interactive=fix -wp-cache=none test.h`
### Expected behaviour
Earlier versions of Frama-C (e.g. 27.1) produce the following output:
```
[kernel] Parsing test.h (with preprocessing)
[wp] 1 goal scheduled
[wp] Proved goals: 1 / 1
Qed: 0
Isabelle 2022: 1 (8.1s)
```
with the theory
```isabelle
theory lemma_enumeration_length imports Why3.Why3 begin
why3_open "lemma_enumeration_length.xml"
why3_vc wp_goal
using assms L_enumeration_def
by (induction i) (simp_all add: facts.length_concat length_cons length_nil)
why3_end
end
```
### Actual behaviour
Frama-C 28.0 produces the following:
```
[kernel] Parsing test.h (with preprocessing)
[wp] 1 goal scheduled
[wp] [Failure] typed_lemma_enumeration_length (Isabelle)
[wp] Proved goals: 0 / 1
Qed: 0
Failed: 1
```
### Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *28.0 (Nickel)*
- Plug-in used: *WP*
- OS name: *Ubuntu*
- OS version: *22.04.4 LTS*
### Additional information (optional)
`-wp-msg-key why3_api` gives the following error trace:
```
[wp] Failure: [Why3 Error] anomaly: Sys_error(".../.frama-c/wp/interactive/lemma_enumeration_length/.xml: No such file or directory")
Raised by primitive operation at Stdlib.open_out_gen in file "stdlib.ml", line 331, characters 29-55
Called from Stdlib.open_out in file "stdlib.ml" (inlined), line 336, characters 2-74
Called from Frama_c_kernel__Command.pp_to_file in file "src/libraries/utils/command.ml", line 31, characters 13-35
Called from Wp__ProverWhy3.prepare in file "src/plugins/wp/ProverWhy3.ml", line 1339, characters 6-130
Called from Wp__ProverWhy3.interactive in file "src/plugins/wp/ProverWhy3.ml", line 1352, characters 8-37
Called from Wp__ProverWhy3.build_proof_task in file "src/plugins/wp/ProverWhy3.ml", line 1413, characters 8-59
```
There is an unexpected slash right the before `.xml` file extension.https://git.frama-c.com/pub/cabrnet/-/issues/27Change model.yml to model_arch.yml2024-02-29T12:02:20ZRomain Xu-DarmeChange model.yml to model_arch.ymlIt appears that the name model.yml can be somewhat confusing as it **may** imply that the file contains everything necessary to build and initialize the model, when it actually only the information regarding the model architecture.
To em...It appears that the name model.yml can be somewhat confusing as it **may** imply that the file contains everything necessary to build and initialize the model, when it actually only the information regarding the model architecture.
To emphasize this, we could rename model.yml into model_arch.yml in the documentation and the provided examples.https://git.frama-c.com/pub/cabrnet/-/issues/26Specify config directory as an alternative to individual files2024-02-29T12:02:49ZRomain Xu-DarmeSpecify config directory as an alternative to individual filesIt is sometimes tedious to specify multiple YML files from the same configuration directory. It would be nice to offer an optional `--config-dir` alternative. This would mean that each script expects specific filenames for the different ...It is sometimes tedious to specify multiple YML files from the same configuration directory. It would be nice to offer an optional `--config-dir` alternative. This would mean that each script expects specific filenames for the different files:
+ For `train.py` and `import.py`, we would expect `model.yml`, `dataset.yml`, `training.yml` and `visualization.yml`
+ For `evaluate.py`, we would expect `model.yml`, `model_state.pth` or `legacy_state.pth`, `dataset.yml`
+ For `explain_local.py`, we would expect `model.yml`, `model_state.pth`, `dataset.yml` and `visualization.yml`
+ For `explain_global.py`, we would expect`model.yml` and `model_state.pth`https://git.frama-c.com/pub/cabrnet/-/issues/25Improper deletion of nodes2024-02-23T14:50:45ZAlban GrastienImproper deletion of nodesIn Prototree's pruning method (`cabrnet.utils.tree.prune_children`) the deletion of nodes seems to be inappropriate. When navigating the tree via the `named_children` after the pruning, the same leaf can be reached multiple times.In Prototree's pruning method (`cabrnet.utils.tree.prune_children`) the deletion of nodes seems to be inappropriate. When navigating the tree via the `named_children` after the pruning, the same leaf can be reached multiple times.Romain Xu-DarmeRomain Xu-Darmehttps://git.frama-c.com/pub/cabrnet/-/issues/24Visualization.yml in checkpoint2024-02-29T12:02:38ZAlban GrastienVisualization.yml in checkpointCould we include `visualization.yml` in the checkpoint? Makes the `resume-from` encore plus awesome.Could we include `visualization.yml` in the checkpoint? Makes the `resume-from` encore plus awesome.Romain Xu-DarmeRomain Xu-Darmehttps://git.frama-c.com/pub/cabrnet/-/issues/23resume-from best2024-02-23T10:18:53ZAlban Grastienresume-from bestIl semble impossible de faire un resume-from depuis un `best` checkpoint.
Par exemple, ça fonctionne :
`cabrnet train --seed 20240220 --device cuda:0 --verbose --resume-from output_2024_02_20_10/epoch_50/ --visualization configs/proto...Il semble impossible de faire un resume-from depuis un `best` checkpoint.
Par exemple, ça fonctionne :
`cabrnet train --seed 20240220 --device cuda:0 --verbose --resume-from output_2024_02_20_10/epoch_50/ --visualization configs/prototree/visualization.yml --output-dir output_elsewhere`
Mais pas ça :
`cabrnet train --seed 20240220 --device cuda:0 --verbose --resume-from output_2024_02_20_10/best/ --visualization configs/prototree/visualization.yml --output-dir output_elsewhere`
Étant donné que les deux folders `epoch_50` et `best` contiennent les même fichiers, le comportement devrait être semblable.Romain Xu-DarmeRomain Xu-Darme